CS Talk
Maximilian Schwenger
Monday - October 21, 2019
3:00 p.m., AKW 300
Host: Ruzica Piskac
Please let her know if you would like to meet Max. He will be visiting today and tomorrow.
Title: Let’s not Trust Experience Blindly: Formal Runtime Verification for CPS
Abstract:
The control logic of complex systems is based on experience: Trained experts steer a machine directly until they help develop an automated controller. Recently, this process was further improved by successfully incorporating machine learning techniques, where the controller was learned from tremendous amounts of empirical data. The resulting controller excels most of the time, especially in situations similar to ones occurring in the training data. In a safety-critical context, however, this is not enough, so formal guarantees about the behavior of the controller become crucial. When a full static analysis and subsequent verification is infeasible due to the complexity of the system, runtime verification is still applicable. It acts as a connecting link between the efficiency of the developed controllers and formally verifiable guarantees. A runtime monitor assesses the system health by using a specification that contains information about desired system states and their expected evolution over time. When the monitor encounters a violation of the specification, it raises an alarm. For complex systems, characterizing the desired behavior requires an expressive language. Moreover, provably correct behavior requires formal semantics and an evaluation algorithm with static guarantees on its resource consumption to prevent crashes during runtime.
In this talk, we present our approach to runtime verification which revolves around the specification language RTLola. We outline RTLola’s formal semantics and illustrate its practicality in terms of expressiveness. Static analyses allow for assessing upper bounds on the resource consumption of the respective monitor. Lastly, we briefly touch upon a compilation of an RTLola specification to VHDL code, which can be realized on an FPGA.
Bio:
Maximilian Schwenger started his PhD in 2017 at Saarland University. Supervised by Prof. Bernd Finkbeiner, his research focuses on formal runtime monitoring with a special interest in cyber-physical systems and human health monitoring. For this, he contributed to the development of the monitoring framework StreamLAB, specifically the real-time aspect thereof. His wider interests include formal language design, hybrid systems and machine learning.