Verifying LUSTRE programs: lus2nbac

Verifying LUSTRE programs: lus2nbac

The main use of NBac has been the verification of programs written in the dataflow synchronous language Lustre. We assume some basic knowledge about Lustre, available at its homepage, and just describe the translation process.

We take an example from [10]. We consider a (simplified) compact-disk controller, connected to a motor as shown by the figure below.

The motor reacts to two logical signals, plus and minus, which make it run faster or slower, respectively. When neither of these two signals is on, the speed varies within two bounds (here, -4 and +4). A sensor gives the current speed. The controller tries to maintain the motor speed within a specified range (here [8,12]), by sending appropriate signals plus and minus. Whenever the speed has been outside the range for a given delay (here, 15), counted as a number of steps, the ok signal becomes false.

This gives the following Lustre program:

node Environment(diff: int; plus,minus: bool) returns (ok: bool);
  ok = (-4 <= diff and diff <= 4) and
     (if (true -> pre plus) then diff >= 1 else true) and
     (if (false -> pre minus) then diff <= -1 else true);

node Controller(diff: int) returns (speed: int; plus,minus: bool);
  speed = 0 -> pre(speed)+diff;
  plus = speed <= 9;
  minus = speed >= 11;

node Property(speed: int) returns (ok: bool);
var cpt: int;
    acceptable: bool;
  acceptable = 8 <= speed and speed <= 12;
  cpt = 0 -> if acceptable then 0 else pre(cpt)+1;
  ok = true -> (pre cpt<=7);

node lector(diff:int) returns
	ok: bool;
	speed: int;
	plus,minus,realistic: bool;
  (speed,plus,minus) = Controller(diff);
  realistic =  Environment(diff,plus,minus);
  ok = Property(speed);

We want to verify that the ok signal is always emitted. This means that, if the speed is initially 0, it must reach the correct range in time, and be properly controlled afterwards.

We type

lus2nbac cd.lus lector

which generate a file (the executable lus2nbac is available at the download section). lus2nbac takes two arguments: the Lustre programs, and the main node, supposed to be a property observer, that is, a node observing the program and returning one Boolean output (if there is several outputs, the first Boolean output is chosen as a definition of the property). It generates a NBac file with initial and final conditions, as well as an assertion. The initial condition is the initial state of the Lustre program, and the final condition describes the set of states from which a false Boolean output may be emitted by the property observer, that is, the set of states violating the property. In addition, lus2nbac slices the program in order to select only the relevant part for the property, and performs some static analysis.

Now, the property may be checked with

nbacg -dot " +all"

which dumps a DOT file, which gives after conversion to Postscript, and outputs these messages:

Forward analysis (..)  Backward analysis (.)
***** creating initial partition *****
*** initial analysis ***

***** heuristic refinement *****
*** Conclusion ***
4 fixpoint analysis, 0+2 refinements, 0+2 divisions
Total time spent in verification : 0.64 sec
  Part of it spent in partition build      : 0.03 sec
  Part of it spent in analysis             : 0.30 sec
  Part of it spent in division heuristics  : 0.12 sec
  Part of it spent in partition refinement : 0.10 sec
Total time spent in post-pre-conditions : 0.53 sec
  assertion : 0.20 sec;
  apply     : 0.33 sec
SUCCESS: property proved
*** END ***

Bertrand Jeannet, February 10, 2011

Verifying LUSTRE programs: lus2nbac