Dr. Stefan Mitsch
Biography
Dr. Stefan Mitsch is a System Scientist in the Logical Systems Lab of Carnegie Mellon University's Computer Science Department. He received his PhD in computer science from Johannes Kepler University in 2012, and was awarded a Promotio Sub Auspiciis Praesidentis Rei Publicae and a ERC Marie Curie research fellowship. His research focuses on modeling, formal verification, and verified runtime safety methods for cyber-physical systems. He is particularly interested in bridging system design, formal verification, and runtime safety to build safe learning-enabled systems.
Abstract
Cyber-physical systems (CPS) are today pervasively embedded into our lives and increasingly act in close proximity as well as with direct impact to humans. For example, driver assistance systems in cars are responsible for controlling acceleration and braking on the basis of distance sensors. Further prominent examples can be found in many safety-critical areas where lives are at stake, such as in factory automation, medical equipment, aviation, automotive, railway industries, and robotics. Formal verification techniques are particularly suitable to provide the necessary correctness guarantees at the necessary level of trust. Reliable CPS safety demands techniques and tools that analyze the control software in learning-enabled systems together with its real-world physical effect to guarantee correctness for all of the infinitely many possible states of a cyber-physical system.
In this series of lectures, we will introduce the modeling language, proof techniques, and synthesis tools of the theorem prover KeYmaera X. KeYmaera X is a theorem prover for hybrid systems, which are mathematical models of cyber-physical systems that combine discrete computations with their continuous physical effects. We will learn the foundations and proof techniques for analyzing hybrid systems, such as induction for discrete computations and their continuous counterparts, such as differential invariants for differential equations. Once a hybrid system is proved correct, the remaining question is whether or not the model used for verification adequately represents the real system and its environment. We will discuss the ModelPlex approach to synthesize provably correct monitor expressions, which test the running system for deviation from the verified model. When run alongside controllers on the real system as watchdogs, these monitors initiate emergency actions on deviation to keep the system safe in a provably correct way.
Throughout the lectures, we will work on models of a ground robot as a running example. The examples will start with simple tasks that KeYmaera X can prove fully automatically (e.g., drive a robot in a straight line to a charging station and stop there) and progress to more complicated models where manual interaction or advanced proof techniques become necessary (e.g., prove properties steering and curved paths).
Participants will learn how to model hybrid systems using hybrid programs, how to avoid modeling pitfalls, how to prove safety properties (e.g., that the robot never collides with walls or never runs past the charging station), and how to integrate formal methods with learning-enabled systems. To explore safety verification concepts we will interact with KeYmaera X through its point-and-click web interface and through its tactics programming language. Tactics provide a powerful way of automating either generic or domain-specific proof search procedures for cases that are out of reach for current proof strategies.