Entwicklung zuverlässiger eingebetteter Systeme in einer modularen Verifikationsumgebung
Zusammenfassung der Projektergebnisse
The verification of embedded systems is challenging, mainly because these systems have a high complexity, have to run on limited resources, and typically consist of deeply integrated hardware and software components. The correct and reliable construction of complex embedded systems requires a clear understanding of the models and languages that are used in the development process. Formal methods provide a basis to achieve such an understanding and to make the development process systematic, well-defined, and automated. However, there are two major barriers that preclude formal methods from standard industrial design processes: First, the models and languages that are used in industrial practice often have informally defined semantics and thus do not allow for automated and comprehensive quality assurance. Second, existing automatic formal verification and formally founded test techniques typically suffer from the state space explosion problem. As a consequence, their scalability is limited. The aim of the RESCUE project was to develop a modular verification framework that enables the correct and reliable construction of complex embedded systems. Our key ideas are twofold: first, we have proposed a quality assurance process that starts with a formalization of the (informally defined) system under verification. To this end, we have proposed that informal system descriptions are automatically transformed into formal models, which enable formal verification using existing verification tools. Second, to increase the scalability of the verification, we have proposed a compositional hardware/software co-verification approach where the strengths of multiple verification techniques are combined. In particular, we have proposed a framework where subsystems can automatically be transformed into the input languages of representatives of the three main classes of verification systems: A real-time model checker (namely U PPAAL), an automatic theorem prover based on SMT solving as typically used in hardware verification (namely UCLID), and a software model checker (namely BLAST). With our approach, a heterogeneous integrated hardware/software system can be verified with the combined force of multiple verification techniques. For each partial verification, an abstraction of the rest of the system is computed to ensure safe results with acceptable verification effort. Our ideas for a compositional hardware/software co-verification approach using multiple verification backends have been published. Our transformation from SystemC to U PPAAL timed automata has been developed in the context of two PhD theses. Valuable extensions (e.g. support for the verification of memory-related properties) have been made within in the RESCUE project and were published. Note that our SystemC to Timed Automata Transformation Engine STATE is freely available. Transformations from SystemC to the input languages of BLAST and UCLID are also published. To increase the scalability of the verification process, we have developed a novel domain-specific abstraction technique for SystemC. Besides our transformation that enable the verification of integrated hardware/software systems that are modeled in the system level design language SystemC, we have also developed transformations from the informal system modeling language Simulink into formal verification backends. Simulink enables modeling and simulation of dynamic and hybrid systems, and is widely used for model-based development of embedded systems in academia and industry. Our transformation from discrete Simulink models to UCLID has been implemented and enables the automated verification of Simulink models with k-inductive invariant verification. Our transformation from hybrid Simulink models into the differential dynamic logic (dL) enables formal verification of hybrid systems that are modeled in Simulink using the interactive theorem prover KeYmaera X. To the best of our knowledge, the RESCUE project is the only one worldwide that systematically combines the strength of multiple verification techniques from different communities for hardware/software co-verification, i.e. real-time model checking with hardware and software verification, in a formal framework. We have gained deep insights on the domain specific features of system level design languages for embedded systems such as SystemC and Simulink, and systematically exploited them to increase the scalability of formal verification. With that, we have done an important step towards increasing the safety for industrial embedded systems as they are used in cars, airplanes, or medical devices.
Projektbezogene Publikationen (Auswahl)
-
Bit-precise formal verification of discrete-time MATLAB/Simulink models using SMT solving. In International Conference on Embedded Software (EMSOFT), pages 1–10. IEEE, 2013
Paula Herber, Robert Reicherdt, and Patrick Bittner
-
The RESCUE Approach – Towards Compositional Hardware/Software Co-verification. In IEEE International Conference on Embedded Software and Systems (ICESS), pages 721–724. IEEE, 2014
Paula Herber
-
Bit-Precise Formal Verification for SystemC using Satisfiability Modulo Theories Solving. In International Embedded Systems Symposium (IESS’2015), IFIP AICT 403, pages 44–53. Springer, 2015
Lydia Jaß and Paula Herber
-
Deductive Verification of Hybrid Control Systems modeled in Simulink with KeYmaera X. In International Conference on Formal Engineering Methods (ICFEM 2018, pages 89 – 105. LNCS volume 11232. Springer, 2018
Timm Liebrenz, Paula Herber, Sabine Glesner
