Lustre (programming language)

Lustre is a synchronous declarative programming language.

Historical development of Lustre

Lustre is as Esterel, originated at the beginning of the 1980s. Again, it was the lack of suitable programming languages ​​and software systems for reactive systems the decisive occasion. With the merger of several French researchers, the " synchronous language school " was born. From the collected proposals from the researcher, one has then opted for Lustre, as this has been the easiest. Lustre was greatly evolved since that time and is now in version V4 with many different tools ( compilers, simulators, test tools, code generators ) available.

Areas of Lustre

Lustre is as reactive systems in general, including in safety-critical systems such as aircraft and power plant control used. For example, the flight control of the Airbus A320, the emergency shutdown of nuclear power plants and the control of driverless metros has been implemented in Lustre. Lustre is used predominantly for programming and control of this type of systems.

Program structure

The program structure in Lustre can be graphically represented as a network of operators. Applications ( nodes ) are also illustrated as separate operators and used according to several times.

In Lustre only a few of the usual types of variables are available, so there is only boolean, integer, real, and tuple. Of the operators are the basic available:

  • Arithmetic operators: - * / div mod
  • Boolean operators: and or not
  • Relational operators: == << = >> =
  • Conditional action: if then else if then else

In addition there are four river operators (temporal operators ) ( pre, ->, when shipped, current). These are used specifically for data flow requests. For example provides the operator " pre" the state of the previous time point of the variable.

The operator " ->" ( Followed by) is used to initialize variables. Such means, for example, " x = 0 -> pre ( X) 1 ," where X is the first point of time 0, and is made with all other, and the previous value incremented by 1.

Below is a simple Lustre code example:

Node A ( b: bool, i: int, x: real) returns ( y: real);        var j: int; z: real;        let j = if b then 0 else i;            z = b (j, x);            if y = b then pre ( z ) else C (z ) <        tel In this example, a handler (node ​​) is described using the name "A". The other procedures "B" and "C" are used as defined elsewhere in the program. "A" is input with three flows initialized (b, i, x ), and outputs a return (y).

Timing in Lustre

The timing of Lustre is probably the main advantage of this language. It is based on a logical and timing is counted in discrete times. However Logical timing says nothing about the length or the time between the individual time points. It is rather, is a reference the values ​​of variables and expressions during the current and / or other timing. New values ​​are always added at the end of the value Esch Lange.

Thus is well defined, which value is valid when.

Compile

The Lustre compiler checks not only the syntax of the program code, but also other important requirements:

  • Definition control: here, it is checked whether each variable was also really defined only once
  • Clock - consistency: all combined expressions and variables must have the same clock base
  • Non -zero values: are allowed only for non- clock - dependent variables and expenses, all others must be initialized.

Verification

The automaton generated by the compiler can then be verified with additional tools ( Lurette, Lucky ). Since Lustre is mainly used for safety-critical systems and which often depend lives that verification is a very important consideration. For example, it is not relevant whether a train ever stops, but rather whether the train stops at a red signal.

535600
de