TP UPPAAL : modélisation et vérification comportementale

Le but de ce TP est de vous permettre de vous exercer à la modélisation d’algorithmes concurrents et/ou temps réels via un réseau d’automates temporisés UPPAAL.

Les cas d’étude seront :

• le modèle du tourniquet pour savoir définir, simuler et vérifier un modèle (extension du cas d’étude du tourniquet vu en cours).
• la modélisation d’une synchronisation sans opération atomique (i.e. pas de verrou, test and set, etc.) via le principe d’exclusion temporelle : algorithme de Fischer.

I Prise en main d’UPPAAL et premiers pas en vérification

UPPAAL est un outil disposant d’une interface graphique pour : définir des réseaux d’automates temporisés, simuler leur comportement, et vérifier des propriétés CTL sur le réseau d’automate. Vous avez vu en cours une partie de ce qui sera illustré dans cette première partie du TP.

a) Lancement d’UPPAAL

Dans un terminal, exécutez :
export PATH=$PATH:/cal/homes/trobert/tool/uppaal
Puis lancez UPPAAL comme suit :
uppaal

b) Récupération de l’archive de tp, et import du modèle

Téléchargez l’archive tourniquet et décompressez son contenu.

Sous Uppaal,  dans la barre des menus ( File-> open system …), vous obtiendrez une fenêtre vous permettant d’ouvrir une description existante de réseau d’automates (system). En supposant le modèle syntaxiquement correct, vous pouvez dès lors le simuler ou parcourir les différentes fenêtres de l’éditeur (les templates d’automates, les déclarations de variables et instances d’automates…. zone (D)).

Action : Ouvrez le modèle tourniquet.xml

c) Interface d’édition de modèle

Figure 1 Détail de la vue d’édition (retour en II)

La figure 1 détaille le rôle de chaque zone de l’interface graphique.

• Les déclarations (D): les variables, types, constantes et événements, et canaux de synchronisation (type chan, comme par exemple l’événement push) sont déclarés dans la section Declarations du système (marqueur d1) si la déclaration est globale, de déclaration de l’automate sinon (marqueur d2 – vous devez développer le modèle en cliquant sur la puce à gauche du nom de l’automate pour accéder à sa  déclaration).
• Edition d’automate (A) : il est possible de définir des automates graphiquement. Les transitions peuvent être complétées par : des gardes, des « synchronisation », des mises à jour de variables. La convention de couleur donne la nature de chaque expression : vert = garde, bleu clair = synchro, bleu foncé = mise à jour.
• La barre d’icône : elle rassemble essentiellement les icônes servant à l’édition graphique du modèle. En particulier, vous y trouverez des outils qui permettent de sélectionner des parties de l’automate (t1) pour les déplacer, les copier / supprimer, d’ajouter des états (t2), ou des transitions (t3). Par défaut, l’outil de sélection (t1) est activé. Notez qu’une fois activée, les autres outils restent actifs (par exemple l’outil d’ajouts d’états (t2) va rester actif après avoir été sélectionné). Il faut cliquer sur l’outil de sélection (t1) pour ré-activer cet outil…

Question 1 : Via le menu Edit, insérez un nouvel automate (Insert Template) au cas d’étude du tourinquet. Nommez le boundedUser, et modélisez un automate ayant les caractéristiques suivantes :

• 2 états (état initial ReadyToEnter, le second état s’appelant Entering).
• Une variable budget entière initialisée à 10.
• une transition de ReadyToEnter vers Entering, ayant une synchronization token !
• une transition de Entering vers lui-même ayant une synchronisation token !
• une transition de Entering vers ReadyToEnter ayant uniquement une synchronisation sur push!

Modifiez la déclaration du système précédent de sorte que le réseau d’automate contienne une instance du tourniquet appelée T et une de boundedUser appelée U, pensez à vérifier la syntaxe (Tools → Check Syntax F7).

Indication Après insertion du Template, vous devez obtenir un écran similaire à celui ci :

Ce que vous savez faire à partir d’ici :
ajouter des états / transitions, définir des variables et un système.

d) Simulation et analyse du comportement

La vue de simulation n’est accessible que si le modèle est syntaxiquement correct : Uppaal sait alors instancier le réseau d’automates correspondant au système décrit. Vous pouvez accéder à la vue de simulation en cliquant sur l’onglet Simulator. Chaque partie de la vue simulateur permet d’observer efficacement différentes caractéristiques du système. Voici une petite liste de questions pour lesquelles on indique la partie du simulateur la plus susceptible de fournir l’information. Pour chaque question/réponse, la figure ci-après vous aidera à visualiser la zone de la vue du simulateur.

• Ai je bien le bon nombre d’instances et correspondent elle à l’attendu → en haut à droite
• Ai je bien déclaré, initialisé mes variables → partie centrale : donne les valeurs possibles des variables dans l’état de contrôle courant (c’est un peu plus compliqué mais l’approximation reste correcte).
• Comment puis je simuler un scénario précis d’exécution → en haut à gauche, vous pouvez réaliser un scénario de simulation pas à pas.
• Comment interpréter mon contre exemple (vous verrez plus tard) → en bas à gauche +  au centre.

Figure 3 Vue d’ensemble du panneau simulation

Question 2 Utilisez la vue de simulation sur le nouveau modèle puis contrôlez la séquence de transitions de sorte que l’utilisateur réalise une transition token !, observez l’état du réseau, puis réalisez une transition push !.

Remarques : notez que la partie centrale n’affecte pas une unique valeur au variable. Uppaal réalise ce que l’on appelle une analyse symbolique par zone. Cela veut dire qu’il regroupe tout les états en fonction de de leur capacité à activer le même ensemble de transition sur l’automate.

e) La vue de vérification

La vue vérification est structurée en 3 parties :

• une liste de formules déjà définies (en haut de la fenêtre),
• un champ pour l’édition d’une formule (au centre) et d’un commentaire la décrivant,
• et une console détaillant les opérations de vérification réalisées (en bas, notez qu’ici l’interface est assez aride et ne vous aidera pas beaucoup).

Dans ce TP, vous devrez vérifier des formules déjà définies. Il est cependant important de comprendre le résultat. Lorsqu’un contre exemple d’une formule (trace d’exécution pour laquelle la formule est évaluée à faux) peut être trouvé, la vue de simulation peut contenir le contre-exemple trouvé.

Question 3 : Chargez la formule contenue dans tourniquet_cours.q (via le menu File ->open queries), configurez l’outil pour qu’il engendre des contre-exemples au cas où la formule serait fausse (Menu Options→ Diagnostic Trace → choix « some »). Puis, vérifiez la formule. Si vous ne la comprenez pas lisez le texte la décrivant. Le résultat issu de la vérification est-il normal ? Pouvez vous expliquer le résultat ?

Aide pour l’interprétation du contre exemple :
La formule devant être « évaluée » sur une trace infinie la fin de la trace doit être répétée. La « fin » répétée sera colorée en rouge dans la version textuelle de la trace. Si la partie en rouge se limite à un état de contrôle, cela signifie que l’on restera indéfiniment dans cet état. Si elle contient une transition suivi d’un état, cela signifie que l’on bouclera indéfiniment sur (état.transition).

Solution / Explication des résultats

T.unlocked → T.locked paraît facile à vérifier… cependant, cette formule acceptera un contre exemple. Ce dernier est considéré comme un artifice de modélisation très connu dans la modélisation de systèmes temps réel : les comportements zeno. Cela correspond à pouvoir enchaîner une infinité de fois la transition token instantanément. Le verifieur considère au pied de la lettre le modèle que vous lui avez donné. Il faut se rappeler que certains modèles physiques utilisent l’hypothèse zeno et que leur modélisation possède un intérêt pratique (e.g. une balle rebondissant fini par rebondir infiniment souvent à une hauteur infiniment petite). Pour éviter ce cas, il faut soit borner le nombre d’itérations de « token ! » soit fixer une borne minimale sur la durée entre deux transitions de l’utilisateur, soit admettre que ce comportement est acceptable malgré l’absence de progression.

Question 4 : Utilisez la variable entière budget que vous avez défini pour éliminer le comportement aberrant en vous assurant que :

• l’utilisateur ne peut franchir de transition émettant token! que si budget est positif,
• il décrémente budget de 1 chaque fois qu’il émet token!.
• la propriété T.unlocked → T.locked soit vérifiée par le système.

Ce que vous savez faire à partir d’ici :
simuler le comportement des automates, configurer la vérification pour obtenir des contre-exemples, vérifier une formule et analyser le résultat

II Algorithme de Fischer

Comme vous l’avez vu, il est facile de commettre des erreurs de modélisation pouvant mener à des verdicts incorrects sur le comportement du système concret (à cause d’une erreur de modélisation). Nous allons dans cette section aborder la modélisation de programmes s’exécutant de manière concurrente et partageant des données. La vérification se fera sur les états atteints par les programmes, ainsi que leur synchronisation.

Nous verrons qu’une manière d’élaborer le modèle pour un tel système consiste à fixer des règles traduisant des structures syntaxique du langage de programmation en élément de l’automate. Avant cela, nous vous encourageons à lire le petit rappel sur les différents types d’algorithmes existant pour réaliser la synchronisation.

La synchronisation peut s’implémenter de différentes manières en fonction des hypothèses que l’on accepte de faire.

a) Principe de fonctionnement de Fischer

Le principe de l’algorithme repose sur une attente active avec une « pause » (ici noté sleep (delay)). L’idée est que chaque processus va tenter de dire qu’il veut être le suivant à entrer dans la section critique (en indiquant son identifiant dans une variable partagée, par exemple has_cs) :

• si un processus est déjà en attente, le processus courant doit attendre avant de pouvoir déclarer son intention de rentrer.
• sinon, il indique qu’il veut rentrer et attend un délai
• puis il vérifie qu’il est bien toujours identifié comme le prochain à avoir accès à la section critique. Si c’est le cas, il y rentre; sinon il revient au début.

Le mécanisme de délai et de saut en arrière est utilisé pour « corriger » une data race sur la variable servant à réaliser le verrou (has_cs). Ceci assure le bon fonctionnement de l’algorithme.

Important : l’initialisation de la variable partagée est toujours une question difficile. Dans un premier temps, nous ignorerons cette difficulté : UPPAAL initialise toutes ses variables à 0 sauf indication contraire. Pour faire court, nous distinguerons la valeur par défaut de la variable (que l’on ne maîtrise pas forcément) et son initialisation (affectation réalisée par le système). Voici deux cas où l’initialisation de has_cs pourrait être problématique (même en supposant une valeur par défaut de 0) : initiation à une valeur ne correspondant à aucun ID de processus, initialisation à 0 ou un ID quelconque de processus alors qu’un processus a déjà atteint la section critique…

Processus N°i:

L0 : if (has_cs != 0) { goto L0;}
L1 : has_cs=i;
L2 : sleep (delay);
L3 : if (has_cs != i) {goto L0;}
L4 : ... //cs
...
Lk : ... //cs
L(k+1) : has_cs =0; // libération du verrou

b) Du code au modèle

Pour éviter des erreurs de modélisation et construire un modèle relativement homogène, il est usuel d’appliquer des règles de traduction ou de création de l’automate. Nous allons ici énoncer un ensemble de règles qui nous permettons de créer un modèle d’automate pour les processus.

1 – les paramètres
Tout d’abord, les automates doivent pouvoir être paramétrés par leur identifiant. Toute variable propre à une instance devra être déclarée de la même manière : via le champ Parameters.
Dans notre cas, nous avons besoin de définir un entier servant d’identifiant (ID) pour chaque instance de processus qui sera crée.
Les paramètres sont forcément des constantes : ajouter « const myID ID » dans le champ paramètre nous permettra de définir l’id de chaque processus.

2 – Identifier les état de contrôle (première phase)

Un principe de base est que les états de contrôle identifient les actions réalisables. Chaque ligne de code correspondant à un statement complet de C pourra se voir attribuer un état de contrôle propre à partir duquel des transitions modéliserons l’impact de l’exécution du statement. Cet état permettra de définir l’état de l’automate durant la période où l’instruction peut s’exécuter (ou est en cours d’exécution).
Le cas des structures plus complexes (if {};, while(){};, …) ou d’expressions (à droite d’une affectation) ayant un effet de bord pourront nécessiter plus de travail.

3 – Des transitions qui modélisent la fin de l’exécution d’une instruction

Le cas le plus simple est celui d’une affectation d’une constante à une variable, e.g. « l1 : var=10; ». Suite à l’exécution de cette variable, l’état de contrôle sera celui de l’instruction suivante (i.e. la transition va de l’état l1 à celui de l’instruction suivante, et la transition porte la mise à jour var =10). Notez que l’on suppose l’action atomique mais l’action peut prendre du temps (ce temps sera estimé comme celui passé en l1). Si vous souhaitez borner ce temps, il faudra ajouter une horloge, des invariants et des gardes.

Exécution atomique vs Exécution non atomique

le cas d’une instruction x = v++; est très particulier. En suivant, les règles ci dessus on serait tenter de n’utiliser pour cette instruction qu’un seul état de contrôle et une seule transition. Cependant, si x et v sont partagées entre plusieurs processus, cette modélisation ne permettrait pas d’identifier une condition de data race. Il est donc déconseiller de modifier plusieurs variables entières sur une même transition pour une vérification de comportement concurrent.

3 – Modélisation de contraintes temporelles

On peut identifier 2 types de contraintes temporelles : des contraintes logiques bloquantes, et des obligations de progression. L’obligation de progression correspond au fait que l’automate n’ait pas le droit de ne rien faire indéfiniment (cf. l’exemple du tourniquet qui ne doit pas rester indéfiniment ouvert). Le premier type de contraintes sera modélisé par des gardes sur les transitions, le second sera modélisé par des invariants.

Attention l’algorithme de Fischer repose sur une hypothèse de progression (le temps pour compléter chaque instruction est borné (e.g. par une constante C), et l’exécution de l2 ne peut durer moins de delay unités de temps. Nous modéliserons cela en considérant que C et delay sont des constantes.

c) Passons à la pratique….

Nous allons traiter tout d’abod le cas if (condition) {statementblock}. Cette instruction a deux conséquence possibles : (i) dans le cas ou la condition est fausse, on doit franchir une transition vers l’état de contrôle représentant l’instruction situé à la fin du statementblock ou (ii) exécuter statementblock qui se traduit par une transition vers le premier état de contrôle de de statementblock.

Si l’on note que le statement goto fait un branchement sans affecter les variables d’état, on modélise son exécution en créant une transition vers l’état de contrôle correspondant au label pointé par le goto.

En appliquant ces raisonnement nous avons modélisé L0 dans fisher-tpt.xml que vous trouverez dans cette archive : fischer-tpt.

La description du système contient une variable partagée int has_cs (initialisé à zéro), et un template appelé « Proc » ayant un paramètre :ID. Nous avons créé pour vous les états de contrôle nécessaires à la traduction du code mais pas les transitions.

Question 5: Complétez ce modèle en vous aidant des règles énoncées ci-dessus (vous avez le droit de rajouter des états de contrôle mais réfléchissez bien avant).

Assurez vous de capturer les éléments suivants :

• Contraintes temporelle de progression : le système ne peut attendre plus de C (constante égale à 4 par exemple) avant de compléter l’exécution d’une instruction (hors sleep), ou de démarrer l’attente de delay unité de temps pour le sleep.
• Contrainte temporelle bloquante : le processus ne peut réaliser l3 que si delay unité de temps se sont écoulées au moins entre le démarrage de l’attente et l’entrée dans l3.

Demandez des conseils pour la réalisation de l’automate si vous êtes bloqués !!

Question 6: Nous vous avons fourni une propriété à vérifier sur Ficher

Essayez de vérifier cette propriété… Il semblerait que le problème vienne d’un mauvais « réglage » de fischer.

Question 7: Trouvez une combinaison satisfaisant la propriété

Ce que vous devriez savoir faire à partir d’ici :

Coté maîtrise de l’outil UPPAAL :

• définir des types bornés, paramétrer un automate,
• Définir des transitions complexes impliquant guardes et update, utiliser plus d’une horloge

Coté savoir faire générique en modélisation

• Appliquer des règles de modélisation
• Distinguer les éléments du modèle correspondant au « code » des éléments correspondants aux hypothèses de correction de l’algorithme.
• Supprimer les comportement zeno non souhaité, vérifier une propriété d’équité.
• Instancier un modèle ayant un nombre paramétrable de noeuds identiques

III Problème : preuve d’équité

Un utilisateur dit que fischer n’est pas équitable si les processus sont en fait des boucles (ie une fois sortie de la section critique, ils reviennent en L0) ou bien qu’une infinité de processus peut être instanciée (non vérifiable en uppaal, on se concentrera sur le premier cas…)

• Introduisez la(les) transition(s) et/ou état(s) nécessaire(s)  à l’ajout d’une boucle « while (1) [ …} » autour du pseudo code des processus modélisés.
• Vous utiliserez la propriété suivante pour évaluer l’équité de l’algorithme de synchronisation pour le processus nommé Process(1) et dans le cas où l’état L4toLk modélise les états de la section critique : Process(1).L0 –> Process(1).L4toLk

Il prétend qu’il est impossible de prouver cette propriété si le temps passé en section critique n’est pas borné. (Notez que la famine est définie en supposant ce temps borné).

Commentez cette affirmation 

Ajouter une borne sur le temps passé en section critique, et commentez le résultat de la vérification dans ce cas (i.e. contre exemple)

Il prétend que le problème pourrait être réglé en ajoutant soit une contrainte de temps pour le retour à l’état L0, soit une variable d’état par processus qui serait partagée et permettrait d’implémenter l’équité.

Proposez une solution dans le cas avec contrainte temporelle de retour et commentez le résultat ? (Notamment on commentera les performance de cette solution en terme de nombre de fois où l’on peut accéder à la section critique par unité de temps). Y a til un lien entre les constantes de temps utilisées et le nombre de processus en exclusion mutuelle.

Proposez une solution dans le cas reposant sur une variable partagée pour deux processus qui permette de limiter le cas où un processus est en attente à 5 passage dans la section critique de l’autre processus (i.e. on borne le nombre de fois où le processus se fait « doubler » à 5 fois)

Utilisez UPPAAL pour répondre à ces questions.