Modular Formal Verification of CyberPhysical Systems with KeYmaera X

KeYmaera X
and FM tutorial and Registration 
Agenda
9:0010:00 Elementary CPS 

9:00  CyberPhysical Systems: Specification and Verification [pdf] André Platzer 
10:3012:30 Practice & Advanced CPS 

10:30  Formal Verification in KeYmaera X Stefan Mitsch 
11:15  Differential Equation Verification [pdf] André Platzer 
14:0015:00 CPS Components 

14:00  Componentbased Modeling and Verification for CPS Stefan Mitsch 
Summary
This tutorial studies modularity principles for the design and formal verification of cyberphysical 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, componentbased 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 CyberPhysical Systems.
Registration
Register for KeYmaera X tutorial at FMWEEK
While the tutorial will be selfcontained, 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 cyberphysical systems (CPSs), as well as an understanding how wellfounded 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, componentbased 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 componentbased CPS verification is challenging because both local component behavior (e.g., decisions and motion of a robot) and inherently global phenomena (e.g., time) cooccur, 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 CyberPhysical 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 skullbase surgery.
Lecturer


