Development Tools for Critical Reactive Systems
using the Synchronous Approach
The Verimag Reactive Tool Box
Author | Erwan Jahier |
Date | 2020-06-23 10:57 |
1 Introduction
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 - Lesar can formally verify (model-check) temporal program properties written in Lustre.
2 Install
There are 4 different tools suites containing Verimag Synchronous tools.
- docker: based on a docker image. It requires docker.
- V4 binaries : made of pre-compiled binaries gathered in a tarball. It
requires to change your environment variables (
PATH
,LUSTRE_INSTALL
, etc.) - V6 binaries: ditto
- V6 via opam: integrated in the opam (ocaml) package manager. It requires opam 2.
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:
tools \ distributions | 2 docker 2 | 2 V4 binaries 2 | 2 V6 binaries 2 | 2 V6 via opam/sources 2 |
---|---|---|---|---|
V4 essentials (*) | X | X | X | |
V4 full (*) | X | X | ||
lv6 |
X | X | X | |
lutin |
X | X | X | |
sim2chro |
X | X | X | |
gnuplot-rif |
X | X | X | |
luciole-rif |
X | X | ||
lurette |
X | X | X | |
rdbg |
X | X | ||
lesar |
X | X | X |
(*) "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:
OS \ distributions | 2 docker 2 | 2 V4 binaries 2 | 2 V6 binaries 2 | 2 V6 via opam 2 |
---|---|---|---|---|
linux | X | X | X | X |
mac os (**) | X | X | ||
windows | X (via a VM) |
(**) 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.
2.1 The V4 and V6 tools suite via docker
One way to install those tools is via docker. Once docker is installed with X display properly settled (which can sometimes be cumbersome. For mac users using a recent distribution (2018), having X windows working correctly is a bit painful. Here a useful link: https://stackoverflow.com/questions/37826094/xt-error-cant-open-display-if-using-default-display), installing the distribution is super easy.
You first need to launch docker
with the
jahierwan/verimag-sync-tools
image, that is available on the docker hub:
docker run -it jahierwan/verimag-sync-tools
The first time, it will download the verimag-sync-tools
docker image
on the docker hub. Then you will be logged onto a docker machine
where all tools are available from the path.
It is very handy to mount your current (host) directory onto some
/workdir
in the docker image adding something that looks like: -v
"$PWD":/workdir -w /workdir --user `id -u`
to the docker
call.
Also, if you want to use tools that make use of graphics (sim2chro
,
gnuplot-rif
, luciole-rif
), one can use the following option: -e
DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix
.
All together, you can therefore use the following command:
docker run -v "$PWD":/workdir -w /workdir \ -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix \ -it jahierwan/verimag-sync-tools
It is might be easier to have a sh/dockver script accessible from your path and defined as follows:
unameOut="$(uname -s)" case "${unameOut}" in Darwin*) DISPLAY=host.docker.internal:0 ;; esac docker run --user `id -u` -v "$PWD":/workdir -w /workdir \ -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix \ -it jahierwan/verimag-sync-tools $@
Such a script can be used like that:
chmod u+x dockver # to do once ./dockver
to open an interactive session.
Once can also use the binaries provided in this image directly like that:
./dockver lutin -l 10 some_file.lut -o some_trace.rif ./dockver gnuplot-rif some_trace.rif
to remain into your CLI context.
nb: this image embeds an emacs with Lustre and Lutin mode installed:
./dockver emacs somefile.lus
Putting this script somewhere accessible from your PATH
migth be
convenient too.
2.2 The V4 tools suite via pre-compiled binaries
The V6 tool suite actually (partly) depends on the Lustre V4 tool suite, that therefore needs to be installed too. Binary distributions of the The Lustre V4 for Linux and Mac can be found here:
http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html
The Lustre V4 tool set is described in the Lustre V4 Documentation.
2.3 The V6 tools suite via pre-compiled binaries
One can install the V6 distribution via Pre-compiled binaries can be found there : http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/pre-compiled/
wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/pre-compiled/`arch`-`uname`-lv6-bin-dist.tgz tar xvfz `arch`-`uname`-lv6-bin-dist.tgz export LV6_PATH=`pwd`/lv6-bin-dist/ . ./v6-tools.sh
nb: if you need to
- use the
rdbg
debugger - call lutin or lustre from ocaml
2.4 The V6 tools suite via opam 2
One way to install the V6 distribution is via opam, a package manager for ocaml programs. It should work out of the box with most Linux distributions and OSX (mac). It ougth to work on windows too (follow this link for instructions).
For instance, on ubuntu, installing opam just requires (intructions for other arch):
apt-get update apt-get install -y m4 make ocaml ocaml-native-compilers camlp4-extra wget patch unzip bubblewrap git g++ wget https://github.com/ocaml/opam/releases/download/2.0.5/opam-2.0.5-x86_64-linux -O /usr/bin/opam chmod a+x /usr/bin/opam opam init -y --jobs=1 --disable-sandboxing eval $(opam env) opam switch create 4.09.0 ; eval $(opam env) # optional, just to have a recent ocaml cp /usr/bin/opam opam/4.09.0/bin/ opam install -y opam-depext
In order to obtain the very last version, one can add the verimag opam repo.
# optional opam repo add verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository" opam update -y
And then to install the necessary packages:
opam depext -y lustre-v6 lutin opam install -y lustre-v6 lutin
Once is is done, upgrading to the last version of the tools is as simple as:
opam update opam upgrade
3 Lustre V6
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
3.1 Compiling Lustre V6 programs
The Lustre V6 compiler is named lv6
. By default,
lv6
produces lic
code out of a .lus
file (hence its name).
lic
stands for "Lustre Internal Code". Basically, lic
is Lustre
V6 with all genericity and syntactic suggar removed.
Consider the content of the edge.lus
file:
node edge (X: bool) returns (Y: bool); let Y = r_edge(X) or r_edge(not(X)); tel node r_edge (X: bool) returns (Y: bool); let Y = false -> X and not pre(X); tel
It is a Lustre program that detects (rising or falling) edges of a
Boolean stream. If one wants to generate lic
out of this Lustre
program, one just need to invoke:
lv6 edge.lus -lic -n edge
Note that the -node
option (or -n
for short), that sets the
top-level node, is now mandatory.
lv6 edge.lus -node edge lv6 edge.lus -n r_edge
Generate lic code is not very useful; generate C code can be done using -2c
:
lv6 edge.lus -n edge -2c
3.2 Executing Lustre V6 programs
The call to lv6 edge.lus -node edge -2c
not only generates C
files: it also generetes a edge.sh
script that can be used to
generate a edge.exec
binary file. The edge.exec
file can be
generated directly via the -cc
(--compile-generated-c
) option.
lv6 edge.lus -node edge -2c -cc ./edge.exec
It is also possible to use the interpreter that is embedded in
lv6
via the -exec
option.
rm -f edge.rif lv6 edge.lus -node edge -exec -o edge.rif
In both cases, input data needs to be provided via the keyboard. It
is also possible to use a tcl/tk based GUI via luciole-rif
:
luciole-rif lv6 edge.lus -node edge -exec lv6 edge.lus -node edge -2c -cc; luciole-rif ./edge.exec
nb: luciole-rif
- requires the V4 tool set installation.
- can be used with all tools that follow the RIF conventions
(
luciole-rif -h
for more information).
3.3 Using the V4 tool set
It is often possible to use the V4 tool set to execute and compile V6 programs,
using -lv4
or -ec
:
lv6 edge.lus -node edge -lv4 -o edge_v4.lus lv6 edge.lus -node edge -ec -o edge.ec
And then you should be able to use the V4 tools set:
lus2ec
, ecexe
, ec2c
, ecverif
, etc.
3.4 More
4 Lutin
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.
5 RIF
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.
5.1 Exemple
A RIF file looks like this:
# This is lutin Version 2.26 ("1af0fb6") # The random engine was initialized with the seed 300035711 #inputs "x":int #outputs "y":int #step 1 4 #outs 5 #step 2 5 #outs 6 #step 3 64 #outs 65 #step 4 5 #outs 6 #step 5 4 #outs 5
It basically contains:
- comments (preceeded with #)
- pragmas (particular kinds of comments: '#inputs', '#outputs', '#outs', '#outs', etc.)
- data (int, bool, float)
5.2 The RIF convention (useful for tool providers)
5.2.1 Data
A RIF file is a sequence of data values separated
by spaces, newlines, horizontal tabulations, carriage returns, line
feed and form feeds. A data value can be either an integer, a
floating-point or a Boolean (t
, T
, or 1
stands for
true
; f
, F
or 0
stands for false
).
5.2.2 Comments
Single line comments are introduced by the two character #
and
terminated by a new line. Multi-line comments are introduced by the
two characters #
, and terminated by the two characters #@
.
5.2.3 Pragmas
Pragmas are special kinds of comments, that migth (or not) be taken
into account by tools that reads RIF data. One-line pragmas have the
form #pragma_ident
, and multi-line pragmas the form
#pragma_ident ... #@
.
The most common pragmas used by verimag tools are (using BNF notation):
#@inputs
(<var name>:
<var type>)+#@
or#inputs
(<var name>:
<var type>)+
to declare the list of input variable names and types;
#@outputs
(<var name>:
<var type>)+#@
or#outputs
(<var name>:
<var type>)+to declare the list of output variable names and types;
#@locals
(<var name>:
<var type>)+#@
or#locs
to indicate that the following data correspond to local variables; to declare the list of local variable names and types;
#outs
, to indicate that the following data correspond to output variables;#step
<int>, to indicate that a new step is starting, and that the following data correspond to input variables.
Note that those pragmas are necessary for RIF file viewers such as
sim2chro
and gnuplot-rif
to work properly. Here is another
exemple:
#seed = 97040004 #program "lurette chronogram (degradable-sensors.lut) " #@inputs "T":real "T1":real "T2":real "T3":real @# #@locals "degradable-sensors__cpt":int "degradable-sensors__eps":real "degradable-sensors__eps1":real "degradable-sensors__eps2":real "degradable-sensors__eps3":real @# #@outputs "Heat_on":bool @# #step 1 7.00 7.00 7.00 7.00 #outs T #locs 0 0.08 -0.05 -0.05 0.10 #step 2 7.13 7.20 7.16 7.18 #outs T #locs 1 0.13 0.07 0.03 0.05 #step 3 7.27 7.37 7.27 7.18 #outs T #locs 2 0.14 0.10 -0.00 -0.09 #step 4 7.45 7.47 7.38 7.36 #outs T #locs 3 0.18 0.02 -0.07 -0.09 #step 5 7.59 7.68 7.61 7.56 #outs T #locs 4 0.14 0.09 0.02 -0.03 #step 6 7.65 7.58 7.64 7.55 #outs T #locs 5 0.06 -0.06 -0.01 -0.09 #step 7 7.84 7.91 7.94 7.90 #outs T #locs 6 0.20 0.07 0.10 0.06 #step 8 8.00 8.07 8.00 8.09 #outs T #locs 7 0.15 0.07 0.00 0.09 #step 9 8.12 8.09 8.17 8.16 #outs T #locs 8 0.13 -0.03 0.05 0.04 #step 10 8.26 8.29 8.30 8.20 #outs T
6 sim2chro
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
7 gnuplot-rif
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
8 luciole-rif
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.
9 lurette
-- 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 environnement 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
.
10 rdbg
If you want to debug the Lustre node N of file f.lus
, you can try
to do:
echo "q\n" | \
If an environnement exists for this node on the form of a Lutin
program env.lut
with node N_env
, you can try:
echo "ni 10\nq\n" | \
If you want rdbg
to skip what occurs in the Lutin program, you can
use -env-nd
instead -env
(-nd
stands for no debug):
echo "ni 10\nq\n" | \
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:
echo "ni 10\nq\n" | \
11 lesar
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 y = a_node(x); res = some_prop(x,y); 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 migth want to try the experimental -eeb (–expand-enums-as-bool)
option of lv6
. Indeed, Lesar
More information on Lesar is available Here.