Formal Abstraction and Verification of Analog Circuits (faveAC)

Motivation

Many safety-critical systems such as for example automated vehicles or surgical robots are controlled by electrical circuits. Since a malfunction of the circuit would most of the time result in a failure of the whole system, it is required to verify that these electrical circuits operate correctly. But since there exist no practicable methods for formal verification of electrical circuits, correct behavior is mostly verified by extensive simulation of the system. This method however is time consuming and therefore also costly, and in addition does not provide formal guarantees for correct functionality. A practicable tool for formal verification of analog circuits would therefore potentially lead to significant improvements in the design process of electric circuits for safety-critical applications.

Objective

The goal of the faveAC-project is to develop practicable methods for the formal verification of analog or mixed-signal electrical circuits. This is realized with the following overall high-level strategy: First, nonlinear elements of the circuit are approximated with a piecewise linear model. An example of this procedure is visualized for a MOSFET transistor in the images above. Thereby, the piecewise linear model is constructed in such a way that it is an over-approximation of the nonlinear dynamics from the real element. In a second step, the piecewise linear models of the single elements are combined, which results in a model for the whole circuit. Finally, reachability analysis is applied to the model of the overall circuit in order to verify that the system fulfills all specifications and does not violate any constraints.

Project Organization

Due to the complexity of the overall task, the project is realized as a collaboration between the Technichal University of Munich, Goethe-Universität Frankfurt am Main and Leibniz Universität Hannover. While the groups in Frankfurt and Hannover develop methods for the automated model generation of analog circuits, our research here in Munich is focused on improvements for reachability analysis of dynamical systems.

People

• Niklas Kochdumper, M.Sc.
• Prof. Dr.-Ing. Matthias Althoff