SAVES - Scalable Verification of Industrial Embedded Control Systems

Embedded systems surround us everywhere in our everyday live. Their functionality spans from simple microcontrollers in a fridge to complex systems with millions of lines of code, for example in cars, airplanes, or smart factories. In such systems, failure often has serious consequences, such as huge financial losses or even loss of lives. Thus, the correctness and reliability of embedded systems are of vital importance. To establish correctness of embedded systems, however, is hard. With trends such as Industry 4.0, the internet of things, and autonomous driving, the complexity of embedded systems is steadily increasing. A prerequisite to ensure the correct functioning of industrial embedded systems under all circumstances is a clear understanding of the models and languages that are used in the development process. Formal methods provide a basis to make the development process systematic, well-defined, and automated. However, for many industrially relevant languages and models, the semantics are only informally defined. Together with the limited scalability of formal design and verification techniques, this makes the formal verification of industrial embedded control systems a difficult challenge, which can not be solved satisfactory with currently available methods and tools. At the same time, we see that in the area of deductive program verification, powerful techniques and tools have been developed to reason about software with unbounded parameters, for example the VerCors tool suite. In this project, we will extend these techniques with concepts to cope with heterogeneity, concurrency, and real-time to make them suitable for industrial embedded systems.

Cooperation partner: University of Twente, Formal Methods and Tools Group

Principal Investigators: Prof. Dr. Marieke Huisman, Prof. Dr. Paula Herber
Involved Researchers: Dr. Raúl Monti, Stefanie Drerup (Master Thesis)

SAVeHyM - Service-oriented Abstraction and Verification of Hybrid Models

Embedded control systems combine discrete and continuous behavior. To cope with the immense complexity of the resulting systems, they are increasingly designed with model-driven development and tools like Matlab Simulink. At the same time, application of embedded systems in safety-critical areas, like in the automotive industry or medical context, require high safety standards. In this project, we investigate a formally well-founded, service-oriented design and verification approach for Simulink. The key ideas of our approach are threefold: First, we propose a service-oriented design approach for Simulink, where we introduce services for Simulink, hybrid contracts to cleanly define these services, and feature models to model their variability. Second, we propose a transformation of Simulink models into the expressive and formally well-defined differential dynamic logic. This enables the formal verification of hybrid systems modeled in Simulink using the powerful interactive theorem prover KeYmaera X. To overcome scalability issues, we enable compositional verification by replacing the inner structure of services by their contracts for system verification.

Research Assistant: Timm Liebrenz, MSc

Example Models and Proofs: https://www.uni-muenster.de/EmbSys/research/projects/SAVeHyM.html

SysCSec - Early Analysis of Security Threats by Modeling and Simulating Power Attacks in SystemC

Side-channel attacks (SCA) enable attackers to gain access to non-disclosed information by measuring emissions of a system, for example, electromagnetic waves or power consumption. In many existing design processes, the emissions of a system can only be measured on the final system. As a consequence, the analysis of such security threats is often only possible at a very late stage in the development process. In this project, we investigate an approach to simulate power attacks in early stages of the development process. The key idea of our approach is threefold: First, we use the powerful system level design language SystemC to provide a detailed model of the power consumption of a given system. Second, we provide a graphical user interface to visualize and analyze the power consumption. Third, we develop predefined attacker modules in SystemC. Together, we provide a framework to simulate and analyze whether known power attacks are successful on a given system.

A preliminary implementation of our SysCSec framework  is licensed under GPL, freely available and demonstrates the applicability of our approach by modeling and simulating a simple power attack (SPA) on a system that uses elliptic curve cryptography (ECC), a differential power attack on a system that uses RSA encryption, and a cross-correlation analysis on the same system.

SysCSec.zip

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

Principal Investigator: Prof. Dr. Paula Herber
Research Assistant: Timm Liebrenz, MSc 

Effective Quality of Software Models (ECoSMo)

Cooperation Partners

STATE - a SystemC to Timed Automata Transformation Engine

STATE 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 is licences under GPL and freely available at https://www.uni-muenster.de/EmbSys/research/projects/state.html