Service and Software Engineering

Interim Professor: Dr. Thomas Göthel

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

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.

STATE

STATE is a SystemC to Timed Automata Transformation Engine. It takes a SystemC design as input and transforms it into a corresponding UPPAAL timed automata model. The transformation is based on a formal semantics defined for SystemC in [Her08],[Her10],[Her11],[Pockr11],[Pockr13],[Her13]. The general idea is to map the informally defined semantics of SystemC to the formally well-defined semantics of UPPAAL timed automata. This mapping defines a formal semantics for SystemC, and, at the same time, it enables the automatic transformation from a given SystemC design into a semantically equivalent UPPAAL timed automata model. The transformation preserves the informally defined semantics of SystemC completely. To ease debugging, it also keeps the structure of the original SystemC design transparent to the designer in the UPPAAL model (through prefixing). The current version of STATE supports structs, pointers, and arrays as well as the TLM 2.0 standard. STATE 2.0 is licensed under GPL and freely available at the STATE project website.

Workflow and Process Modeling

We investigate workflow and process modeling methodologies based on model-driven design and service orientation. Our particular research focus is on the use of formal methods (such as model checking and synthesis techniques) in the workflow design process in order to make it more domain-specific and bring application development to a user-accessible level. This involves to a large extent also a careful semantic domain modeling, that is, the adequate formalization of the required domain knowledge, typically making use of ontologies and constraints. While we are principally open to all application areas, our focus is on scientific disciplines, such as bioinformatics, geoinformatics, medical research and business analytics, where we work in close collaboration with the respective domain experts. Current initiatives comprise a joint project with the Potsdam Institute for Climate Impact Research on workflows for climate impact risk assessment, and a cooperation with the Cancer Metabolism Research Group of the University of São Paulo on workflows and processes for the collection and analysis of experimental data.

External Cooperations

We are involved in several projects at TU Berlin: