Combining Forces: How to Formally Verify Informally Defined Embedded Systems

Herber P, Liebrenz T, Adelt J

Abstract

Embedded systems are ubiquitous in our daily lives, and they are often used in safety-critical applications, such as cars, airplanes, or medical systems. As a consequence, there is a high demand for formal methods to ensure their safety. Embedded systems are, however, concurrent, real-time dependent, and highly heterogeneous. Hardware and software are deeply intertwined, and the digital control parts interact with an analogous environment. Moreover, the semantics of industrially used embedded system design languages, such as MATLAB/Simulink or SystemC, is typically only informally defined. To formally capture informally defined embedded systems requires a deep understanding of the underlying models of computation. Furthermore, a single formalism and verification tool are typically not powerful enough to cope with the heterogeneity of embedded systems. In this paper, we summarize our work on automated transformations from informal system descriptions into existing formal verification tools. We present ideas to combine the strengths of various languages, formalisms, and verification backends, and discuss promising results, challenges and limitations.