The information listed on this page refers to the state of the tool in '99. For more recent information, please use the following link:

http://www-verimag.imag.fr/SYNCHRONE/tools.html

LUSTRE - VERIMAG

Name: Lustre toolset

Main Functionalities

This distribution provides tools dedicated to the synchronous dataflow language Lustre :
compilers, simulators and a verification tool (LESAR).

Description

The main tools in the distribution are:

Compilers: a set of tools for producing C code from Lustre programs.
Simulators (interpreters): a ``file to file'' simulator and a graphical simulator (LUCIOLE).
Verification tool: LESAR is dedicated to the formal verification of safety properties on Lustre programs. Both properties and assumptions must be written in Lustre.
Documentation: a tutorial, a manual and a set of examples are provided.

Related papers

"The synchronous dataflow programming language Lustre"
N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud
Proceedings of the IEEE, September 1991

" Programming and verifying critical systems by means of the synchronous data-flow programming language Lustre"
C. Ratel, N. Halbwachs, and P. Raymond
ACM-SIGSOFT'91 Conference on Software for Critical Systems, December 1991

Availability

The Lustre V4 distribution is submitted to a free Licence. For informations and download:

http://www-verimag.imag.fr/SYNCHRONE/

Contact persons : P. Raymond (Pascal.Raymond@imag.fr) or N. Halbwachs (Nicolas.Halbwachs@imag.fr)

Format of the distribution

Binaries and documentation (post-script)

Supported platforms

Sun-Solaris and Intel-Linux platforms.

Input format

Lustre programs

Output format

Ansi-C, ec (Lustre-expanded code), oc (Lustre-Esterel object code)