Development Tools for Critical Reactive Systems
using the Synchronous Approach
The Verimag Reactive Tool Box

Several development tools targeting the design of reactive programs (typically, for critical embedded systems) are made available by the synchronous team of the Verimag laboratory.

The objective of this document is to describe briefly how to install and to use them. This tools set contains tools to

• Execute Lustre V6 programs
• Execute Lutin programs
• Luciole-rif eases the simulation of programs that reads/writes RIF using TK GUIs
• Lurette is a tool that automate the black-box testing of Reactive programs (e.g., written in Lustre)
• rdbg can help to debug Lustre V6 or Lutin programs
• Lustre, Lutin, lurette, rdbg, and otherscn produce RIF Data files, that can be visualised with
  • sim2chro
  • or gnuplot-rif
• Lesar can formally verify (model-check) temporal program properties written in Lustre.

There are 4 different tools suites containing Verimag Synchronous tools.

1. docker: based on a docker image. It requires docker.
2. V4 binaries : made of pre-compiled binaries gathered in a tarball. It requires to change your environment variables (PATH, LUSTRE_INSTALL, etc.)
3. V6 binaries: ditto
4. V6 via opam: integrated in the opam (ocaml) package manager. It requires opam 2.

5. From sources. The gitlab projects hosting the different tools are accessible from: https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone

   Not all suites contain all tools, as outlined in the table below:

(*) "V4 essentials" is a sub-set of "V4 full", containing the V4 tools that are really useful to use the V6 tool-set (luciole, gnuplot-rif, sim2chro, etc.).

Hence, to get the complete set of tools, you need to use the docker distribution, or both the "V4 binaries"+the "V6 via opam" ones. As far as OSes are concerned:

(**) For mac users, to be able to use X11-based tools (luciole, gnuplot-rif, sim2chro, etc.) it is necessary to

• install xquartz: brew cask install xquartz
• start it (click in Finder -> Applications)
• open XQuartz -> Preferences from the menu bar. Go to the last tab, Security, and enable both "Allow connections from network clients" and "Authenticate connections" checkboxes and restart XQuartz.

(*) for windows users, in order to use the docker version via wsl, you still need to install an X server, for instance using mobaxterm.

The Lustre V6 language is described in the Lustre V6 Reference Manual. Here we focus on tools.

Some programs can be found in a dedicated github repo: https://github.com/jahierwan/lustre-examples

Consider the lutin/range.lut Lutin program:

node range(i:int) returns (y:int) = 
   loop 0 <= y and y <= i

In order to simulate this program, on can use one of the following commands:

lutin range.lut 
lutin range.lut -n range
luciole-rif lutin range.lut 

Here again, the focus is on the basic use of tools, not on the language. More information can be found in this Lutin Tutorial.

More on Lutin

RIF stands for Reactive Input Format. It is the format used between the V4 and the V6 distributions tools to read inputs and write outputs. If you simulate a Lustre (V4 or V6), a Lutin program, or if you use lurette or rdbg, all tools will produce .rif files which follows the RIF conventions.

RIF Data files, that can be visualised with sim2chro or gnuplot-rif.

In order to graphically display RIF data files via chronograms, you can use sim2chro or sim2chrogtk

sim2chro    -ecran -in edge.rif > /dev/null
sim2chrogtk -ecran -in edge.rif > /dev/null

For more information: sim2chro -help

sim2chro -help

nb : sim2chro and sim2chrogtk are part of the V4 tool set distribution

In order or graphically display RIF data files, one can also used gnuplot-rif, that basically pre-process RIF to feed gnuplot:

gnuplot-rif edge.rif

It is possible to hide the display of some variables, using command-line options, or using the .gnuplot-rif resource file.

For more information:

gnuplot-rif -h

luciole-rif generates little TK-based GUIs. Such GUIs allow one to provide input and visualize outputs graphically. luciole-rif can be used with all tools that follows the RIF conventions, such as the Lustre V6 interpreter:

luciole-rif lv6 edge.lus -node edge -exec

The executable produced via C also speaks RIF:

lv6 edge.lus -node edge -2c -cc -o edge
luciole-rif ./edge.exec --debug-me

The Lutin interpreter too:

luciole-rif lutin range.lut 

Try luciole-rif -h more information.

luciole-rif is a wrapper around luciole, which is part of V4 tool set distribution.

-- f.lus
node a_node (X: bool) returns (RE: bool);
let
 RE = false -> X and not pre(X);
tel;
node some_prop(X,RE:bool) returns (res:bool);
let
  res = true -> (pre(RE) => not(RE)) and (RE => not(pre(RE)));
tel

-- env.lut
node an_env () returns (X: bool) = loop true 

In order to test (during 100 steps) a Lustre node defined in file f.lus (called hereafter the sut, for system under test), against properties defined in the Lustre node some_prop (called hereafter the oracle), and using an environment for N defined by the Lutin node an_env defined in file env.lut (called the environment), one can use lurette as follows:

lurette -sut "lv6 f.lus -n a_node" -env "lutin env.lut -n an_env" \
     -oracle "lv6 f.lus -n some_prop" -l 100

Before running the test, lurette will check that:

• The set of sut inputs names is included in the set of env outputs names
• The set of env inputs names is included in the set of sut outputs names
• The set of oracle inputs names is included in the set of sut and env outputs names

Note that several sut/env/oracle can be used. Any system call that follows the RIF conventions can be used as arguments of -sut, -env, and -oracle.

lurette is actually (now) an alias for rdbg -lurette ; more information can therefore be obtained via rdbg -h.

More on Lurette and automatic testing of Reactive Programs

If you want to debug the Lustre node N of file f.lus, you can try to do:

rdbg -sut "lv6 f.lus -n a_node"

If an environnement exists for this node on the form of a Lutin program env.lut with node N_env, you can try:

rdbg -sut "lv6 f.lus -n a_node" -env "lutin env.lut -n an_env"

If you want rdbg to skip what occurs in the Lutin program, you can use -env-nd instead -env (-nd stands for no debug):

rdbg -sut "lv6 f.lus -n a_node" -env-nd "lutin env.lut -n an_env"

If you have found a bug using Lurette, you can call the rdbg debugger just like you called Lurette: just replace lurette by rdbg. Note that the oracle can be debugged too. In the following call, only the oracle will be stepped into:

rdbg -sut-nd "lv6 f.lus -n a_node" \
     -env-nd "lutin env.lut -n an_env" \
     -oracle "lv6 f.lus -n some_prop"

More information on rdbg

Lesar is a model-checker of temporal program properties written in Lustre. It is distributed with the V4 tool set (it is also part of the V6 pre-compiled distribution and the docker image). In order to model-check Lustre V6 programs properties, one first needs to translate it into ec or Lustre V4.

-- f.lus
node a_node_satisfy_some_prop (x: bool) returns (res: bool);
var y : bool;
let
   assert(some_prop_on_inputs(x));
   y = a_node(x);
   res = some_prop(x,y);
tel;
node some_prop_on_inputs(x: bool) returns (res: bool);
let
  res = x -> true; -- true at the first instant
tel

lv6 f.lus -n a_node_satisfy_some_prop -lv4 -o prove_me.lus
lesar  prove_me.lus f__a_node_satisfy_some_prop

lesar actually uses the V4 compiler under the hood to generate an .ec file, which is given to ecverif, which performs the real work.

A different path consists of generating an .ec file with lv6 -ec, and to give the resulting file to ecverif:

lv6 f.lus -n a_node_satisfy_some_prop -ec -o prop.ec
ecverif prop.ec

nb: if you want to prove properties that involve programs with enums, you might want to try the experimental -eeb (–expand-enums-as-bool) option of lv6.

More information on Lesar is available Here.

Note that the kind2 SMT-based model-checker, which works on most Lustre V4 and V6 programs, is worth giving a try if your property involves numeric variables.