TU Berlin

Software and Embedded Systems EngineeringRESCUE

SESE-Logo in blau

Page Content

to Navigation

The RESCUE Project

This project is funded by the German Research Foundation.

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.  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.

Project Participants

Principal Investigator
Prof. Dr. Paula Herber
Research Assistant
Timm Liebrenz
Former Research Assistant
Lydia Jaß


Quick Access

Schnellnavigation zur Seite über Nummerneingabe