Research
The research of the group focusses on software engineering. In particular, we consider the use of formal methods for the correct construction and analysis of complex software systems. Current research addresses verification and analysis techniques for embedded software and systems, and we investigate workflow and process modeling methodologies based on model-driven design and service orientation. We are especially interested in
- Formal methods and test automatization
- Verification and validation of embedded systems
- Quality assurance for hardware/software codesigns
- Workflow and process modeling
The RESCUE project
This project is funded by the German Research Foundation (DFG).
Reliable Embedded System Design based on Co-verification in a Unified Environment (RESCUE)
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.