From transistor level to cyber physical/hybrid systems: Formal verification using automatic compositional abstraction
| Autor: | Lars Hedrich, Ahmad Tarraf |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
010302 applied physics
General Computer Science business.industry Computer science Transistor Cyber-physical system Information technology 02 engineering and technology 01 natural sciences 020202 computer hardware & architecture law.invention law Hybrid system 0103 physical sciences 0202 electrical engineering electronic engineering information engineering business Software engineering Formal verification Abstraction (linguistics) |
| Zdroj: | it - Information Technology. 62:257-270 |
| ISSN: | 2196-7032 1611-2776 |
| DOI: | 10.1515/itit-2020-0004 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|