KeYmaera X CPSWEEK 2016 Tutorial

From Idea to Provably Safe Implementation

 

Modeling, Proving, Simulation, and Synthesis in KeYmaera X

Table of Contents
  1. Objectives
  2. Topics
  3. Synthesis
  4. Content and Objectives
  5. Outcomes
  6. Lecturer Short Biographies

The verification tool KeYmaera has been used in the verification of several cyber-physical system (CPS) applications, including the Airborne Collision Avoidance System ACAS X, the European Train Control System ETCS, several automotive systems, mobile robot navigation with the dynamic window algorithm, and a surgical robotic system for skull-base surgery . Its successor, KeYmaera X, expands upon functionality by providing easier ways of augmenting the automatic proof capabilities and by providing proof-based code synthesis. KeYmaera X is also based on a significantly smaller soundness-critical core than all other hybrid systems verification tools, which makes it easier to ensure correct verification results.

KeYmaera X or
CPSWEEK tutorial or
Slides

 

Objectives

This tutorial will explain how hybrid system theorem proving in KeYmaera X can be used as a powerful technique to analyze and design safe cyber-physical systems. We will illustrate how developers can benefit from KeYmaera X by demonstrating on a series of examples how it can be used to:

  1. model cyber-physical systems
  2. express safety/correctness properties
  3. find bugs in a system design
  4. identify safety constraints
  5. identify system invariants
  6. fully verify the final system design
  7. write automated tactics for (sub)systems that serve as "unit proofs", in analogy to unit tests
  8. derive new products from a verified system design and refine a system design while retaining correctness proofs
  9. automatically synthesize correct monitors from the system design, which can be used as test cases or as runtime monitors to check compliance of observed behavior with the verified model
The presentation will focus on conducive examples and general takeaway messages.

 

Topics

The tutorial will introduce the modeling language, proof techniques, and synthesis tools of KeYmaera X . We will present techniques for analyzing both discrete and continuous parts of a model, such as differential invariants for differential equations Along the way, we will convey the intuition behind proof techniques for differential equations such as Lyapunov functions or differential invariants.

Throughout the tutorial, we will use a ground robot as a running example. The tutorial 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., proving properties about a trajectory generator).

Participants will learn how to model hybrid systems using hybrid programs, how to avoid modeling pitfalls, and how to prove safety properties (e.g., that the robot never collides with walls or never runs past the charging station). To explore safety verification concepts we will interact with KeYmaera X through its point-and-click web interface. We will then demonstrate how these manual point-and-click proofs can be automated using the 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 the proof strategies that already ship with KeYmaera X.

 

Synthesis

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 show participants how to use the ModelPlex proof tactic implemented in KeYmaera X 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.

The tutorial will feature practical hands-on tutoring and exercises done online using the web interface of KeYmaera X. Participants are invited to also bring their own computers with a web browser if they are seeking to gain hands-on experience in hybrid systems proving.

Content and Objectives

In an example-driven style, the tutorial will introduce the background, modeling, and proof techniques of KeYmaera X for formally verifying safety properties of hybrid systems. The emphasis in the tutorial is put on intuition grounded in insightful examples with generalizable takeaway messages. The tutorial is accompanied by a companion tutorial article for easy reference after the conference, a book and in-depth course material from an undergraduate course held at Carnegie Mellon University.

Outcomes

Participants will:

Lecturer Short Biographies

Nathan Fulton
Nathan is a Ph.D. student at Carnegie Mellon University. His research focuses on verification technology for cyber-physical systems and is a major developer of KeYmaera X.
Nathan Fulton
Stefan Mitsch
Stefan is a Marie Curie fellow at Johannes Kepler University, and associated with the Logical Systems Lab of Carnegie Mellon's Computer Science Department. His current research focuses on modeling, refactoring, verification, and monitoring methods for cyber-physical systems, and he contributed to ModelPlex and is a major developer of KeYmaera X.
Stefan Mitsch
André Platzer
André is an Associate Professor of Computer Science at Carnegie Mellon University. His interests include logic in computer science, cyber-physical systems, programming languages, formal methods, and automated theorem proving. He introduced differential dynamic logic and led the development of the KeYmaera and KeYmaera X provers for hybrid systems.
Andre Platzer