Name: Paula Herber
Title: Combine Forces - How to Formally Verify Informally Defined Embedded Systems
Abstract: Embedded systems are ubiquitous in our everyday lives, and they are often used in safety-critical applications, such as cars, airplanes, or medical systems. As a consequence, there is a high demand for formal methods to ensure their safety. Embedded systems are, however, concurrent, real-time dependent, and highly heterogeneous. Hardware and software are deeply intertwined, and the digital control parts interact with an analogous environment. Moreover, the semantics of industrially used embedded system design languages, such as Matlab/Simulink or SystemC, is typically only informally defined. To formally capture informally defined embedded systems requires a deep understanding of the underlying models of computation. Furthermore, a single formalism and verification tool are typically not powerful enough to cope with the heterogeneity of embedded systems. In this talk, I summarize our work on automated transformations from informal system descriptions into existing formal verification tools. I present ideas to combine the strengths of various languages, formalisms, and verification backends, and discuss promising results, challenges and limitations.
Short Bio: Prof. Dr.-Ing. Paula Herber received her Ph.D. from TU Berlin in 2010. She worked as a postdoc at the International Computer Science Institute (ICSI) in Berkeley, California, as a substitute professor at the University of Potsdam, and as a postdoc and independent research group leader in the Software Engineering and Embedded Systems group at TU Berlin. Since October 2018, she is a full professor at the University of Münster and head of the Embedded Systems Group at the Computer Science Department. Her main research interests are quality assurance for embedded systems, test automation, and formal methods.