Lustre (Programmiersprache)
aus Wikipedia, der freien Enzyklopädie
Lustre ist eine Programmiersprache.
Inhaltsverzeichnis |
[Bearbeiten] Geschichtliche Entstehung von Lustre
Lustre ist, wie Esterel, am Anfang der 80er Jahre entstanden. Auch hier war es das Fehlen geeigneter Programmiersprachen und Software-System für reactive systems der ausschlaggebende Anlass. Mit dem Zusammenschluss mehrerer französischer Forscher entstand die „synchrone Sprachen Schule“. Aus den ganzen 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 weiterentwickelt und ist mittlerweile in der Version V4 mit vielen verschiedenen Tools (Compiler, Simulatoren, Test-Tools, Code-Generatoren) verfügbar.
[Bearbeiten] Einsatzgebiete von Lustre
Lustre wird, wie reactive systems im Allgemeinen, u.a. in sicherheitskritischen Systemen wie z.B. Flugzeug- und Kraftwerksteuerung verwendet. Lustre wird überwiegend für die Programmierung und Steuerung dieser Art von Systemen verwendet. So wurde z.B. die Flugsteuerung im Airbus A320, die Notabschaltung von Kernkraftwerken und die Steuerung von fahrerlosen U-Bahnen in Lustre umgesetzt [3].
[Bearbeiten] 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
- boolean Operatoren: and, or, not
- relationale Operatoren: =, <, <=, >, >=
- bedingte Operatoren: if then else
Des Weiteren kommen noch 4 Fluss-Operatoren (temporal operators) dazu (pre, ->, when, current). Diese werden speziell für Datenfluss-Zugriffe verwendet. Zum Beispiel liefert der Operator „pre“ den Zustand des vorherigen Zeitpunktes der Variable. [1]
Der Operator „->“ (followed by) wird zum initialisieren von Variablen verwendet. So bedeutet z.B. „X = 0 -> pre(X) + 1“ das X beim ersten Zeitpunkt 0 ist und bei allen anderen der vorherige Wert genommen wird und um 1 erhöht wird. [5]
Nachfolgend ein kleines Lustre Code Beispiel [2]:
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 den Name „A“ beschrieben. Die weiteren verwendeten Prozeduren „B“ und „C“ sind an anderer Stelle im Programm definiert. „A“ wird mit 3 input flows initialisiert (b, i, x) und gibt einen zurück (y).
[Bearbeiten] 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 [2]. 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
- Abbildung 1: Variablen – Clock Zusammenhang
Somit ist genau definiert, welcher Wert zu welchem Zeitpunkt gültig ist.
[Bearbeiten] Compilieren
Der Lustre Compiler überprüft nicht nur die Syntax des Programmcodes, sondern auch andere wichtige Voraussetzungen [1]:
- 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.
[Bearbeiten] Verifikation
Der vom Compiler erzeugte Automat kann dann mit zusätzlichen Tools verifiziert werden (Lurette, Lucky) [4]. 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 z.B. nicht relevant ob ein Zug jemals anhält sondern vielmehr ob der Zug bei einem roten Signal anhält. [1]
[Bearbeiten] Referenzen
- [1] N. Halbwachs, P. Caspi, P. Raymond, D. Pilaud. The synchronouse dataflow programming language LUSTRE. Journal: Proceedings of the IEEE volume 79.
- [2] P. Caspi, A. Curic, A. Maignan, C. Sofronis, S. Tripakis (2003). Translating Discrete-Time Simulink to Lustre
- [3] VERIMAG Research Center – Frankreich (11/2005) http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lustre-story/history_1
- [4] VERIMAG Research Center – Frankreich (11/2005) http://www-verimag.imag.fr/SYNCHRONE/index.php?page=tools
- [5] P. Caspi, D. Pilaud, N. Halbwachs, J. A. Plaice (15. Oktober 1986). LUSTRE: A declarative language for programming synchronous systems
