|
Download
or Launch KeYmaera |
Using the KeYmaera Prover for Verifying Hybrid Systems
KeYmaera is a verification tool for hybrid systems and built as a hybrid theorem prover for hybrid systems. KeYmaera separates the overall verification workflow into two phase. In the first phase you specify the hybrid system that you would like to verify along with its correctness properties. In the second phase, you can use KeYmaera and its automatic proof strategies to verify the specified property of the hybrid system.
-
Load a KeYmaera problem specification using
- Project Assistant with the File->Load Project menu, e.g., for loading Simple Acceleration, or
- Load File to locate a .key problem specification file yourself using with the File->Load menu, e.g., for opening simple.key or use the toolbar
-
Run the automatic proof strategies to verify your hybrid system with the Proof->Start Proof Search menu or toolbar.
As a simple example, you can look at the following:
- File->Load Project
- Choose Simple Acceleration example
-
Run the automatic prover
- Depending on your settings, KeYmaera may stop showing you an intermediate result to inspect, just click again to proceed.
- Apply find counterexample rule to see if there is a counterexample for the property, if it cannot be proven.
- Directly select proof rules from the context menu, e.g., to discover parameter constraints for parametric verification.
- Adjust the proof strategy to your needs in the "Hybrid Strategy" tab to determine the proving behaviour of KeYmaera.
- Choose from many computational back-end solvers in "real arithmetic solver" option of the "Hybrid Strategy" tab to customise your prover and tune in to your system environment and improve verification power.
- Select visualization rule to see a graphical view of the transition system. (requirement: install graphviz/dotty)
KeYmaera Problem Specification Files by Example
You can specify the verification problem by loading a .key problem specification file. This file specifies bot the model of your hybrid system (using the notation of hybrid programs) and the correctness property that you want to verify.
Before we introduce the precise syntax of KeYmaera's specification language, we start with two introductory examples.
Example (Controlled Moving Point)
Consider the following simple example of a hybrid controller moving a point
x towards 0 on the real line.
It is a very simple bang-bang controller that pushes x opposite to its sign
such that it moves towards 0.
You can directly load it in KeYmaera and push the play button
to prove it automatically.
\problem { /* state variable declarations */ \[ R x, a, t, c; \] ( /* initial state characterization */ x^2 < (4*c)^2 -> \[ /* system dynamics */ ( if (x>0) then a := -4 /* move left */ else a := 4 /* move right */ fi; t := 0; /* reset clock variable t */ {x'=a, t'=1, t<=c} /* continuous evolution */ )* /* repeat these transitions */ \] (x^2 <= (4*c)^2) /* safety / postcondition */ ) } |
 |
- The outer program R x, a, t, c; declares all required real state variables for the system and any auxiliary variables for its correctness property (we need no auxiliary variables in this example).
- The correctness property itself is a safety property of the form φ -> \[α\] ψ.
It says that if φ is true initially then after all executions of α the system state satisfies ψ, where
- φ is the precondition characterising the initial states of the hybrid system.
- α specifies the hybrid system dynamics given as a hybrid program.
- ψ is the postcondition that is claimed to hold for all reachable states of the hybrid system (safety).
- In the example, the precondition x^2<(4*c)^2 of the implication characterises the set of possible initial states of the system. The controlled moving point system can start in any state satisfying this precondition.
- The hybrid system is specified as a hybrid program within the modality \[...\].
Here, it is given as a controller-plant loop of the form (controller; plant)*.
- The
discrete controller adjusts the control choice variable a depending on the current value of x by an if-then-else statement. - The
continuous plant dynamics is specified by a differential equation system x'=a,t'=1 with an additional evolution domain (or invariant region) t<=c. This differential equation characterises how the state variables x and t change over time. By the slope of 1, variable t is a clock variable. - The
evolution domain t<=c of the differential equation system specifies that the plant does not leave t<=c, i.e., takes at most c time units, which is a free parameter of the system. - The overall controller-plant loop repeats any number of times, which is indicated by the * at the end for repetition.
- The
- The postcondition x^2<=(4*c)^2 specifies the safety property that is conjectured to hold for each reachable state.
Example (Bouncing Ball)
As a standard example, consider the bouncing ball [7]. A ball falls from height h and bounces back from the ground (h=0) after an elastic deformation. The current speed of the ball is denoted by v, and t is a clock measuring the falling time. We assume an arbitrary positive gravity force g and that the ball loses energy according to a damping factor 0≤c<1.
\problem { /* state variable declarations */ \[ R h,v,t; R c,g,H \] ( /* initial state characterization */ g>0 & h>=0&t>=0 & 0<=c&c<1 & v^2<=2*g*(H-h) & H>=0 -> \[ /* system dynamics */ ( {h'=v,v'=-g,t'=1, h>=0}; /* falling/jumping */ if (t>0 & h=0) then /* if on ground */ v := -c*v; /* bounce back */ t := 0 fi. )* /* repeat these transitions */ \] (0<=h & h<=H) /* safety / postcondition */ ) } |
 |
Structure of KeYmaera Problem Specification File
A .key input file for KeYmaera specifies both the operational model of your hybrid system (using the notation of hybrid programs) and the correctness property that you want to verify. The verification problem is specified in a block called \problem {...} that contains the problem description. This block contains a single formula of differential dynamic logic (dL). For instance, this formula can characterise the initial state of the system using implications, the operational system specification using hybrid programs, and the safety/liveness/reactivity/controllability properties to show using modalities.
General Philosophy
The general guiding principle behind the notation of hybrid programs is to be able to describe hybrid systems in a language that is a close extension of standard discrete programming languages. Then the discrete parts are easy to implement while the differential equations describe the dynamics of the physical system you want to control.
Variables do not just change on their own unless you explicitly tell them to using an assignment x:=t or differential equation like x'=5-a. If you specifically want a variable to change arbitrarily you can use x:=* random assignments as needed.
Hybrid Program Notation for Hybrid Systems
In KeYmaera, the behaviour of hybrid systems can be specified easily in a program notation called hybrid programs. In| Hybrid programs, with typical names α and β, are defined by the following syntax | ||
| α ::= | α; β | Sequential composition that does α first and then β |
| x:=t | Discrete assignment/jump assigning the value of t to x | |
| x:=* | Random assignment assigns any real value to x, non-deterministically | |
| if(F) then α fi | If-then statement, performs α if F holds and does nothing otherwise | |
| if(F) then α else β fi | If-then-else statement, performs α if F holds and performs β otherwise | |
| ?F | State assertion testing whether formula F is true in current state (otherwise abort) | |
| α ++ β | Non-deterministic choice following either α or β | |
| while(F) α end | While loop, repeats α as long as F holds, stops before doing α only if F is false (α will not be stopped in the middle just because F becomes false at some intermediate state during α). | |
| α* | Non-deterministic repetition, repeating α arbitrarily often including 0 times | |
| {x'=t,y'=s, F} | Continuous evolution along differential equation system with terms t,s, optionally with domain of maximum evolution or invariant region F.
This domain constraint F needs to be true |
|
| {x'=t,y'<=s,y'>=r, F} | Continuous evolution along system of differential equations and differential inequalities with terms t,s,r, optionally with domain of maximum evolution or invariant region F. The time-derivative of y needs to stay within r and s all the time. | |
| {\exists R u; (x'=t & y'=s & F)} | Continuous evolution along system of differential-algebraic equations with disturbance u (which may occur in the terms t,s and formula F), optionally with domain of maximum evolution or invariant region F. | |
| R x | Variable declaration, declaring x as a real variable (either a state variable or auxiliary variable) | |
| R x, y, z | Variable declaration, declaring x, y, and z as real variables | |
| where F is a formula of (possibly non-linear) real arithmetic (possibly including quantifiers). | ||
Formula Notation for Properties of Hybrid Systems
In KeYmaera, the safety/liveness/reactivity/controllability properties that you are interested in can be specified using formulas of differential dynamic logic. In these formulas, the actual hybrid system to consider can be embedded easily as a hybrid program. In| Formulas of dL, with typical names φ and ψ, are defined by the following syntax | ||
| φ ::= | \forall R x; φ | Universal quantifier: for all real values of x, formula φ holds |
| \exists R x; φ | Existential quantifier: for some real value of x, formula φ holds | |
| !φ | Negation (not) | |
| φ & ψ | Conjunction (and) | |
| φ | ψ | Disjunction (or) | |
| φ -> ψ | Implication (implication) | |
| φ <-> ψ | Biimplication (equivalence) | |
| \[α\] φ | After all runs of hybrid program α, formula φ holds (safety) | |
| \<α\> φ | There is at least one run of hybrid program α, after which formula φ holds (liveness) | |
| pred | Real arithmetic predicate expression | |
| Real arithmetic predicate expressions are defined by the following syntax | ||
| pred ::= | t > s | Greater than |
| t >= s | Greater equals | |
| t = s | Equals | |
| t != s | Not equal | |
| t <= s | Less equals | |
| t < s | Less than | |
| Real arithmetic terms, with typical names s and t, are defined by the following syntax | ||
| t ::= | t + s | Addition |
| t - s | Subtraction | |
| t * s | Multiplication | |
| t / s | Division | |
| t^s | Power | |
| - s | Minus | |
| f(t1,...,tn) | Function application | |
| VARIABLE | An arbitrary variable identifier | |
| NUMBER | An arbitrary rational number | |
Additional Function Symbols
Before the \problem-block of a problem specification file, you can declare auxiliary functions that you intend to use in the system specification. This block is called \functions {...} and contains definitions of function symbols used in the system specification. The functions are declared using their return type, name and argument types. Use, e.g., R f(R,R); to declare a function f of type reals with two real-valued arguments. Or use R c; to declare a real-valued constant function with no arguments.
\functions { R f(R,R); R c; R g(R); R mindistance; }Note that these are logical function symbols. Some function symbols have a special meaning.
Representing Hybrid Automata as Hybrid Programs
In much the same way as finite automata can be written as programs or timed automata can be represented as real-time programs, Hybrid automata can be represented naturally as hybrid programs. Hybrid programs essentially correspond to a program rendition of hybrid automata.
The following simple example corresponds to a water tank, which regulates water level y between 1 and 12 by filling or emptying the water tank.
 |
 |
\problem { /* state variable declarations */ \[ R y, x, st; x:=0; y:=1; st:=0 \] ( st = 0 /* initial state characterization */ -> \[ /* system dynamics */ ( /* repeat the following discrete or continuous transitions */ (?(st=0); (?(y=10); x:=0; st:=1) ++ {x'=1,y'=1, y<=10} ) ++ (?(st=1); (?(x=2); st:=2) ++ {x'=1,y'=1, x<=2} ) ++ (?(st=2); (?(y=5); x:=0; st:=3) ++ {x'=1,y'=-2, y>=5} ) ++ (?(st=3); (?(x=2); st:=0) ++ {x'=1,y'=-2, x<=2} ) )*@invariant(1<=y & y<=12 & (st=3 -> (y>=5-2*x)) & (st=1 -> (y<=10+x))) \] (1<=y & y<=12) /* safety / postcondition */ ) }
You do not need to specify the @invariant-annotation for the loop in advance. But it is easier to start exploring KeYmaera with an example that already contains annotations. Be advised that we encourage the development of systems directly in terms of hybrid programs. This exploits the notational power and often gives much more natural system descriptions than formal translation. This improved representational power of hybrid programs also helps verification.
When you want to avoid encoding state/mode information as numbers, you can also use the following pattern to declare mnemonic constants:\problem { /* state variable declarations */ \[ R y, x, st; x:=0; y:=1; R fill, stop, drain, start; fill:=0; stop:=1; drain:=2; start:=3; st:=fill \] ( st = fill /* initial state characterization */ -> \[ /* system dynamics */ ( /* repeat the following discrete or continuous transitions */ (?(st=fill); (?(y=10); x:=0; st:=stop) ++ {x'=1,y'=1, y<=10} ) ++ (?(st=stop); (?(x=2); st:=drain) ++ {x'=1,y'=1, x<=2} ) ++ (?(st=drain); (?(y=5); x:=0; st:=start) ++ {x'=1,y'=-2, y>=5} ) ++ (?(st=start); (?(x=2); st:=fill) ++ {x'=1,y'=-2, x<=2} ) )*@invariant(1<=y & y<=12 & (st=start -> (y>=5-2*x)) & (st=stop -> (y<=10+x))) \] (1<=y & y<=12) /* safety / postcondition */ ) }
KeYmaera Prover Usage, Verification, and Automation
For proving the specified properties of the hybrid system run KeYmaera,
load the problem specification file and press the play button to verify it.
In addition, you can apply the Find Counterexample rule to find if there is a counterexample for the property and display it.
Furthermore, you can select proof rules from the context menu in case the automatic strategy stops.
If you want KeYmaera to prove your examples automatically, select
auto for the Differential Saturation option in the
Hybrid Strategy tab before you click on start prover.
If you prefer to work more interactively, select off instead, which can help you understand the working principle of KeYmaera better. When you run the prover with Differential Saturation switched off, KeYmaera will stop and ask you which way to go when it is unsure. Turning the automatic Differential Saturation procedure off or selecting simple can also help you verify examples that are beyond the capabilities of today's arithmetic solvers.
Prover Settings and Arithmetic
KeYmaera supports several different settings and real arithmetic procedures. You have multiple options to choose from in the real arithmetic solver options of the Hybrid Strategy tab. You can also control using built-in arithmetic and built-in inequalities if you want to enable internal handling of arithmetic or use the back-end arithmetic directly.
Depending on the number of tools you have configured, you several options for handling arithmetic:
- Built-in Arithmetic
- Mathematica
- Reduce/Redlog
- QEPCAD B or QEPCAD B for Mac
- HOL Light
- Cohen-Hörmander Quantifier Elimination
- Gröbner Bases (built-in)
- Semi-definite Programming for the Positivstellensatz using CSDP
- Semi-definite Programming for the Real Nullstellensatz [5] using CSDP
More Information
For more usage information please have a look at the KeYmaera slides, the slides for differential dynamic logic, the KeYmaera Tool Paper, related publications. In particular, publications about KeYmaera case studies [2][4][1][3] can be useful to understand how complicated systems and complicated properties can be verified with KeYmaera. Answers to typical questions can be found in the FAQ
You can also read the extensive documentation for the underlying KeY system in the KeY-Book, or at the KeY tutorials.
Selected Publications
-
André Platzer and Jan-David Quesel.
European Train Control System: A Case Study in Formal Verification.
Reports of SFB/TR 14 AVACS 54, 2009. ISSN: 1860-9821, www.avacs.org.
[bib | pdf | study]
-
André Platzer and Jan-David Quesel.
European Train Control System: A case study in formal verification.
In Karin Breitman and Ana Cavalcanti, editors, 11th International Conference on Formal Engineering Methods, ICFEM, Rio de Janeiro, Brasil, Proceedings, volume 5885 of LNCS, pages 246-265. Springer, 2009. (c) Springer Verlag
[bib | pdf | doi | slides | study]
-
André Platzer and Edmund M. Clarke.
Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study.
School of Computer Science, Carnegie Mellon University, CMU-CS-09-147, 2009.
[bib | pdf | study]
-
André Platzer and Edmund M. Clarke.
Formal verification of curved flight collision avoidance maneuvers: A case study.
In Ana Cavalcanti and Dennis Dams, editors, 16th International Symposium on Formal Methods, FM, Eindhoven, Netherlands, Proceedings, volume 5850 of LNCS, pages 547-562. Springer, 2009. (c) Springer Verlag
This paper was awarded the FM Best Paper Award.
[bib | pdf | doi | slides]
-
André Platzer, Jan-David Quesel, and Philipp Rümmer.
Real world verification.
In Renate A. Schmidt, editor, International Conference on Automated Deduction, CADE'09, Montreal, Canada, Proceedings, volume 5663 of LNCS, pages 485-501. Springer, 2009. (c) Springer Verlag
[bib | pdf | doi]
-
André Platzer and Edmund M. Clarke.
Computing differential invariants of hybrid systems as fixedpoints.
Formal Methods in System Design, 35(1), pages 98-120, 2009. (c) Springer Verlag
[bib | pdf | doi]
-
André Platzer and Jan-David Quesel.
KeYmaera: A hybrid theorem prover for hybrid systems.
In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pages 171-178. Springer, 2008. (c) Springer Verlag
[bib | pdf | doi | slides]
-
André Platzer and Edmund M. Clarke.
Computing differential invariants of hybrid systems as fixedpoints.
In Aarti Gupta and Sharad Malik, editors, Computer Aided Verification, CAV 2008, Princeton, USA, Proceedings, volume 5123 of LNCS, pages 176-189, Springer, 2008. (c) Springer Verlag
[bib | pdf | doi]
-
André Platzer and Edmund M. Clarke.
Computing Differential Invariants of Hybrid Systems as Fixedpoints.
School of Computer Science, Carnegie Mellon University, CMU-CS-08-103, Feb, 2008.
[bib | pdf]
-
André Platzer and Jan-David Quesel.
Logical verification and systematic parametric analysis in train control.
In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, 11th International Conference, HSCC 2008, St. Louis, USA, Proceedings, volume 4981 of LNCS, pages 646-649. Springer, 2008. (c) Springer Verlag
[bib | pdf | doi]
-
André Platzer.
Differential-algebraic dynamic logic for differential-algebraic programs.
Journal of Logic and Computation, 20(1), pages 309-352, 2010. Advance Access published on November 18, 2008 by Oxford University Press.
[bib | pdf | doi]
-
André Platzer.
Differential dynamic logic for hybrid systems.
Journal of Automated Reasoning, 41(2), pages 143-189, 2008. (c) Springer Verlag
[bib | pdf | doi]
-
André Platzer.
Combining deduction and algebraic constraints for hybrid system analysis.
In Bernhard Beckert, editor, 4th International Verification Workshop, VERIFY'07, Workshop at Conference on Automated Deduction (CADE), Bremen, Germany, CEUR Workshop Proceedings, 259:164-178, 2007.
[bib | pdf]
-
André Platzer.
Differential dynamic logic for verifying parametric hybrid systems.
In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings, volume 4548 of LNCS, pages 216-232. Springer, 2007. (c) Springer Verlag
This paper was awarded the TABLEAUX Best Paper Award.
[bib | pdf | doi | slides]
-
André Platzer.
A temporal dynamic logic for verifying hybrid system invariants.
In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings, volume 4514 of LNCS, pages 457-471. Springer, 2007. (c) Springer Verlag
[bib | pdf | doi | slides]
-
André Platzer.
Differential logic for reasoning about hybrid systems.
In Alberto Bemporad, Antonio Bicchi, and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pages 746-749. Springer, 2007. (c) Springer Verlag
[bib | pdf | doi]