We present the first work on the automated generation of reachset conformant models for analog circuits. Our approach applies reachset conformant synthesis to add non-determinism 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 non-determinism 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.     «

We present the first work on the automated generation of reachset conformant models for analog circuits. Our approach applies reachset conformant synthesis to add non-determinism 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 non-determinism for the piecewise-linear models. The effectiveness of our approach is demonstrated on a real analog circuit. Since the resulting models...     »