RESCUE - Reliable Embedded System Design based on Co-verification in a Unified Environment

Embedded systems are often employed in safety-critical applications, for example, in cars, airplanes or traffic control systems. This makes their correctness crucial to avoid high financial losses or even human injuries or deaths. However, the verification of embedded systems is a challenge, mainly because these systems are very complex, have to run on limited resources, and typically consist of deeply integrated hardware (HW) and software (SW) components.  At the same time, embedded systems typically involve interdisciplinary applications, which introduces further heterogeneity into the set of used models of computation, and what makes it hard to gain a clear understanding of what is exactly happening. 
In the RESCUE project, we have investigated the idea that the scalability of existing verification techniques can be significantly increased by combining static analyses, slicing, and verification techniques from various communities. The underlying observation of the RESCUE project is that some systems or components can be quite effectively verified with model checking, while others can be more effectively verified using SMT solving or counter-example guided abstraction refinement.

A key concept that enables compositional hardware/software co-verification in our RESCUE frame- work is that formal models can be automatically derived from models with an informally defined execution semantics, e.g., from SystemC or Simulink models. The key idea behind our formalizations is that for informal system models with informally defined execution semantics, we map the informally defined execution semantics into an existing formally well-defined language. From this semantic mapping, we derive transformation rules for relevant language constructs, and define predefined components for key components of the language definition that define its execution semantics, for example, for the SystemC or Simulink scheduler. Based on our semantic mapping, we have then developed fully-automatic transformations from industrially used system design languages into well-defined formal models. By using existing formal languages, we gain access to existing verification tools, which we can used to verify given requirements, for example, safety, liveness, and timing properties. If the requirements are not satisfied, we tyipcally get a counter-example, which can be used for debugging. Our approach has three major advantages: First, with our semantic mapping, we define formal semantics for the informally defined industrial system design languages. Second, the transformation into formal models is performed fully-automatically, which means that we spare the de- signer the tedious task of creating a formal model and just derive it from an existing system description automatically. Third, we gain access to existing and thus mature and sophisticated verification tools. For SystemC, we have developed transformations into the input languages of three powerful verification tools: the real-time model checker U PPAAL , which is especially well-suited for real-time systems and communication architectures, the bit-precise SMT solver UCLID which is especially well-suited for hardware components, and the software model checker BLAST, which is especially well-suited for software model checking. For Simulink, we have developed transformations into the input languages of the bit-precise SMT solver UCLID and an interactive theorem prover for hybrid systems, namely KeYmaera X.

The results of this project are published in [HRB13, HH14, HPG15, JH17, LHG18, LHG19, LHG20, SH20, HL20] 

Principal Investigator: Prof. Dr. Paula Herber
Research Assistants: Lydia Jaß, Timm Liebrenz, MSc