Modular Formal Verification of Cyber-Physical Systems with KeYmaera X

Agenda

Summary

This tutorial studies modularity principles for the design and formal verification of cyber-physical systems (CPS), which are those that combine cyber aspects such as communication and computer control with physical aspects such as movement in space. CPSs have many important applications, e.g., in robotics, aerospace, and automotive domains, but require careful designs to meet stringent safety demands. Formal verification techniques justify such safety properties but need to handle mathematical models of CPSs called hybrid systems, i.e., those that combine the discrete dynamics of stepwise controller computations with the continuous dynamics of their differential equations.

This tutorial explains how differential dynamic logic (dL) for hybrid systems can be used to model and verify CPS in a modular fashion. Its theorem prover KeYmaera X provides compositional verification techniques for hybrid systems, which not only handle nonlinear systems but also use invariants to reduce the verification of larger systems to subsystems. For very large models, component-based modeling can be used to split large models into multiple component models with local responsibilities to further reduce modeling complexity. Yet, this only helps the analysis if verification proceeds one component at a time. We show how decomposition into subcomponents works by disentangling the physical interaction into measurements and actuation guarantees that are represented in local contracts. More detail about the presented approach can also be found in the recent textbook on Logical Foundations of Cyber-Physical Systems.

Registration

Register for KeYmaera X tutorial at FMWEEK

While the tutorial will be self-contained, if you want to follow along or try out KeYmaera X yourself in the breaks we suggest to install all software ahead of time.

Description

The purpose of this tutorial is to give the audience an understanding of the unique challenges and opportunities of cyber-physical systems (CPSs), as well as an understanding how well-founded logic and modularity principles help master the fundamental challenges in safe CPS design. Direct interaction of physical behavior alongside computerized control in CPSs enables important practical applications, including automotive, aviation, railway, and robotics, which are all subject to stringent safety demands. Formal verification techniques justify such safety properties, but need to handle the interplay between discrete dynamics (e.g., coming from the computations that a computer performs one discrete step at a time) and continuous dynamics (e.g., the continuous physical motion of an aircraft through the air), described in mathematical models called hybrid systems. For this purpose, differential dynamic logic (dL) provides logically grounded ways of specifying and verifying the correctness of the behavior of hybrid systems, written as hybrid programs. The theorem prover KeYmaera X provides compositional verification techniques for hybrid systems, which not only handle nonlinear systems but also use invariants to reduce the verification of larger systems to subsystems.

For very large models, component-based modeling can be used to split large models into multiple component models with local responsibilities to further reduce modeling complexity. Yet, this only helps the analysis if verification proceeds one component at a time. Modular component-based CPS verification is challenging because both local component behavior (e.g., decisions and motion of a robot) and inherently global phenomena (e.g., time) co-occur, as components can interact virtually (e.g., robots communicate) and physically (e.g., a robot manipulates an object), and because their interaction is subject to measurement uncertainty and actuation disturbance. Key steps that we will also study in this tutorial include how decomposition into subcomponents works by disentangling the physical interaction into local responsibilities with measurements and actuation guarantees that are represented in local component contracts, and how KeYmaera X builds system proofs from local component safety proofs with communication and compatibility proofs.

This tutorial is based on the accessible but rigorous approach for CPSs that is provided in a recent textbook on Logical Foundations of Cyber-Physical Systems. The logic dL that is the foundation for this tutorial has been instrumental in the safety design and verification of many applications, including the Airborne Collision Avoidance System ACAS X, the European Train Control System, mobile robot navigation, and a medical robot for skull-base surgery.

Lecturer

Stefan Mitsch Stefan Mitsch is a System Scientist at Carnegie Mellon University. He obtained his Ph.D. from Johannes Kepler University, Linz, Austria, in 2011, was awarded a Promotio Sub Auspiciis Praesidentis and received a Marie Curie Fellowship.

André Platzer André Platzer is an Associate Professor of Computer Science at Carnegie Mellon University. He obtained his Ph.D. from the University of Oldenburg, Germany, in 2008, received an ACM Doctoral Dissertation Honorable Mention and NSF CAREER award, and was named one of the Brilliant 10 Young Scientists by the Popular Science magazine and one of the AI's 10 to Watch by the IEEE Intelligent Systems Magazine.