Static Analysis and Verification of Embedded and Cyber-Physical Systems

Sabine Glesner (Technische Universität Berlin)

part of “Distinguished Lecturer Series”

Software has become a central and integral part of many systems and products of the information era. In embedded and cyber-physical systems, software is not an isolated component but instead an integrated part of larger, e.g. technical or mechanical systems. During the last decades, there has been an exponential growth in the size of embedded software, resulting in an increasing need for software engineering methods addressing the special needs of the embedded and cyber-physical domain.
Especially in cyber-physical systems, security has become a major issue. Systems communicate with each other and with their environments and, hence, need to be open and to have interfaces to the outside.
Nevertheless, being open also implies that malicious intruders can gain access. A first step to increase security is to understand how data and information in the system can flow.

In this talk, I present research results concerning information flow analysis for systems that are modeled in Matlab/Simulink/Stateflow, which is one of the modeling and programming languages of choice in technical environments. A particular problem arises in these systems as they also show time-dependent behavior. We have modeled this behavior by timed automata and constraint systems. Our results can be directly applied to systems from the automotive domain, which I demonstrate by presenting respective case studies from our experiments. Concludingly, I give an overview over further research topics in my group.