Travaux pratiques ETR 2015

Cette page décrit les travaux pratiques avec IMITATOR à l’École temps-réel 2015. L’interface graphique utilisée est la plate-forme CosyVerif.

La présentation des automates temporisés paramétrés et de IMITATOR (effectuée à ETR) est disponible en PDF ici.

0) Lancement de CosyVerif

La plate-forme CosyVerif est une plate-forme regroupant de nombreux outils de vérification au sein d’une interface graphique unifiée. Elle est constituée d’un client graphique (Coloane) et d’un serveur (Alligator). Dans le cadre de ce TP, tout est regroupé au sein d’un bundle unique, qui se lance de façon graphique, et n’intègre que l’outil IMITATOR afin de garder une taille raisonnable.

Lancer CosyVerif
Attendre que l’éditeur graphique (Coloane) se lance
Créer un projet : File > New > Modeling Project… > laisser le nom par défaut > Finish

1) Vérification d’un passage à niveau

Nous considérons un passage à niveau avec la spécification suivante.

Un capteur est installé à une certaine distance en amont du passage à niveau; le temps entre le moment où le train active le capteur (action approach) et celui où il arrive au passage à niveau (action pass) est dApproach. Une fois que le train active le capteur, cela va enclencher la baisse de la barrière (action startDown); le temps entre le moment où le train active le capteur et celui où la barrière commence à descendre est dStartDown. Le temps entre le moment où la barrière commence à descendre et celui où la barrière est entièrement baissée (action endDown) est dGetDown.

Si le train passe quand la barrière est déjà baissée, le système repart immédiatement dans son état initial (c'est-à-dire que la barrière remonte instantanément et le train s'éloigne aussitôt).

On suppose que des voitures, piétons ou vélos peuvent toujours passer tant que la barrière n'est pas complètement baissée. Si le train passe alors que la barrière n'est pas complètement baissée, une collision se produit (enfin, peut se produire…), et le système part dans un état crash.

L’objectif va (bien sûr) être de synthétiser des valeurs des paramètres dApproach, dStartDown et dGetDown garantissant la sûreté du système.

Ouvrir dans CosyVerif l’automate temporisé paramétré modélisant ce passage à niveau avec IMITATOR : clic droit sur votre projet (fenêtre à gauche) > New > Model… > Parametric timed automata > Next > entrer train dans File name > à la place de Empty Model sélectionner Railway barrier > Finish
Prendre connaissance du système en comprenant quel est le rôle de chaque état en relisant la description ci-dessus
Quel est l’état de contrôle qui ne doit en aucun cas être accessible ?
Que signifie à votre avis le champ initialConstraint ? (qui apparaît en bas de l’éditeur lorsque l’on clique dans la partie vide autour de l’automate)
Ouvrir la fenêtre d’analyse pour une synthèse de paramètres pour la non-accessibilité : Services > Local Alligator > IMITATOR > EF synthesis
Dans la fenêtre qui s’affiche, remplir le champ Property en y indiquant la propriété, qui devra avoir la forme « unreachable XXXX », où XXXX est l’état ne devant surtout pas être accessible.
Lancer la synthèse de paramètres pour la non-accessibilité : next > cocher votre modèle (probablement train.model) puis Finish.
Lorsque l’analyse est terminée, une fenêtre s’affiche. Le graphique du haut ne nous intéresse pas ; celui du bas représente tous les comportements accessibles, pour toutes les valeurs des paramètres. Voyez-vous l’état qui ne doit en aucun cas être accessible ? Est-ce étonnant ?
Récupérer le résultat sous forme textuel en cliquant sur next. Le résultat de IMITATOR est visible après « Final constraint such that the property is *violated* ». Quelles sont les valeurs des paramètres garantissant la sûreté de ce passage à niveau ?

2) Spécification et vérification d’une machine à café

Nous allons maintenant entrer dans Coloane la machine à café vue précédemment.

Créer dans CosyVerif un nouveau modèle : clic droit sur votre projet (fenêtre à gauche) > New > Model… > Parametric timed automata > Next > entrer cafe dans File name > Finish
Recopier le modèle de machine à café ci-dessous

Bien respecter la syntaxe suivante :
- Gardes et invariants [entre crochets]
- Réinitialisations d’horloges avec l’opérateur = (par exemple x = 0)
- Contrainte initiale : [p1 >= 0] & [p2 >= 0] & [p3 >= 0]
- Liste des horloges (champ Clocks) : liste des horloges de votre modèle séparées par des virgules
- Liste des paramètres (champ Parameters) : liste des paramètres de votre modèle séparés par des virgules
Déterminer des valeurs des paramètres telles qu’il est impossible d’obtenir un café. Pour cela, ouvrir la fenêtre d’analyse pour une synthèse de paramètres pour la non-accessibilité :
Services > Local Alligator > IMITATOR > EF synthesis
Dans la fenêtre qui s’affiche, remplir le champ Property en y indiquant la propriété « unreachable Coffee ».
Lancer la synthèse : next > cocher votre modèle (probablement cafe.model) puis Finish.
Quel est la contrainte garantissant qu’il est impossible d’obtenir un café ? Pouvez-vous l’expliquer ?
Nous allons maintenant effectuer une analyse de robustesse (en utilisant la méthode inverse [ACEF09]) :
Services > Local Alligator > IMITATOR > Inverse Method > Next > cocher votre modèle (probablement cafe.model) > Next
Dans la fenêtre qui s’affiche, remplir le champ Reference valuation of all parameters in the model. en y indiquant la valeur de référence des paramètres vue dans la présentation, à savoir :
p1 = 1
p2 = 5
p3 = 8
puis Next > Finish.
Lorsque l’analyse est terminée, une fenêtre s’affiche. Le résultat est donné en-dessous de "Final constraint K0". Ce résultat représente toutes les valeurs des paramètres pour lesquelles l’ensemble des comportements possibles est le même que pour la valeur de référence ci-dessus. Trouvez-vous ce résultat intuitif ? Combien de sucres au maximum peut-on mettre dans son café pour ces valeurs ?
(Note : en cliquant sur Next, on obtient une vue graphique (un ensemble de traces) de tous ces comportements.)

3) Exercice complémentaire : une histoire de nouilles

Après une harassante journée de travaux pratiques à ETR, un étudiant en systèmes temps-réel rentre chez lui pour cuisiner des nouilles. Il place une casserole sur une plaque de cuisson à t = 0. Au bout d'un certain temps (tout à fait arbitraire), il enclenche un minuteur (action enclenche). Le minuteur va sonner pMinuteur secondes après avoir été enclenché (action sonne).

À t = pCasserole, si le minuteur n'a pas encore sonné, la casserole va déborder (action déborde). En revanche, si le minuteur a sonné avant t = pCasserole, la casserole ne déborde pas, et les nouilles sont prêtes ! (action prêt)

Créer dans CosyVerif un nouveau modèle : clic droit sur votre projet (fenêtre à gauche) > New > Model… > Parametric timed automata > Next > entrer nouilles dans File name > Finish
Mettre au point un automate temporisé paramétré modélisant ce problème. Cet automate contiendra au plus deux horloges, contiendra uniquement les actions mentionnées ci-dessus, et contiendra uniquement les deux paramètres pMinuteur et pCasserole. Les contraintes dans les gardes (contraintes sur les transitions) et invariants (contraintes dans les états) sont nécessairement de la forme x ~ p, où x est une horloge, p un paramètre, et ~ un opérateur de comparaison appartenant à {<, <=, = , >= , >}.
Quelles sont les valeurs des paramètres garantissant que la casserole ne déborde pas ? Ce résultat est-il étonnant ? Expliquer.