Reprise de : v 1.15 2008/09/29 de J. Hugues (hugues@enst.fr), lui même repris de P. Raymond, pour adaptation à l'environnement UPMC.
Noeud « Next »: Partie 1 : Initiation à Lustre, Noeud « Previous »: (dir), Noeud « Up »: (dir)
Noeud « Next »: TP2 Problèmes, Noeud « Previous »: Top, Noeud « Up »: Top
LustreLe but de ce premier TP est de vous familiariser avec les
outils et le langage Lustre. Le TP est
découpé en plusieurs exercices, de difficulté
croissante.
Noeud « Next »: Tutoriel outils Lustre, Noeud « Up »: Partie 1 : Initiation à Lustre
L'environnement de travail de Lustre
est installé sur les stations de la salle SAR de l'UPMC.1
Pour le configurer, depuis un terminal que vous utiliserez pour invoquer les différents outils, déclarez la variable d'environnement LUSTRE_INSTALL et ajoutez le répertoire de lustre dans votre path.
export LUSTRE_INSTALL=/usr/local/lustre-v4-III-dc-linux64
export PATH=$PATH:$LUSTRE_INSTALL/bin
export _POSIX2_VERSION=199209
Noeud « Next »: Fonctions Lustre utiles, Noeud « Previous »: Mise en place, Noeud « Up »: Partie 1 : Initiation à Lustre
LustreedgeDans ce premier exercice, on va analyser l'exemple fourni
en cours: edge.
Ce programme détecte un front montant, c'est à dire
le passage d'une variable booléenne de la valeur false
à la valeur true. Nous en
rappelons la spécification :
node EDGE (b : bool) returns (edge : bool);
let
edge = false -> b and not pre b;
tel
Dans l'expression qui définit EDGE,
on retrouve plusieurs opérateur Lustre
dont nous rappelons la signification :
Le "et logique" (and)
et la négation (not), la
constante booléenne "faux" (mot-clé false).
Les autres opérateurs sont particuliers à Lustre:
La flèche (->)
permet de distinguer la valeur initiale du flot (en partie gauche)
des autres valeurs (en partie droite). La première valeur du
flot edge est donc false,
les valeurs successives sont définies par l'expression "b
and not pre b".
L'opérateur pre (pour précédent) permet de faire référence au "passé" : la valeur à l'instant précédent.
Au final, le noeud EDGE définit le flot modélisé par l'équation suivante:
EDGE(1) = faux,
pour tout t > 1, EDGE(t) = b(t) & not b(t-1)Question: Écrire le noeud EDGE dans un fichier edge.lus
Dans cette section, nous nous intéressons à
la simulation de programmes Lustre à
l'aide du simulateur graphique luciole.
Luciole requiert le nom du fichier
.lus à lire, et le nom du noeud à
simuler.
luciole edge.lus EDGE
Cette commande ouvre une fenêtre de simulation. Elle présente une série de boutons correspondant aux entrées/sorties du noeud.
Dans le cas du noeud EDGE, on dispose
d'un bouton pour l'entrée b et
une "lampe" pour la sortie edge
(Note: une lampe est un label qui s'affiche en rouge quand edge
est vrai, et en gris quand edge est
faux).
Par défaut, avec cette interface, cliquer sur le bouton "b" provoque un cycle de calcul avec b vrai, cliquer sur le bouton "Step" provoque un cycle de calcul avec b faux. Le résultat est renvoyé sur la lampe edge.
Commande : luciole edge.lus EDGE
Chronogrammes : La commande "Tools ! sim2chro" ouvre
l'outil de visualisation de chronogramme. L'évolution des
variables b et edge
est alors automatiquement visualisée sous forme de
chronogramme, indexé par les entrées du noeud..
Chronogramme
Modes auto-step et modes compose : Par défaut,
l'interface d'exécution de luciole
est en mode “auto-step”, c'est-à-dire que le noeud
est activé dès qu'on active sur une entrée
booléenne ou sur Step.
Avec la commande "Clocks ! Compose", on passe en mode
compose : les entrées booléennes
deviennent des interrupteurs qu'on peut activer/désactiver
sans provoquer un pas de calcul. Le pas de calcul est déclenché
en appuyant sur le bouton Step.
Ce mode est nécessaire pour des programmes qui ont plusieurs entrées, pour pouvoir composer des états où plusieurs entrées sont vraies simultanément.
Horloge temps-réel : Utiliser le bouton Step
peut devenir gênant, on peut alors utiliser une horloge
"temps-réel".
Le menu "Clocks ! Real time clock" permet d'activer/désactiver le mode temps-réel. Dans ce mode, le pas de calcul est automatiquement déclenché à intervalles réguliers. La période de l'horloge peut être modifiée avec "Clocks ! Change period". Elle est exprimée en milli-secondes.
Attention ! L'aspect temps-réel est relatif et dépend de la plate-forme utilisée. On utilise un système multi-tâches multi-utilisateur qui n'offre aucune garantie temps-réel. En pratique, si la machine est un peu trop chargée, le simulateur aura du mal à soutenir une période inférieure à quelques ms.
La compilation d'un programme Lustre
se déroule en plusieurs phases :
La pré-compilation transforme un programme Lustre
en programme "Lustre noyau",
aussi appelé code expansé. Cette phase est réalisée
par la commande :
lus2ec edge.lus EDGE
Elle produit un fichier EDGE.ec, qui dans ce cas précis est pratiquement très proche du programme initial edge.lus.
La compilation proprement dite transforme un programme ec en programme C. La commande est :
ec2c EDGE.ec -v
L'option -v permet de passer en mode
"verbeux" : des informations additionnelles sur le
déroulement de la compilation sont affichées (Note:
tous les outils Lustre disposent
d'une option -v).
Le résultat de la compilation est un fichier EDGE.c qui contient le noyau réactif du programme, ainsi que le fichier EDGE.h qui contient les informations nécessaires à l'utilisation du noyau.
La compilation en C ne produit que le noyau réactif du
système, c'est normalement à l'utilisateur d'écrire
un programme principal qui se charge de l'acquisition des entrées
et de la visualisation des sorties. Le compilateur ec2c
propose une option -loop qui produit,
en plus du noyau réactif, un programme principal standard. La
commande :
ec2c EDGE.ec -loop -v
produit EDGE.h, EDGE.c
plus un fichier EDGE_loop.c qui
contient une fonction main standard.
Pour des programmes simples (comme edge) ce programme principal peut
être utilisé tel-quel.
Pour obtenir un exécutable, il faut finalement utiliser un compilateur C, par exemple GCC sur GNU/Linux. La commande :
gcc EDGE.c EDGE_loop.c -o EDGE
compile les deux fichiers C, et produit l'exécutable EDGE. Le programme principal standard est en fait très rudimentaire : l'utilisateur doit taper au clavier, une par une, les entrées du programme.
Lux permet d'enchaîner toute
ces phases automatiquement. Il gère en particulier la phase de
liaison avec les différentes bibliothèques nécessaires
à la construction de l'exécutable. La commande :
lux edge.lus EDGE
enchaîne automatiquement toutes les phases et produit un exécutable EDGE.
Une solution alternative pour la compilation d'exécutable
consiste à générer le noyau réactif du
noeud Lustre sous la forme d'un automate
à états finis:
La phase de pré-compilation est la même :
lus2ec edge.lus EDGE
produit le fichier EDGE.ec. La commande :
ec2oc EDGE.ec
produit un automate, dans un format particulier appelé oc (dans un fichier EDGE.oc). On génère le code C correspondant avec la commande :
poc EDGE.oc
On obtient alors, comme avec ec2c un fichier EDGE.c et un fichier EDGE.h.
La commande poc dispose aussi d'une option -loop. On peut donc enchaîner les commandes suivante pour obtenir un programme exécutable edge :
poc EDGE.oc -loop
gcc EDGE.c EDGE_loop.c -o EDGE
Cette méthode de génération de code est assez proche de la précédente, à ceci près qu'un automate fournit un modèle pertinent pour raisonner sur les exécutions possibles du programme, et ainsi analyser son espace d'états.
Lustre dispose d'un outil de
vérification formelle de propriétés.
L'utilisateur exprime un ensemble de propriétés que
doit vérifier le programme, et l'outil indique si ces
propriétés sont satisfaites, ou fournit un
contre-exemple.
On utilise ici l'outil xlesar : une
interface graphique du vérificateur lesar.
Pour lancer l'outil, taper : xlesar.
Sélectionner le fichier et le noeud à analyser (commande “Browse”). Les entrées/sorties du noeud sont affichées.
L'outil xlesar
La partie basse de la fenêtre permet de rentrer les différentes propriétés que l'on souhaite vérifier (commandes New , puis sur Edit). Cette dernière commande ouvre une fenêtre d'édition de propriété. La partie gauche est l'éditeur de propriété proprement dit, la partie droite permet de lancer la vérification.
L'outil xlesar en action
Une propriété triviale: Le point important est
que la propriété doit être exprimée sous
la forme d'une expression booléenne Lustre.
Par défaut, cette définition est true,
et est donc vraie. On peut tout de même essayer de lancer le
vérificateur en appuyant sur “RUN PROOF”. On
obtiendra naturellement (dans la fenêtre de dialogue) le
résultat "TRUE PROPERTY".
Une propriété vraie: On va maintenant exprimer et vérifier une propriété plus complexe. On cherche à évaluer la propriété suivante:
La sortie EDGE ne peut pas être vraie à deux instants consécutifs.
Pour utiliser le vérificateur, on doit tout d'abord
traduire cette propriété en une expression Lustre.
On va simplement dire que, initialement, la propriété
est toujours vérifiée, puis à chaque instant, si
edge est vraie alors edge
était faux à l'instant précédent. En
utilisant l'opérateur "implication logique" (=>),
cela donne :
true -> (edge => not pre edge)
On peut alors lancer le prouveur, en utilisant l'option “Verbose” pour avoir des informations sur le déroulement de la preuve. On peut essayer les différents algorithmes proposés :
Enumerative , Symbolic forward et Symbolic backward. On doit évidemment obtenir la même réponse pour chaque algorithme.
Complexité de la preuve : Grâce au mode verbeux, on peut se faire une idée de la "complexité" de la preuve : avec l'algorithme énumératif, le nombre d'états et de transitions sont une bonne mesure de la complexité de la propriété (4 états et 8 transitions pour cet exemple). En symbolique, c'est le nombre d'itérations qui mesure la complexité (2 pas de calculs en mode "forward" et en mode "backward").
Un autre exemple de propriété vraie est edge ne peut être vrai que si b est vrai, ce qu'on traduit simplement par : edge => b.
Cette propriété est beaucoup plus évidente que la précédente : elle est, pour ainsi dire, écrite dans le programme. On peut d'ailleurs observer cette simplicité en regardant la complexité de la preuve : 2 états et 2 transitions en énumératif, 2 pas de calcul en "forward", et 0 pas de calcul en mode "backward".
Une propriété fausse: On va maintenant voir ce qui se passe pour une propriété fausse, par exemple :
si b est vrai, alors edge est vrai
Ce qu'on traduit par b => edge. Si on n'utilise aucune option, le prouveur se contente de répondre FALSE PROPERTY. Il faut utiliser l'option Diagnosis pour obtenir un contre exemple :
DIAGNOSIS:
--- TRANSITION 1 ---
bL'interprétation est la suivante : dès la première réaction du programme, si b est vrai, la propriété n'est pas satisfaite. Ce résultat est attendu: la sortie est toujours fausse à l'instant initial. Il faut donc modifier la propriété :
Sauf à l'instant initial, si b est vrai, alors edge est vrai.
Traduite en Lustre, cette propriété
devient : true -> (b => edge).
Là encore on va obtenir un résultat négatif, avec un nouveau contre-exemple :
DIAGNOSIS:
--- TRANSITION 1 ---
b
--- TRANSITION 2 ---
bqui stipule que la propriété est fausse si b est vrai deux fois de suite. Mieux vaut alors se rentre à l'évidence : la propriété est bien totalement fausse.
Noeud « Next »: Observateurs, Noeud « Previous »: Tutoriel outils Lustre, Noeud « Up »: Partie 1 : Initiation à Lustre
Lustre utilesLe but de cet exercice est de programmer une bibliothèque d'opérateurs qui seront réutilisés dans les exercices suivants. Ces opérateurs seront regroupés dans un fichier utiles.lus.
Ecrire et simuler un noeud jafter
:
Entrée : X, booléen
Sortie : Y, booléen
Fonction : Y(t) vrai ssi X(t-1) existe et est vrai
Ecrire et simuler un noeud edge :
Entrée : X, booléen
Sortie : Y, booléen -
Fonction : Y(t) vrai ssi (X(t-1) existe et est faux et X(t) est vrai) ou (X(t-1) existe et est vrai et X(t) est faux)
Remarque :
Les fronts descendants de x sont simplement les fronts montants de la négation de x, c'est-à-dire :
edge(not x).
Ecrire et simuler un noeud switch :
Entrées : orig, on, off (booléens)
Sortie : state (booléen)
Fonction :
state passe de faux à vrai sur la commande on,
de vrai à faux sur la commande off,
state est initialement égal à orig.
Noeud « Next »: Code C et Lustre, Noeud « Previous »: Fonctions Lustre utiles, Noeud « Up »: Partie 1 : Initiation à Lustre
Les observateurs sont des programmes particuliers
utilisés pour exprimer des propriétés ou des
hypothèses. Leur caractéristique principale est d'avoir
une seule sortie booléenne (qu'on nomme par convention ok).
Cette sortie doit rester vraie aussi longtemps que les entrées de l'observateur satisfont la propriété. Par abus de langage, on dit que l'observateur “implante” la propriété.
Une des propriétés les plus utiles concerne l'ordonnancement d'événements : un événement “X” doit impérativement apparaître au moins une fois entre un événement “A” et un événement “B”.
Ecrire un observateur once_from_to(X, A, B :
bool) returns (ok : bool) qui implante cette propriété.
Indication : on remarque que cette propriété
fait intervenir une notion d'intervalles temporels, qui débutent
sur un A, et se termine sur le premier B qui suit. Le noeud switch
est donc tout à fait indiqué pour servir de base à
l'observateur once_from_to.
Noeud « Next »: Approfondissement des constructions Lustre, Noeud « Previous »: Observateurs, Noeud « Up »: Partie 1 : Initiation à Lustre
Dans cette section, on s'intéresse à
l'inclusion de code C dans un programme
Lustre. Une telle action est souvent
nécessaire pour interfacer le code avec d'autres portions
logicielles, dont des drivers.
La construction d'une telle application est un peu plus complexe, du fait du modèle de compilation des applications C qui impose à l'utilisateur de définir les dépendances entre les différents modules à compiler puis lier.
On cherche à interfacer le code C
suivant, défini dans gett.c
#include <stdio.h>
int gett (int a)
{
usleep(200000);
return a;
}et comme fichier prototype (gett.h):
int gett(int a);
avec le code Lustre suivant
function gett (val : int) returns(num : int);
node c_code (a : int) returns (x : int);
let
x = gett(a);
tel;
Vous noterez la définition de la fonction gett
qui indique à Lustre
l'existence de gett sans pour
autant la définir.
Pour compiler ce programme, il faut au préalable fournir la
définition C du code que l'on
souhaite inclure. Le fichier Lustre
ayant comme point d'entrée c_code,
vous définirez le fichier c_code_ext.h
fournissant les définitions au code extérieur, il a
pour contenu:
#include "gett.h"
Pour compiler ce programme, il est nécessaire de suivre la démarche suivante:
lustre c_code.lus c_code
poc -loop c_code.oc
gcc -c gett.c
gcc -c c_code.c
gcc c_code_loop.c gett.o c_code.o -o c_codeOn peut alors exécuter le programme c_code.
Noeud « Previous »: Code C et Lustre, Noeud « Up »: Partie 1 : Initiation à Lustre
Vous trouverez dans $LUSTRE_INSTALL/doc/tutorial.ps
un tutoriel plus complet du langage Lustre.
Il décrit en détail plusieurs exercices qui vous permettront d'approfondir votre connaissance du langage. Vous pouvez vous y intéresser pour préparer les prochains exercices ;)
Noeud « Previous »: Partie 1 : Initiation à Lustre, Noeud « Up »: Top
Le but de ce second TP est de poursuivre l'apprentissage
de Lustre et de résoudre des
problèmes plus complexes.
Important: Il est indispensable d'avoir complété les parties Mise en place, Tutoriel outils Lustre et Fonctions Lustre utiles avant de poursuivre.
Noeud « Next »: Contrôleur de feux de voiture, Noeud « Up »: TP2 Problèmes
Pour éviter l'ouverture/fermeture répétée des portillons de sortie du métro, la RATP a déployé à St Lazare un mécanisme de détection des sorties des usagers.
La porte reste ouverte en permanence, deux cellules photo-sensibles (notées A et B) contrôlent le passage des usagers.
Le passage s'effectue de A vers B. Tout passage de B vers A doit
déclencher la fermeture du portillon, représentée
par une variable booléenne alarm.
Autrement dit, alarm est déclenchée si la séquence
des événements captés est différente de
((notA et notB)* . (A et notB) . (notA et notB)* . (notA et B))*
Coder en Lustre le noeud
Portillon, il aura pour spécification:
node Portillon (A, B: bool) returns (alarm: bool);
On fera l'hypothèse que A et B ne peuvent être simultanément vrais, du fait des contraintes physiques du système.
Simuler et vérifier ce noeud.
Noeud « Next »: Contrôleur de feux (version étendue), Noeud « Previous »: Portillon dans le métro, Noeud « Up »: TP2 Problèmes
Une voiture dispose de trois types de lampes: veilleuses, codes et phares. Le conducteur dispose d'une manette qui dispose de plusieurs degrés de liberté.
On souhaite décrire en Lustre
le module de contrôle des feux d'une voiture. L'utilisateur
entre ses ordres via une manette et une série d'interrupteurs,
agissant sur les phares de la voiture.
Voici la description du contrôleur de phare :
La manette peut être tournée
dans le sens direct (TD) ou indirect
(TI);
A partir d'une situation initiale
où tout est éteint, TD
allume les veilleuses, un second TD
éteint les veilleuses et allume les codes;
Lorsqu'on est en codes ou en
phares, TI les éteint et rallume
les veilleuses, un second TI éteint
tout;
Le fait de tirer la manette vers
l'avant (CP) permet de commuter entre
codes et phares; lorsqu'on est en codes, CP
éteint les codes et allume les phares, un second CP
éteint les phares et rallume les codes;
Le conducteur ne peut pas simultanément tourner et tirer la manette.
Pour les variables d'entrée, on prendra trois
variables booléennes TD, TI
et CP, vraies aux instants où
l'action correspondante est effectuée par le conducteur.
Pour les sorties, on choisit trois flots qui représentent
l'état des lampes : veilleuses
(resp. codes, phares)
est vrai tant que les veilleuses (resp. les codes, les phares) sont
allumées, et est faux tant qu'elles sont éteintes.
Écrire et simuler un programme Lustre
qui décrit le noyau du contrôleur.
Noeud « Next »: Porte de tramway, Noeud « Previous »: Contrôleur de feux de voiture, Noeud « Up »: TP2 Problèmes
On ajoute à présent des projecteurs antibrouillard et de longue portée. Deux boutons-poussoirs permettent d'activer les feux antibrouillard (bouton AB) et les longue portée (bouton LP).
Le rôle de la manette est inchangé.
A partir d'une situation initiale, une pression sur AB (resp. LP) sélectionne les antibrouillard (resp. les longue portée), et une seconde pression les désélectionne.
Les antibrouillard (resp. les longue portée) ne sont allumés que quand on est en codes (resp. en phares). Dans ce cas, ils ne sont allumés que s'ils sont sélectionnés.
On conserve les entrées et sorties de la version simple, auxquelles on ajoute :
deux entrées AB
et LP vraies à chaque pression
du bouton correspondant.
deux sorties anti_brouillard et
longue_portee représentant
l'état des projecteurs d'antibrouillard et de longue portée
(vrai : allumé, faux : éteint).
Écrire et simuler un programme Lustre
qui décrit le noyau du contrôleur de la version
étendue.
En utilisant xlesar, on va chercher à prouver les propriétés suivantes sur le contrôleur de feux (étendu) :
veilleuse, code et phare sont exclusifs
on ne peut être en antibrouillard que si on est en code
on ne peut être en longue-portée que si on est en phares.
Si une preuve échoue : utiliser l'option “Diagnosis” de xlesar pour obtenir un contre-exemple. On sera éventuellement amené à introduire des hypothèses sur les entrées pour mener à bien la preuve.
Noeud « Next »: Porte de tramway (version étendue), Noeud « Previous »: Contrôleur de feux (version étendue), Noeud « Up »: TP2 Problèmes
On souhaite construire un module contrôlant l'ouverture et la fermeture automatique d'une porte de tramway.
Il y a trois éléments dans l'environnement du contrôleur :
La porte : le contrôleur lui envoie les commandes
fermer_porte et ouvrir_porte.
L'état de la porte est connu en permanence grâce au
capteur porte_ouverte.
On suppose que la porte fonctionne parfaitement : elle s'ouvre et se ferme quand on lui demande, la seule inconnue étant le temps qu'elle met à réagir.
Pour que la communication s'effectue bien, il faut que le
contrôleur maintienne la commande ouvrir_porte
(resp. fermer_porte) jusqu'à ce
que la porte soit effectivement ouverte (resp. fermée).
L'usager envoie des demandes demande_porte.
On ne peut faire aucune supposition sur son comportement (on doit même plutôt considérer qu'il est potentiellement malveillant !).
Le contrôleur doit donc filtrer et enregistrer les demandes pour pouvoir les traiter en toute sécurité.
Le tramway fournit au contrôleur l'information
en_station qui signifie que le tramway
est arrêté dans une station.
Quand cet indicateur devient vrai, le contrôleur peut ouvrir la porte (si la demande en a été faite).
Au bout d'un certain temps, le tramway émet le signal
attention_depart qui signifie au
contrôleur que le ramassage des passagers est terminé
et qu'il faut fermer la porte. A partir de cet instant, le tramway
va attendre du contrôleur le signal porte_ok
qui signifie que la porte est bien fermée, et qu'il peut
redémarrer.
On peut faire des hypothèses fortes sur le
comportement du tramway : à partir du moment où
l'information en station devient vraie, elle le restera (au moins)
tant que le signal porte_ok n'est pas
émis par le contrôleur.
Le but essentiel du contrôleur est de garantir la sécurité du tramway et des usagers : la porte doit être toujours fermée en dehors des stations.
En plus de cette condition de sureté de fonctionnement, le contrôleur doit satisfaire dans la mesure du possible les demandes de l'utilisateur; un comportement trop sécuritaire correspondrait à ne jamais ouvrir la porte ;).
Les demandes de l'utilisateur doivent donc être prises en compte de la manière suivante :
Hors station, demande_porte
signifie qu'un utilisateur veut descendre au prochain arrêt :
la demande sera traitée à l'arrivée dans la
prochaine station.
En station, et avant le signal
attention_depart, demande_porte
provoque l'ouverture de la porte.
En station, après le signal attention_depart,
demande_porte est ignorée.
Ouverture de la porte Il est recommandé d'utiliser les variables intermédiaires suivantes :
un signal depart,
vrai à l'instant où le tramway quitte une station.
une variable accepter_demande,
vraie dans tout l'intervalle de temps où une demande de porte
peut être acceptée.
une variable porte_demandee,
vraie quand la porte a effectivement été demandée
alors que cette demande était acceptable.
Le schéma suivant montre (en fonction du chronogramme de
en_station), le fonctionnement de ces
variables dans le cas où la demande est faite hors station :
On remarque que la commande ouvrir_porte
peut être émise dès que les conditions en_station
et porte_demandee sont toutes deux
vraies, et doit être maintenue jusqu'à ce que la porte
s'ouvre effectivement.
Fermeture de la porte On conseille d'utiliser une variable
depart_imminent qui devient vraie dès
que le tramway souhaite repartir, et reste vraie jusqu'à ce
que le tramway reparte.
La commande fermer_porte doit être
envoyée quand les conditions suivantes sont réunies :
le départ est imminent,
l'ouverture de la porte a été demandée (elle est donc soit ouverte, soit en cours d'ouverture),
la porte est effectivement ouverte.
Comme pour la commande ouvrir_porte,
cette commande doit être maintenue jusqu'à ce qu'elle
soit effective (i.e. que la porte soit fermée).
Porte ok Quand le départ est imminent, le contrôleur
doit envoyer le signal porte_ok au
tramway pour lui signaler qu'il peut redémarrer. Il y a deux
cas possibles :
la porte n'a pas été demandée, auquel cas on peut redémarrer tout de suite.
la porte a été demandée, et il faut attendre que la porte soit fermée.
Pour simuler et mettre au point le programme, le plus
simple est d'utiliser le simulateur graphique luciole.
Pour la mise au point, il est conseillé de mettre les variables locales en sortie, de manière à visualiser leur comportement.
De plus, on peut supprimer certaines entrées pour
simplifier la simulation. En particulier, le délai de réaction
de la porte n'a pas d'importance sur la fonctionnalité du
programme. On peut donc simuler le programme en supposant que la
porte réagit avec exactement un top de retard aux commandes
ouvrir_porte et fermer_porte.
On va prouver formellement que le contrôleur satisfait la propriété de sûreté essentielle suivante :
Le tramway ne peut jamais rouler avec la porte ouverte.
Propriété : Exprimez cette propriété
en Lustre, en fonction des
entrées/sorties du programme.
Plusieurs hypothèses de fonctionnement sur la porte et le tramway vont nous permettre de valider cette propriété. On ne peut faire aucune hypothèse sur l'utilisateur qui est supposé imprévisible.
Hypothèses sur la porte : L'hypothèse
première est que la porte s'ouvre (resp. se ferme)
inévitablement sur la commande ouvrir_porte
(resp. fermer_porte), après un
délai quelconque.
Ce type de propriété, non bornée dans le
temps, est appelée propriété de vivacité,
et ne peut ni être exprimée en Lustre
ni (a fortiori) prise en compte par le vérificateur de
programmes.
On va donc utiliser une hypothèse proche, exprimable en
Lustre : la porte ne peut s'ouvrir et se
fermer que sur ordre du contrôleur.
Dans ce cas, la porte peut ne jamais s'ouvrir ou se fermer. Cependant, d'un point de vue sûreté de fonctionnement, cette hypothèse est acceptable : si on arrive à prouver la propriété désirée avec cette hypothèse, cela signifie que le contrôleur est correct pour tout les comportement "normaux" de la porte, mais aussi pour quelques comportements anormaux (les cas où la porte se "bloque" en position ouverte ou fermée).
Ecrire une hypothèse (assertion) qui stipule que :
initialement, la porte est fermée,
la porte ne peut s'ouvrir que si
ouvrir_porte est vraie,
la porte ne peut se fermer que si fermer_porte
est vraie.
Hypothèses sur le tramway : On va supposer que le
tramway est initialement hors station. Le tramway peut entrer en
station à tout instant. Une fois en station, il ne peut
repartir qu'après avoir émis attention_depart
et avoir reçu le signal porte_ok.
Autrement dit :
Il doit y avoir au moins une
occurrence de attention_depart entre
les événements "arrivée en station"
et "départ de station".
Il doit y avoir au moins une occurrence de porte_ok
entre les événements attention_depart
et "départ de station".
Indication: pensez à utiliser l'observateur générique
once_from_to.
Noeud « Previous »: Porte de tramway, Noeud « Up »: TP2 Problèmes
Dans cette version étendue, on rajoute un élément à contrôler : un passerelle extractible.
En plus d'une porte coulissante classique, le tramway dispose (sous la porte) d'une passerelle extractible qui peut sortir et se poser sur le quai pour faciliter l'accès aux poussettes, fauteuils roulants etc.
En plus de la porte, le contrôleur doit maintenant gérer l'ouverture et la fermeture de la passerelle. Celle-ci fonctionne de manière très similaire à la porte. On ajoute deux nouvelles sorties au contrôleur:
sortir_pass
rentrer_pass
et une nouvelle entrée :
pass_sortie qui indique l'état
de la passerelle.
On fait sur la passerelle les mêmes hypothèses que sur la porte : elle fonctionne correctement et réagit uniquement aux commandes du contrôleur.
L'usager : Il peut maintenant demander la passerelle avec la commande :
demande_pass
Cette demande signifie que l'usager veut à la fois la passerelle sortie et la porte ouverte, même si la porte n'a pas été explicitement demandée.
Le tramway : Pour pouvoir redémarrer, il doit
maintenant attendre que la porte soit fermée et que la
passerelle soit rentrée. En fait, ces deux conditions sont
réunies en une seule : le nouveau contrôleur émet
une sortie porte_pass_ok qui remplace
l'ancienne porte_ok.
Ce nouvel élément pose de nouvelles contraintes de sûreté de fonctionnement :
Le tramway ne doit jamais rouler avec la passerelle sortie
La passerelle ne doit jamais sortir ou rentrer quand la porte est ouverte, sinon cela serait dangereux pour les chevilles des usagers.
Cette contrainte implique un ordre causal dans les commandes à émettre : s'il doit sortir la passerelle, le contrôleur doit le faire avant d'ouvrir la porte; de même, il doit fermer la porte avant de rentrer la passerelle.
Comme pour la porte, le contrôleur doit satisfaire autant que possible les demandes de l'usager. Les règles sont très similaires à celles de la porte :
Toute demande faite entre le moment où le tramway quitte une station et le moment où le tramway souhaite repartir de la station suivante doit être prise en compte.
Sauf dans le cas particulier où, en station, la porte est déjà ouverte ou sur le point de s'ouvrir, auquel cas il est trop tard pour sortir la passerelle sans risque pour les chevilles des usagers.
Écrire et simuler le nouveau contrôleur.
Vérifier les propriétés de sûreté suivantes :
Le tramway ne peut pas rouler avec la porte ouverte ou la passerelle sortie
La passerelle ne peut pas bouger (ni rentrer, ni sortir) quand la porte est ouverte.
[1] Vous pouvez aussi télécharger
Lustre (pour plates-formes GNU/Linux,
x86) à l'URL suivante:
http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html