Establishing Reachset Conformance for the Formal Analysis of Analog Circuits
Niklas Kochdumper, Ahmad Tarraf, Malgorzata Rechmal, Markus Olbrich, Lars Hedrich, Matthias Althoff · 2020
We present the first work on the automated generation of reachset conformant models for analog circuits. Our approach applies reachset conformant synthesis to add nondeterminism to piecewise-linear circuit models so that they enclose all recorded behaviors of the real system. To achieve this, we present a novel technique to compute the required nondeterminism for the piecewise-linear models. The effectiveness of our approach is demonstrated on a real analog circuit. Since the resulting models enclose all measurements, they can be used for formal verification.