Version : v 2.0 20012/10/31 de E. Encrenaz.
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-c-linux64
export PATH=$PATH:$LUSTRE_INSTALL/bin
export _POSIX2_VERSION=199209Code
Lustre, représentation en automates, observateurs1.1
Modélisation d'un métronomeOn souhaite modéliser en Lustre le comportement d'un métronome. Le dispositif est évalué sur l'horloge de base et dispose de deux entrées : reset et delay. Il produit deux signaux en sortie tic et tac.
node metronome (reset : bool; delay : int) returns (tic, tac : bool);
A chaque occurrence du signal reset, la période de pulsation delay est mémorisée, et le métronome produit alternativement, à chaque période, un tic ou un tac.
Tant que le système n'a pas été initialisé, le métronome ne produit ni tic ni tac.
Lors d'une réinitialisation, le système reste sur le tic (ou le tac) qu'il devait produire; le compteur décomptant le délai restant avant l'émission du tic (ou du tac) est réinitialisé.
Lors d'une (ré) initialisation, le délay affecté à la période de pulsation est strictement positif.
Pour modéliser ce système, vous pourrez utiliser les variables auxiliaires désignées ci-dessous :
hz : représente la période courante depuis le dernier reset; i.e. le nombre de ticks de l'horloge de base à décompter pour une période définie par delay.
first : le système a subi une première initialisation ou non.
n : le nombre de ticks de l'horloge de base restant avant l'échéance de la période.
state : émission d'un tic ou d'un tac à l'échéance de la période.
Question 1 : Écrire le noeud métronome et simuler son exécution.
Le compilateur lustre-v4 génère un code C à partir de la description Lustre. La génération se fait en deux étapes, en utilisant les outils lus2oc et poc. Vous analyserez la structure de l'automate à partir du code C généré.
syntaxe : lus2oc nom_fichier.lus noeud [options]
options : -0 (code en boucle) ou -1 (code déplié selon les horloges) ou -2 (code déplié selon les horloges et certaines variables)
produit une description en automate au format oc dans le fichier nom_fichier.oc
syntaxe : poc [-loop] nom_fichier.oc
produit un code C (et la boucle d'évaluation si l'option loop est activée), dans le fichier noeud.c
Question 2 : Représentez l'automate implicite associé à l'évaluation de ce noeud. Vous pouvez le déduire directement du code Lustre ou bien en analysant le code C en boucle généré par lus2oc puis poc.
Question 3 : Analysez la structure de l'automate généré par lus2oc et poc lorsque lus2oc est exécuté avec l'option -2 et comparez la à l'automate implicite. Selon quelle(s) variable(s) l'automate implicite a-t-il été déplié ?
Question 4 : Ecrire une description lustre du métronome explicitant les traitements différents selon la valeur de la variable state. On nommera ce noeud metronome_deplie.
Question 5 : Construisez le programme permettant de prouvez (par équivalence observationnelle) que les deux noeuds sont équivalents (leurs états initiaux sont bisimilaires). Cette preuve peut-elle être réalisée sur les abstractions booléennes des noeuds metronome et metronome_deplie ? Simulez l'exécution de ce programme de preuve sur une séquence significative.
Question 6 : On souhaite vérifier des propriétés de sûreté sur la description du métronome :
P1 : A tout instant, on ne peut avoir simultanément tic et tac.
P2 : On ne peut jamais avoir deux tic consécutifs (il y a exactement un tac entre deux tics).
P3 : Les occurrences consécutives de deux tic (s'il n'y a pas de reset entre eux) sont séparées par exactement 2 * delay ticks de l'horloge de base.
Pour chaque propriété, vous construirez l'automate observateur associé, puis vous exprimerez cet automate sous la forme d'un noeud Lustre. Vous synchroniserez l'ensemble des noeuds observateurs avec le noeud metronome.
Quelle sera la propriété à vérifier sur le système observé ?
Faut-il adjoindre des hypothèses sur les entrées pour vérifier ces propriétés ? Si oui, lesquelles ? Sont-elles exprimables sous la forme d'un observateur ? Quelle est alors la propriété vérifiée sur le modèle observé et sous hypothèse ?
Indiquez les résultats de vérification fournis par Lesar et interprétez ces résultats.
Dans sa thèse, K. Mc Millan présente un arbitre de bus distribué et synchrone. Un arbitre de bus est un dispositif connecté à un bus de communication, et chargé d'arbitrer entre les requètes d'accès au bus émanant de plusieurs composants désirant communiquer sur le bus. Le bus étant une ressource partagée, à chaque instant un seul composant peut disposer du bus pour réaliser sa communication vers un ou plusieurs autres composants connectés au bus; l'arbitre proposé attribue le bus pour un tick (il y a un nouvel arbitrage à chaque tick) et garantit une certaine équité de traitement des requètes.
L'arbitre est composé d'autant de cellules élémentaires qu'il y a de composants susceptibles d'écrire sur le bus, chaque cellule étant reliée à un tel composant. La cellule reçoit une demande d'accès au bus par le signal Req_in et autorise l'accès par le signal Ack_out. Les cellules doivent réaliser le mécanisme d'arbitrage de telle sorte qu'à chaque instant, au plus une requête parmi les requêtes positionnées (Req_in = 1) soit autorisée (Ack_out = 1). Les cellules sont connectées selon un anneau; l'arbitrage se fait par niveau de priorité de la cellule. Afin d'éviter les famines, un mécanisme d'inversion de la priorité est implanté : si une requête perdure suffisamment longtemps, elle passera en priorité maximale. La circulation d'un jeton sur l'anneau permet de déterminer si une requête a persisté suffisamment longtemps (deux réceptions du jeton).
Le schéma interne d'une cellule et l'interconnexion des cellules entre-elles sont décrits sur les figures suivantes.
Figure 1. Architecture interne d'une cellule d'arbitrage. Les carrés W et T représentent des éléments mémorisants (opérateur pre en Lustre)
Figure 2. Connexion des cellules d'arbitrage. Le diagramme au dessus du tk_in de la cellule 1 est un multiplexeur permettant l'initialisation de tk_in_1 à 1 au premier instant.
Question 1 : Modélisez un arbitre composé de 3 cellules en Lustre. Initialement, le jeton sera présent dans la première cellule. Vérifiez le bon fonctionnement de l'arbitre à l'aide de quelques simulations. Vous étudierez particulièrement le fonctionnement de l'arbitre lorsqu'il est soumis à un seule requête continue (sur plusieurs cycles), à deux requêtes toujours exclusives, à deux requêtes non exclusives, à trois requêtes sporadiques et à trois requêtes continues. Vous étudierez également les quelques cycles suivant l'initialisation.
Question 2 : Générez l'automate de l'arbitre (option -2). Combien d'états contient-il, quelles variables ont été dépliées ?
Question 3 : Les propriétés suivantes sont-elles vérifiées sur l'arbitre à trois cellules ?
P1 : A tout instant, il n'y a qu'une seule requête autorisée à accéder au bus.
P2 : A tout instant, une autorisation d'accès au bus correspond bien à une demande effective du bus.
P3 : Les requêtes de la cellule la plus prioritaire sont toujours servies (immédiatement).
P4 : Les requêtes de la cellule la moins prioritaire seront servies si elles persistent suffisamment longtemps. (Comment exprimer “suffisamment longtemps” ?)
Pour chaque propriété, vous construirez un automate observateur et dans certains cas vous construirez les automates observateurs des hypothèses, puis vous chercherez à vérifier le système avec l'outil Lesar. Lorsqu'elles ne sont pas vérifiées, vous expliciterez le contre-exemple fourni.
Modélisation
de systèmes indéterministes et/ou asynchrones (d'après
[JHRNL 07))Les systèmes décrits en Lustre ou Esterel sont généralement déterministes et synchrones : pour une séquence d'entrée définie, le système ne produit qu'une unique séquence de sortie, et chaque réaction à une nouvelle entrée effectue le calcul des sorties en temps nul. Ces hypothèses facilitent grandement l'écriture des comportements des systèmes et leur analyse, mais elles deviennent de moins en moins justifiables dans le contexte des systèmes embarqués actuels : le contrôle applicatif est généralement distribué sur différentes parties du système, certaines étant cadencées sur des horloges différentes ; les communications entre différentes parties ne sont pas effectuées en temps nul ; le mécanisme de broadcast ne délivre pas l'information au même instant pour tous les composants du système.
On s'intéresse ici aux possibilités de modéliser ces phénomènes dans le formalisme synchrone. Cela permet de modéliser une architecture plus proche de sa réalisation physique, tout en bénéficiant des outils de génération de code et de vérification développés autour de ces langages.
L'indéterminisme d'un composant est modélisé en ajoutant des entrées supplémentaires, libres, appelées oracles. Ces oracles contrôlent les choix non-déterministes ou permettent l'affectation de valeurs non déterministes. (précision : Le noeud Lustre est déterministe vis à vis de l'ensemble de ses entrées, incluant les oracles; ce sont les choix effectués selon les valeurs des oracles qui représentent l'indéterminisme du système)
On considère un environnement pouvant produire les signaux set et reset. L'environnement le plus général sera modélisé par deux variables libres set et reset. On suppose que l'environnement ne peut jamais positionner simultanément set et reset à 1; même lorsqu'il est contraint, l'environnement est indéterministe. Un noeud lustre représentant cet environnement est donné ci-après:
node env(S,R : bool; o : bool) returns (set,reset : bool);
let
set = if S and not R then 1
else if S and R then o
else 0;
telle noeud prend en entrée les variables libres S et R à contraindre, un oracle o, et produit les signaux set et reset tels qu'ils ne sont jamais simultanément à 1. Il n'est fait aucune hypothèse sur le passé de S et R; il n'y a aucune priorité donnée à S ou R.
Question 1 : Assurez-vous que le noeud lustre respecte bien la contrainte, et qu'à chaque instant il peut générer les trois configurations <set=0,reset=0>, <set=1,reset=0>, <set=0,reset=1>
Question 2 : Pouvez-vous exprimer cette propriété avec un observateur, pourquoi ?
L'asynchronisme des systèmes correspond au fait que tous les composants n'exécutent pas leurs actions à chaque instant. Les langages Lustre et Esterel disposent de constructions permettant de bloquer l'exécution d'un composant : en Lustre, l'évaluation d'un noeud peut être conditionné à la valeur d'une horloge; en Esterel, l'instruction suspend suspend l'exécution du processus courant.
En pratique, l'utilisation des horloges de Lustre introduit la notion de valeur absente, qui complexifie la modélisation et l'analyse des systèmes plutôt que de la simplifier. Un mécanisme plus simple a été proposé (et est implanté dans Scade) : les conditions d'activation.
Aux composants qui ne sont pas évalués à tous les instants on adjoint une condition d'activation. L'évaluation du composant C conditionnée par l'expression (booléenne) b est définie comme suit :
A chaque tick de l'horloge de base,
si b = true, alors les sorties et état sont mis à jour conformément aux fonctions de transition et de génération de C;
si b = false, alors les sorties et état de C restent inchangées (mais ne sont pas absentes).
Le noeud lustre représentant l'activation sporadique d'un composant C sur une condition d'activation b est décrit ci-après :
node activ_C(b : bool;i : int) returns (o :int);
let
o = current(C(i when b));tel
On souhaite réaliser un ordonnanceur permettant de déclencher sporadiquement deux composants distincts C1 et C2, n'ayant pas d'interaction interne. On part d'un noeud instanciant C1 et C2; leur évaluation est synchrone sur l'horloge de base.
node main(x,y : int) returns (o1,o2 : int);
let
o1 = C1(x);
o2 = C2(y);
telQuestion 2 : Modifiez l'ordonnanceur pour activer l'exécution de deux composants C1 et C2 de façon non déterministe et potentiellement différente pour chaque composant. Indication : vous introduirez deux signaux de déclenchement supplémentaires, S et R sur l'interface du noeud main, modifierez et instancierez activ_C.
Question 3 : Montrez que le graphe des états accessibles du système correspond au produit asynchrone des composants C1 et C2 : vous choisirez des modèles de C1 et C2 suffisamment simples pour représenter leur produit.
Question 4 : Que faut-il modifier au système décrit ci-dessus pour imposer un asynchronisme strict (au plus un seul composant s'exécute à chaque instant) ? Quelle repercussion cela induit-il sur le graphe des états accessibles ? Effectuez la modification et vérifiez la composition asynchrone stricte.
Certains traitements ou mécanismes de communication ne sont pas instantanés. Lorsque chaque délai de traitement et communication est défini dans un intervalle [l,u] (l et u étant exprimés en nombres de ticks d'horloge), on peut le représenter dans le modèle synchrone comme un retard pur.
On considère un composant C, activé sur une condition b et produisant son résultat de calcul dans un intervalle [l,u]. Ce système est modélisé par un composant C, produisant son calcul à l'instant de son activation, et suivi par un composant retard, filtrant le résultat du calcul de C d ticks après l'instant d'activation de C. d est choisi aléatoirement entre l et u.
Question 1 : Modélisez le noeud lustre du choix de d émis entre l et u ticks après l'activation. On supposera qu'il n'y a pas de nouvelle activation tant que u tick au moins ne se sont pas écoulés. L'interface du noeud est la suivante :
node retard(b : bool; l,u : int ; o : bool) returns (d : bool);
b est la condition d'activation du noeud C, l et u les bornes de délai, o l'oracle, d la condition d'activation du filtre. En outre, vous pourrez utiliser les variables suivantes :
st : état courant du noeud retard,
cpt : nombre de ticks écoulés depuis la dernière occurrence de b,
emis : indicateur d'emission de d depuis la dernière occurrence de b.
Question 2 : Modélisez le noeud lustre du composant avec retard bi-borné. L'interface du noeud est la suivante : en plus des paramètres précedemment nommeés, i désigne les paramètres d'entrée de C et res ses paramètres de sortie.
node bi_bounded_delay(b : bool; i : int; l,u : int; o : bool) returns (res : int);
Question 3: Montrez que si C est activé une fois à l'instant t, alors son résultat sera produit à t' \in [t+l,t+u] (pour des valeurs particulières de l et u).
Question 4 : Que se passe-t-il si C est réactivé avant que son calcul précédent n'ait été émis ? Est-ce un problème ? Dans l'affirmative, quelle solution peut-on apporter à ce problème ?
Les systèmes multiprocesseurs embarqués sont structurés selon plusieurs domaines d'horloges différents. Chaque processeur et son environnement immédiat (caches / mémoire locale ...) dispose de sa propre horloge, de période T. Des phénomènes de dérive et de gigue peuvent apparaitre : au fil du temps, du fait des conditions de température non homogène ..., la fréquence d'une horloge ou la vitesse d'acheminement des fronts varie sensiblement. On considère que l'horloge est de période T +/- epsilon avec epsilon << T. En général, les horloges des différents processeurs sont toutes cadencées à la même fréquence, mais du fait de la variabilité décrite ci-dessus, la différence de période de deux horloges peut dériver de façon non bornée.
La figure 1. (issue de [JHRNL 07]) montre comment on peut modéliser la dérive bornée de deux horloges. Dans ce modèle, une horloge peut prendre de l'avance (resp. du retard) par rapport à l'autre, mais cette avance (resp. ce retard) est bornée. Un ordonnanceur Sched construit des conditions d'activation CP et CQ non déterministe et respectant la contrainte de quasi-synchronisme. Pour réaliser ces conditions d'activation, Sched dispose de deux oracles OmegaP et OmegaQ. La condition de quasi-synchronisme des conditions d'activation s'exprime comme suit :
Entre deux activations successives de P (resp. Q) , il y a au plus deux conditions d'activation de Q (resp. P).
La figure 2. montre un entrelacement possible des conditions d'activation de P et Q.
Question 1 : Représentez l'automate de Sched et codez-le dans un noeud Lustre.
Question 2 : Utilisez Sched pour synchroniser les composants C1 et C2 définis à l'étape 2.2.
Question 3 : Vérifiez que les activations des composants C1 et C2 respectent bien la relation de quasi-synchronisme.
[1] Vous pouvez aussi télécharger
Lustre (pour plates-formes GNU/Linux,
x86) à l'URL suivante:
http://www-verimag.imag.fr/~raymond/edu/distrib/linux/index.html
[JHRNL 07] E. Javier, N. Halbwachs, P. Raymond, X. Nicollin, D. Lesens. Virtual Execution of AADL Models via a Translation into Synchronous Programs. Proc of 7th IEEE international conference on Embedded Software, 2007.
[McMillan 93] K. McMillan, Symbolic Model Checking, Kluwer, 1993.