Lustre is a synchronous dataflow language commonly used to model or implement safety-critical embedded systems. You can have a look at the following resources to learn about the language:
Luke is a tool written by Koen Claessen for simulating and verifying Lustre programs. Luke binaries are available for the following platforms:
To use the Linux, FreeBSD, or Solaris version, the provided file has to be unzipped (using gunzip <filename>), made executable (chmod +x <filename>), and possibly moved to a location present in the PATH variable (like ~/bin).
On Windows computers (e.g., on the computers in lab room 1313), it is enough to download the Luke Windows binary and save it to the directory where your Lustre programs are located. Luke has to be invoked using the Windows command line prompt, using the same command line options as for the Unix versions.
An overview of Luke commands and options can be displayed using:
> luke --help
Simulation of Lustre programs
Given a Lustre program file.lus and a node Node contained in the file (for instance, one of the examples given in the lectures), Luke can generate a simulator in form of a HTML page:
> luke file.lus --node Node
> firefox Luke/Node.html
Static verification of Lustre programs
Luke can also statically verify that programs satisfy safety requirements, using SAT-based model checking and k-induction techniques. Safety requirements are specified by writing synchronous observers, as has been discussed in this lecture; also see the lecture examples.
Luke is invoked as follows to verify the properties specified in a synchronous observer ReqNode:
> luke file.lus --node ReqNode --verify