Lustre (Programmiersprache)

Lustre ist eine synchrone deklarative Programmiersprache.

Geschichtliche Entstehung von Lustre

Lustre ist, wie Esterel, zu Beginn der 1980er Jahre entstanden. Auch hier war es das Fehlen geeigneter Programmiersprachen und Software-Systeme für reactive systems der ausschlaggebende Anlass. Mit dem Zusammenschluss mehrerer französischer Forscher entstand die „synchrone Sprachen-Schule“. Aus den gesammelten Vorschlägen der Forscher hat man sich dann für Lustre entschieden, da dies der einfachste gewesen ist. Lustre wurde seit dieser Zeit sehr stark weiterentwickelt und ist mittlerweile in der Version V4 mit vielen verschiedenen Tools (Compiler, Simulatoren, Test-Tools, Code-Generatoren) verfügbar.

Einsatzgebiete von Lustre

Lustre wird, wie reaktive Systeme im Allgemeinen, unter anderem in sicherheitskritischen Systemen wie beispielsweise der Flugzeug- und Kraftwerksteuerung verwendet. So wurde beispielsweise die Flugsteuerung im Airbus A320, die Notabschaltung von Kernkraftwerken und die Steuerung von fahrerlosen U-Bahnen in Lustre umgesetzt.<ref name="VERIMAG"><templatestyles src="Webarchiv/styles.css" />{{#if:20061209172339

      | {{#ifeq: 20061209172339 | *
    | Vorlage:Webarchiv/Wartung/Stern{{#if: VERIMAG Research Center | {{#invoke:WLink|getEscapedTitle|VERIMAG Research Center}} | {{#invoke:Webarchiv|getdomain|http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lustre-story%2Fhistory_1}} }} (Archivversionen)
    | {{#iferror: {{#time: j. F Y|20061209172339}}
         | {{#if:  || }}Vorlage:Webarchiv/Wartung/DatumDer Wert des Parameters {{#if: wayback | wayback | Datum }} muss ein gültiger Zeitstempel der Form YYYYMMDDHHMMSS sein!
         | {{#if: VERIMAG Research Center | {{#invoke:WLink|getEscapedTitle|VERIMAG Research Center}} | {{#invoke:Webarchiv|getdomain|http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lustre-story%2Fhistory_1}} }} {{#ifeq:  | [] | [ | ( }}Memento{{#if: {{#if: 2019-04-28 18:06:46 InternetArchiveBot | 2019-04-28 18:06:46 InternetArchiveBot |  }} |  des Vorlage:Referrer }} vom {{#time: j. F Y|20061209172339}} im Internet Archive{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
      }}
  }}
      | {{#if:
          | {{#iferror: {{#time: j. F Y|{{{webciteID}}}}}
    | {{#switch: {{#invoke:Str|len|{{{webciteID}}}}}
       | 16= {{#if: VERIMAG Research Center | {{#invoke:WLink|getEscapedTitle|VERIMAG Research Center}} | {{#invoke:Webarchiv|getdomain|http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lustre-story%2Fhistory_1}} }} {{#ifeq:  | [] | [ | ( }}Memento{{#if: {{#if: 2019-04-28 18:06:46 InternetArchiveBot | 2019-04-28 18:06:46 InternetArchiveBot |  }} |  des Vorlage:Referrer }} vom {{#time: j. F Y| 19700101000000 + {{#expr: floor {{#expr: {{#invoke:Str|sub|{{{webciteID}}}|1|10}}/86400}} }} days}} auf WebCite{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
       | 9 = {{#if: VERIMAG Research Center | {{#invoke:WLink|getEscapedTitle|VERIMAG Research Center}} | {{#invoke:Webarchiv|getdomain|http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lustre-story%2Fhistory_1}} }} {{#ifeq:  | [] | [ | ( }}Memento{{#if: {{#if: 2019-04-28 18:06:46 InternetArchiveBot | 2019-04-28 18:06:46 InternetArchiveBot |  }} |  des Vorlage:Referrer}} vom {{#time: j. F Y| 19700101000000 + {{#expr: floor {{#expr: {{#invoke:Str|sub|{{#invoke:Expr|base62|{{{webciteID}}}}}|1|10}}/86400}} }} days}} auf WebCite{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
       | #default= Der Wert des Parameters {{#if: webciteID | webciteID | ID }} muss entweder ein Zeitstempel der Form YYYYMMDDHHMMSS oder ein Schüsselwert mit 9 Zeichen oder eine 16-stellige Zahl sein!Vorlage:Webarchiv/Wartung/webcitation{{#if:  || }}
      }}
    | c|{{{webciteID}}}}} {{#if: VERIMAG Research Center | {{#invoke:WLink|getEscapedTitle|VERIMAG Research Center}} | {{#invoke:Webarchiv|getdomain|http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lustre-story%2Fhistory_1}} }} (Memento{{#if: {{#if: 2019-04-28 18:06:46 InternetArchiveBot | 2019-04-28 18:06:46 InternetArchiveBot |  }} |  des Vorlage:Referrer}} vom {{#time: j. F Y|{{{webciteID}}}}} auf WebCite{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
  }}
          | {{#if: 
              | Vorlage:Webarchiv/Today
              | {{#if:
                      | Vorlage:Webarchiv/Generisch
                      | {{#if: VERIMAG Research Center | {{#invoke:WLink|getEscapedTitle|VERIMAG Research Center}} | {{#invoke:Webarchiv|getdomain|http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lustre-story%2Fhistory_1}} }}  
                 }}}}}}}}{{#if:2019-04-28 18:06:46 InternetArchiveBot
    | Vorlage:Webarchiv/archiv-bot
  }}{{#invoke:TemplatePar|check
     |all      = url=
     |opt      = text= wayback= webciteID= archive-is= archive-today= archiv-url= archiv-datum= ()= archiv-bot= format= original=
     |cat      = Wikipedia:Vorlagenfehler/Vorlage:Webarchiv
     |errNS    = 0
     |template = Vorlage:Webarchiv
     |format   = *
     |preview  = 1
  }}{{#ifexpr: {{#if:20061209172339|1|0}}{{#if:|+1}}{{#if:|+1}}{{#if:|+1}}{{#if:|+1}} <> 1
    | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Genau einer der Parameter 'wayback', 'webciteID', 'archive-today', 'archive-is' oder 'archiv-url' muss angegeben werden.|1}}
  }}{{#if: 
    | {{#switch: {{#invoke:Webarchiv|getdomain|{{{archiv-url}}}}}
        | web.archive.org = 
          {{#if:  || }}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Im Parameter 'archiv-url' wurde URL von Internet Archive erkannt, bitte Parameter 'wayback' benutzen.|1}} 
        | webcitation.org = 
          {{#if:  || }}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Im Parameter 'archiv-url' wurde URL von WebCite erkannt, bitte Parameter 'webciteID' benutzen.|1}} 
        | archive.today |archive.is |archive.ph |archive.fo |archive.li |archive.md |archive.vn = 
          {{#if:  || }}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Im Parameter 'archiv-url' wurde URL von archive.today erkannt, bitte Parameter 'archive-today' benutzen.|1}}
      }}{{#if: 
         | {{#iferror: {{#iferror:{{#invoke:Vorlage:FormatDate|Execute}}|Vorlage:FormatDate/Wartung/Error}}
             | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Der Wert des Parameter 'archiv-datum' ist ungültig oder hat ein ungültiges Format.|1}}
          |  }} 
         | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Der Pflichtparameter 'archiv-datum' wurde nicht angegeben.|1}}
      }}
    | {{#if: 
         | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Der Parameter 'archiv-datum' ist nur in Verbindung mit 'archiv-url' angebbar.|1}}
      }}
  }}{{#if:{{#invoke:URLutil|isHostPathResource|http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lustre-story%2Fhistory_1}}
    || {{#if:  || }} URL/Pfad ungültig.
  }}{{#if: VERIMAG Research Center
    | {{#if: {{#invoke:WLink|isBracketedLink|VERIMAG Research Center}}
        | {{#if:  || }} Linktext ungültig.
      }}
    | {{#if:  || }}Vorlage:Webarchiv/Wartung/Linktext_fehlt Linktext fehlt.
  }}{{#switch: 
    |addlarchives|addlpages= {{#if:  || }}{{#if: 1 |Vorlage:Webarchiv/Wartung/Parameter}}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: enWP-Wert im Parameter 'format'.|1}}
  }}{{#ifeq: {{#invoke:Str|find|http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lustre-story%2Fhistory_1%7Carchiv}} |-1
    || {{#ifeq: {{#invoke:Str|find|{{#invoke:Str|cropleft|http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lustre-story%2Fhistory_1%7C4}}%7Chttp}} |-1
         || {{#switch: {{#invoke:Webarchiv|getdomain|http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lustre-story%2Fhistory_1 }}
              | abendblatt.de | daserste.ndr.de | inarchive.com | webcitation.org = 
              | #default = {{#if:  || }}{{#if: 1 |Vorlage:Webarchiv/Wartung/URL}}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Archiv-URL im Parameter 'url' anstatt URL der Originalquelle. Entferne den vor der Original-URL stehenden Mementobestandteil und setze den Archivierungszeitstempel in den Parameter 'wayback', 'webciteID', 'archive.today' oder 'archive-is' ein, sofern nicht bereits befüllt.|1}}
            }} 
       }}
  }} – Frankreich (11/2005)</ref> Lustre wird überwiegend für die Programmierung und Steuerung dieser Art von Systemen verwendet.

Programm-Struktur

Die Programm-Struktur in Lustre kann grafisch als Netzwerk aus Operatoren dargestellt werden. Unterprogramme (nodes) werden auch als eigene Operatoren dargestellt und auch entsprechend mehrfach verwendet.

In Lustre sind nur wenige der üblichen Variablentypen vorhanden, so gibt es nur boolean, integer, real und tuple. Von den Operatoren sind die grundlegenden verfügbar:

arithmetische Operatoren: + - * / div mod
boolesche Operatoren: and or not
relationale Operatoren: == < <= > >=
bedingte Aktion: if then else if then else

Dazu kommen noch vier Fluss-Operatoren (temporal operators) (pre, ->, when, current). Diese werden speziell für Datenfluss-Zugriffe verwendet. Zum Beispiel liefert der Operator pre den Zustand des vorherigen Zeitpunktes der Variable.<ref name="Halbwachs">N. Halbwachs, P. Caspi, P. Raymond, D. Pilaud: The synchronous dataflow programming language LUSTRE. In: Journal: Proceedings of the IEEE volume 79.</ref>

Der Operator -> (followed by) wird zum Initialisieren von Variablen verwendet. So bedeutet beispielsweise X = 0 -> pre(X) + 1, dass X beim ersten Zeitpunkt 0 ist und bei allen anderen der vorherige Wert genommen und um 1 erhöht wird.<ref name="Caspi 1986">P. Caspi, D. Pilaud, N. Halbwachs, J. A. Plaice: LUSTRE: A declarative language for programming synchronous systems. 15. Oktober 1986.</ref>

Nachfolgend ein kleines Lustre Codebeispiel:<ref name="Caspi 2003">P. Caspi, D. Pilaud, N. Halbwachs, J. A. Plaice: LUSTRE: A declarative language for programming synchronous systems. 15. Oktober 1986</ref> <syntaxhighlight lang="text" style="margin-left:2em;"> 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);
      y = if b then pre(z) else C(z);<
  tel.

</syntaxhighlight>

In diesem Beispiel wird eine Prozedur (node) mit dem Namen „A“ beschrieben. Die weiteren verwendeten Prozeduren „B“ und „C“ sind an anderer Stelle im Programm definiert. „A“ wird mit drei input flows initialisiert (b, i, x) und gibt einen zurück (y).

Timing in Lustre

Das Timing bei Lustre ist wohl der Hauptvorteil dieser Sprache. Es basiert auf einem logischen Timing und wird in diskreten Zeitpunkten gezählt.<ref name="Caspi 2003" /> Logisches Timing sagt jedoch nichts über die Länge oder die Zeit zwischen den einzelnen Zeitpunkten aus. Es ist hier vielmehr eine Referenz zu den Werten der Variablen und Ausdrücke während des momentanen und/oder eines anderen Zeitpunkts. Neue Werte werden immer am Ende der Werteschlange angefügt.

Zusammenhang Variablen – Clock
Variable X	X₀	X₁	X₂	X₃	…	X_n
clock	0	1	2	3	…	n

Somit ist genau definiert, welcher Wert zu welchem Zeitpunkt gültig ist.

Kompilieren

Der Lustre Compiler überprüft nicht nur die Syntax des Programmcodes, sondern auch andere wichtige Voraussetzungen:<ref name="Halbwachs" />

Definitions-Kontrolle: hier wird überprüft, ob jede Variable auch wirklich nur ein einziges Mal definiert wurde
Clock-Konsistenz: alle kombinierten Ausdrücke und Variablen müssen die gleiche Clock-Basis besitzen
non-recursive calls: rekursive Aufrufe sind in Lustre nicht erlaubt
non-null-values: sind nur für nicht Clock-abhängige Variablen und Ausgaben erlaubt, alle anderen müssen initialisiert sein.

Verifikation

Der vom Compiler erzeugte Automat kann dann mit zusätzlichen Tools verifiziert werden (Lurette, Lucky).<ref>SYNCHRONE. VERIMAG Research Center (Frankreich), 11/2005</ref> Da Lustre überwiegend für sicherheitskritische Systeme verwendet wird und davon oftmals Menschenleben abhängen, ist die Verifikation ein sehr wichtiger Gesichtspunkt. So ist es beispielsweise nicht relevant, ob ein Zug jemals anhält, sondern vielmehr, ob der Zug bei einem roten Signal anhält.<ref name="Halbwachs" />

Einzelnachweise