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.[1] 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.[2]
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.[3]
Nachfolgend ein kleines Lustre Codebeispiel:[4]
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.
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.[4] 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.
| Variable X | X0 | X1 | X2 | X3 | … | Xn |
| 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:[2]
- 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).[5] 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.[2]
Einzelnachweise
- ↑ VERIMAG Research Center (Memento des Originals vom 9. Dezember 2006 im Internet Archive) Info: Der Archivlink wurde automatisch eingesetzt und noch nicht geprüft. Bitte prüfe Original- und Archivlink gemäß Anleitung und entferne dann diesen Hinweis. – Frankreich (11/2005)
- ↑ a b c N. Halbwachs, P. Caspi, P. Raymond, D. Pilaud: The synchronous dataflow programming language LUSTRE. In: Journal: Proceedings of the IEEE volume 79.
- ↑ P. Caspi, D. Pilaud, N. Halbwachs, J. A. Plaice: LUSTRE: A declarative language for programming synchronous systems. 15. Oktober 1986.
- ↑ a b P. Caspi, D. Pilaud, N. Halbwachs, J. A. Plaice: LUSTRE: A declarative language for programming synchronous systems. 15. Oktober 1986
- ↑ SYNCHRONE. VERIMAG Research Center (Frankreich), 11/2005
