From transistor level to cyber physical/hybrid systems: Formal verification using automatic compositional abstraction

Abstract

In this paper we present a methodology to automatically generate an accurate behavioral model from an analog circuit description. The current machine learning method is limited to circuits with up to 80 transistors, limiting our approach to small and mid size circuit blocks due to a state explosion problem. However, if complex building blocks such as IOT systems should be modeled, the current approach needs to recoup with feasible simulation and modeling time. To come up with a solution for this problem, we extend the current method by a compositional approach. The approach is illustrated upon an example from the area of autonomous driving. Our method decomposes this large example into smaller building blocks and models each of them automatically. All models are combined into a compositional hybrid automaton of the whole complex system. Compared to the original state space, the building blocks operate on smaller and reduced state spaces and hence drastically reduce the complexity. Using a back-transformation on the compositional automaton, all values from the original state space can be reconstructed. Moreover, we perform a formal verification on the generated compositional automaton. Results from a meaningful example are presented and discussed.