From Idea to Provably Safe Implementation
Modeling, Proving, Simulation, and Synthesis in KeYmaera X
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:
- model cyber-physical systems
- express safety/correctness properties
- find bugs in a system design
- identify safety constraints
- identify system invariants
- fully verify the final system design
- write automated tactics for (sub)systems that serve as "unit proofs", in analogy to unit tests
- derive new products from a verified system design and refine a system design while retaining correctness proofs
- 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
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:- learn how to model systems with hybrid programs and how to simulate models in KeYmaera X
- learn how to prove models with KeYmaera X both automatically and manually
- learn how to interpret counterexamples and find bugs in models
- learn how to use proof techniques, such as differential invariants, to prove properties of nonlinear differential equations
- learn how to use KeYmaera X to find correct switching conditions for a controller
- learn how to write tactics for steering the proof search of KeYmaera X
- learn how to turn a model into a safety-ensuring runtime monitor.
Lecturer Short Biographies
|
|
|
|
|
|