Tutorial for the KeYmaera Verification Tool for Hybrid Systems

Using the KeYmaera Prover for Verifying Hybrid Systems

KeYmaera, like KeY, 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 automation strategies to verify the specified property of the hybrid system.

1. Load the .key problem specification file, e.g., simple.key.
2. Run the automatic proof strategies to verify the hybrid system.

• Apply find counterexample rule to see if there is a counterexample for the property, if it cannot be proven.
• Directly select further proof rules from the context menu, e.g., to discover parameter constraints.
• Adjust proof strategy to your needs in the "Hybrid Strategy" tab to determine the behaviour of KeYmaera.
• Select visualization rule to see a graphical view of the transition system.

KeYmaera Problem Specification Files

You can specify the verification problem by loading a .key problem specification file. This file contains a formula of differential dynamic logic (dL) specifying both the operational model of your hybrid system and the correctness property that you want to verify.

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 -> \[ ( 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) ) }

This example contains typical idioms for specifying correctness properties and hybrid systems in KeYmaera:

• 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 postcondition x^2<=(4*c)^2 specifies the safety property that is conjectured to hold for each reachable state.

Structure of Problem Specification File

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). This dL formula can characterise the prestate using implications, the operational system specification using hybrid programs, and the properties to show using modalities. In EBNF syntax this looks as follows:

Representing Hybrid Automata as Hybrid Programs: Example (Water Tank)

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. Each of its lines correspond to the discrete or continuous transitions of the water tank hybrid automaton.

  \problem {
    /* state variable declarations */
    \[ R y, x, st; x:=0; y:=1; st:=0 \] (
     st = 0  /* initial state characterization */
   ->
     \[
       ( /* 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)
   )
  }
  

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.

Additional Function Symbols

Before the problem-block, 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;
}

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 or the Options->KeYmaera Options menu 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 verifying examples that are beyond the capabilities of today's arithmetic solvers.

More Information

For more usage information please have a look at related publications, the KeY-Book, or at the KeY tutorials.