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

• Applicant: Professorin Dr.-Ing. Paula Herber
• Subject Area: Computer Architecture, Embedded and Massively Parallel Systems
• Term: from 2013 to 2021
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 234310760

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. To overcome this problem, we propose a modular verification framework that supports the whole design flow of digital HW/SW system combining a variety of verification techniques, ranging from formal hardware verification over software verification to system verification. We target the system level design language SystemC, which has become the de facto standard in HW/SW co-design, but severely lacks support for automated and comprehensive verification. Its semantics is only informally defined, and verification techniques are ad-hoc and non-systematic. To achieve a formally well-founded verification flow, We start with a formal definition of an intermediate representation (IR) for SystemC (SysCIR). Then, we process the SysCIR by a set of modular engines. First, we develop innovative slicing and abstraction engines, which significantly reduce the semantic state space. Second, we provide a set of transformation engines that target a variety of verification tools. In particular, we combine hardware, software and system verification techniques in order to cope with the different models of computation inherently intertwined in embedded HW/SW systems. Another important contribution will be a technique to automatically select and combine our slicing, abstraction, and transformation engines.

• DFG Programme: Research Grants