Lustre (linguaggio di programmazione)

Lustre è un linguaggio di programmazione dichiarativo sincrono .

Storia di Lustre

Come Esterel , Lustre è stato creato nei primi anni '80. Anche qui la ragione decisiva è stata la mancanza di linguaggi di programmazione e sistemi software adeguati per sistemi reattivi . Con la fusione di diversi ricercatori francesi, è stata creata la "scuola di lingue sincrona". Dai suggerimenti dei ricercatori, la scelta è stata fatta per Lustre, in quanto questa era la più semplice. Lustre è stato sviluppato molto da allora ed è ora disponibile nella versione V4 con molti strumenti diversi ( compilatori , simulatori, strumenti di test, generatori di codice).

Aree di applicazione di Lustre

Come i sistemi reattivi in generale, Lustre viene utilizzato in sistemi critici per la sicurezza come i controlli di aeromobili e centrali elettriche. Ad esempio, a Luster sono stati implementati il ​​controllo del volo nell'Airbus A320 , l'arresto di emergenza delle centrali nucleari e il controllo delle metropolitane senza conducente. Lustre è utilizzato principalmente per programmare e controllare questo tipo di sistema.

Struttura del programma

La struttura del programma in Lustre può essere rappresentata graficamente come una rete di operatori. Anche le subroutine (nodi) vengono visualizzate come operatori separati e vengono utilizzate più volte di conseguenza.

In Lustre ci sono solo alcuni dei soliti tipi di variabili, quindi ci sono solo booleana, intera, reale e tupla. Tra gli operatori sono disponibili quelli base:

  • operatori aritmetici: + - * / div mod
  • operatori booleani: and or not
  • operatori relazionali: == < <= > >=
  • azione condizionale: se allora altrimenti if then else

In più ci sono quattro operatori fluviali (operatori temporali) ( pre, ->, when, current). Questi vengono utilizzati specificamente per l'accesso al flusso di dati. Ad esempio, l' operatore restituisce prelo stato del punto temporale precedente della variabile.

L'operatore ->(seguito da) viene utilizzato per inizializzare le variabili. Ad esempio X = 0 -> pre(X) + 1, ciò significa che Xil primo punto temporale è 0 e per tutti gli altri viene preso il valore precedente e aumentato di 1.

Di seguito è riportato un piccolo esempio di codice Lustre:

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 questo esempio viene descritta una procedura (nodo) con il nome "A". Le altre procedure "B" e "C" utilizzate sono definite altrove nel programma. "A" viene inizializzato con tre flussi di input (b, i, x) e ne restituisce uno (y).

Tempismo in Lustre

Il tempismo in Lustre è senza dubbio il principale vantaggio di questo linguaggio. Si basa su un tempismo logico e viene conteggiato in tempi discreti. Tuttavia, il tempismo logico non dice nulla sulla lunghezza o il tempo tra i singoli punti nel tempo. Piuttosto, è un riferimento ai valori delle variabili e delle espressioni durante il momento corrente e / o in un altro momento. I nuovi valori vengono sempre aggiunti alla fine della coda dei valori.

Relazione tra variabili e orologio
Variabile X X 0 X 1 X 2 X 3 ... X n
orologio 0 1 2 3 ... n

Questo definisce precisamente quale valore è valido in quale momento.

Compilare

Il compilatore Lustre non solo controlla la sintassi del codice del programma, ma anche altri importanti requisiti:

  • Controllo della definizione: qui viene verificato se ciascuna variabile è stata effettivamente definita una sola volta
  • Consistenza dell'orologio: tutte le espressioni e le variabili combinate devono avere la stessa base dell'orologio
  • chiamate non ricorsive: le chiamate ricorsive non sono consentite in Lustre
  • valori non nulli: sono consentiti solo per variabili e uscite non dipendenti dal clock, tutti gli altri devono essere inizializzati.

verifica

L'automa generato dal compilatore può quindi essere verificato con strumenti aggiuntivi (Lurette, Lucky). Poiché Lustre è utilizzato principalmente per sistemi critici per la sicurezza e le vite umane spesso dipendono da esso, la verifica è un aspetto molto importante. Ad esempio, non è rilevante se un treno si ferma mai, ma piuttosto se il treno si ferma quando c'è un segnale rosso.

Prove individuali

  1. ↑ VERIMAG Research Center ( Memento del l' originale datata 9 dicembre, 2006 in Internet Archive ) Info: Il dell'archivio collegamento è stato inserito automaticamente e non è stata ancora verificata. Si prega di controllare l'originale e il collegamento all'archivio secondo le istruzioni, quindi rimuovere questo avviso. - Francia (11/2005) @ 1@ 2Modello: Webachiv / IABot / www-verimag.imag.fr
  2. ↑ a b c N. Halbwachs, P. Caspi, P. Raymond, D. Pilaud: The synchronous dataflow programming language LUSTER. In: Journal: Proceedings of the IEEE volume 79.
  3. ↑ P. Caspi, D. Pilaud, N. Halbwachs, JA Plaice: LUSTER: Un linguaggio dichiarativo per la programmazione di sistemi sincroni. 15 ottobre 1986.
  4. ^ A b P. Caspi, D. Pilaud, N. Halbwachs, JA Plaice: LUSTER: Un linguaggio dichiarativo per la programmazione di sistemi sincroni. 15 ottobre 1986
  5. ↑ SINCRONI. Centro di ricerca VERIMAG (Francia), 11/2005