Test a Lustre program with Lurette

This Tiny Tutorial shows a basic usage of lurette to test a Lustre program.

The Lurette Methodology

The design of the system, its oracles, and its stimulus generators is not a linear process. Several iterations are necessary, that are described below, and outlined in The below

Refining the SUT: When an oracle is violated, it can be, of course, because of a design or coding error, which results in a erroneous SUT. Detecting such incorrect behaviors of the SUT is indeed the original motivation of all this infrastructure.

Refining oracles: An oracle violation can also be due to a wrong formalization. Despite the fact that sequence recognizers (oracles) are much simpler to develop than sequence generators (SUT), they are still the result of a human work and thus exposed to errors.

Refining ambiguous requirements: Lurette can also detect ambiguous requirements, when they are interpreted differently by the SUT and the oracle designers. It happened quite frequently during the project.

Refining inconsistent requirements: Formalizing requirements in a language such as Lustre that is equipped with a model-checker allows to detect inconsistencies, i.e., the absence of correct behaviors.

Refining imprecise requirements: Another reason that results in invalidated oracles is when they are based on imprecise requirements. One typical case encountered in the project was a requirement formulated as follows: ``when x exceeds the threshold t, the alarm a should be raised”. In a distributed system like the one of COMON, where sub-systems communicate over buses and networks, such a requirement will be immediately violated if interpreted literally. One should permit some reaction delay, and specify its bounds.

Refining incomplete requirements: Another very common source of oracle violations is a lack of completeness. A typical example, also encountered during the project, is a requirement that states that ``the temperature of tank t should never exceeds 100 degrees”, whereas the correct requirement was ``the temperature of tank t should never exceeds 100 degrees when the system is in the nominal mode and the validity bit associated to its sensor is 1”.

One outcome of the project is that the Lurette tool and methodology was actually helpful for debugging and refining requirements.

Refining scenarios: When the coverage is not complete, we must enrich the set of possible behaviors of the environment with new scenarios. Note that new scenarios may lead to properties violations, which lead to changes in the SUT (or in oracles); and changes in the SUT may change the coverage in turn.

xxx

node idiot (t:bool) returns(x,y:real) =
     assert x = 10. in
     run x,y := ivrogne(20., 20., 20., 20., 0., 100., 0., 200.)

node simu (t:bool) returns(x,y:real) =
     run x,y := ivrogne(2., 2., 2., 2., 0., 100., 0., 200.)

node rabbit_speed (low, high:real) returns (Speed: real) =
   exist Delta, SpeedLow, SpeedHigh: real in
   let draw_params() =
      between(Delta, 0.5, 1.0) and
      between(SpeedLow, 0.0, low) and between(SpeedHigh, 1.0, high)
    in
    let keep_params() =
       (Delta = pre Delta) and (SpeedLow = pre SpeedLow) and
       (SpeedHigh = pre SpeedHigh)
    in
       {
          &> loop { draw_params() fby loop ~100: 10 { keep_params() } }
          &> Speed = 1.0 fby
             run Speed := up_and_down(pre SpeedLow, pre SpeedHigh, pre Delta)
       }
extern sin(x:  real) : real
extern cos(x:  real) : real