Lustre resources
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 binaries
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, which will be discussed in the lecture on Monday, 20/2/2012.
Luke is invoked as follows to verify the properties specified in a synchronous observer ReqNode:
> luke file.lus --node ReqNode --verify