Ce TP vise deux objectifs : vous familiariser avec la description d'un système par un automate temporisé, vous faire découvrir l'outil de vérification UPPAAL. Il est fortement inspiré des exemples fournis comme exemples pour illustrer l'usage du Model-Checker.
Une copie d'UPPAAL se trouve dans l'archive uppaal.tar.gz.
Une fois décompressé, vous pouvez lancer le programme principal
par la commande suivante java -jar uppaal.jar.
Pour commencer, chargez le système décrit dans le fichier Etude de cas 1 (File -> Open System). Cette étude de cas est une modélisation d'un contrôleur d'accès assez à une variable partagée. Cette modélisation reste simpliste car nous ne modélisons pas la file d'attente des processus cherchant à acquérir la ressource. Dans notre modèle, tant que les processus n'ont pas la possibilité d'acquérir la ressource, ces derniers restent dans l'état "Safe". Nous allons poursuivre la description du modèle en détaillant chaque élément et son rôle.
Nous allons détailler la sémantique de chacun des deux types d'automates. Cette description est destinée à renforcer la présentation des automates temporisés faîte en cours.
Un modèle UPPAAL est constitué de 3 parties : Des déclarations de constantes et des canaux de communications, la déclaration des automates, et la déclaration des composants du système étudié.
SI l'on prend l'exemple du projet RcontrolA.xml, la constante N définie dans la section Projet est utilisée pour borner la taille du système étudié
Cette section contient aussi la déclaration des canaux de communication get de 0 jusqu'à N-1.
La section Template contient la description du comportement d'un "composant" du système sous la forme d'un automate temporisé. Un automate temporisé est une extension d'une machine à état finie. La structure de base de l'automate reste un graphe décrivant des chemins d'exécution possibles.
Les noeuds sont appelés des lieux ou 'locations' en anglais. L'un de ces lieux est identifié comme le lieu initial d'où démarre toute exécution de l'automate (double cerclage). L'espace d'état de l'automate est étendu par un ensemble de variables déclarée dans la section "Declarations" de chaque partie du modèle. Il existe trois types primitifs relativement incontournables : les horloges, les entiers et les booléens.
Le type d'une variable peut être restreint à un sous-domaine de son type de base : int[0,6] représente tous les entiers entre 0 et 6.
///// Déclaration au niveau Projet (permet de borner le type de système étudier
/*
* Exemple de système dérivé du case study railroad crossing de UPPAAL
* Déclaration des identifiants de thread + des canaux entre chaque thread
* et le controleur
*/
const int N = 4; //# threads
typedef int[0,N-1] id_thread;
typedef int[0, N-2] fair_thread;
chan get[N], release; // de N canaux indépendants pour
//l'acquisition et un seul canal pour le retrait
//// Déclaration au niveau de l'automate Rcontrol
bool lock;
id_thread owner;
clock timeout;
// Put an element at the end of the queue
void Lock_get(id_thread element)
{
owner=element;
lock=true;
}
void Lock_release()
{
lock=false;
}
|
Sur la figure ci-dessous :
Free et Used.
Free
evt ! signifie un envoi, evt ? une réception.
thread_acquiring_R dont la valeur est parmi 0 ... N-2. Ce sélecteur va nous permettre de savoir quel automate Thread est en train de prendre la ressource.
Allez dans la section simulation et animez l'automate en cliquant sur le bouton next.
Vous pouvez consulter une description plus détaillé de la syntaxe des architectures de systèmes dans la section système de l'aide intégrée au logiciel.
Uppaal fournit principalement deux services : un service de simulation, et un service de vérification de propriétés.
Chaque service est accessible par l'onglet associé au centre de la fenêtre du logiciel.
Avant de pouvoir passer aux phases de simulation ou vérification, l'outils procède à une vérification de la cohérence du modèle qui va au delà de la simple cohérence syntaxique puisque l'outils vérifie aussi que les canaux de communication sont correctement connectés.
La phase de simulation permet d'animer l'exécution du système à partir des différents états initiaux du système. Ce mode est intéressant puisqu'il permet l'exploration des comportements possible du système et permet d'enregistrer les traces "d'intérêt".
Le service de vérification permet, quant à lui de faciliter la preuve de propriétés exprimées en logique temporelle sur les états de l'automate.
La notation est légèrement différente de celle vu en cours puisque la logique manipulée par UPPAAL est légèrement plus expressive. UPPAAL utilise la logique CTL et des formules sur les horloges pour exprimer des contraintes comportementales sur les systèmes temps-réel. (CTL: computational Tree Logic).
Cette logique permet de raisonner non pas sur une trace mais sur toutes les traces possibles.
On distingue les opérateurs de branche (A et E) des opérateurs temporels <> et [].
Nous vous donnons les interprétations pratique de chaque opérateur, puis leur intéprétation formelle sur l'ensemble des chemins d'exécution C parcourables depuis un état s dans un automate donné :
La liste complète des propriétés d'état que vous pouvez spécifier est décrite dans l'aide d'UPPAAL. Notez l'existence d'un prédicat relativement important "deadlock" qui permet de tester si une architecture peut se bloquer (se placer dans un état à partir duquel plus aucune transition n'est tirable.
ouvrez le fichier Rcontrol-Queries.q qui contient deux formules exprimées dans la logique de l'outil. Un commentaires est associé à chaque formule pour vous aider à en comprendre le sens.
Le premier exercice vise à poursuivre la prise en main de l'outil UPPAAL et vous faire réfléchir sur l'utilisation d'un model-checker.
L'ensemble du système décrit deux thread qui accèdent à la ressource partagée en exclusion mutuelle l'un de l'autre. Nous avons défini deux formules à vérifier sur ce système.
Réaliser la vérification de ces formules. Si une formule est fausse servez vous du simulateur pour trouver une trace pouvant servir de contre exemple. (L'outil de diagnostic vous permet de sélectionner les transitions tirables au fur et à mesure. Une transition spéciale indique le risque de verrouillage du système.
Il est possible de contrainte d'avantage la dynamique des automates en forçant l'automate à sortir d'un lieu donné. Les invariants de lieux permettent de borner la valeur maximale acceptable pour des horloges choisies. Vous pouvez définir un tel invariant en double cliquant sur un lieu de l'automate.
Utilisez un invariant pour vous assurer que votre système ne risque plus de verrouillage.
Ce modèle de contrôleur fonctionne en supposant que les thread "jouent" la règle du jeu et ne tentent pas de pousser le contrôleur à penser, à tort, que la ressources et de nouveau libre.
Notez la présence d'un deuxième type de thread dans la description du projet. Allez dans la section "System declarations" pour commenter la première ligne et décommenter la seconde. La seconde ligne correspond à une autre architecture.
Modifiez le modèle du second type de thread pour éviter le verrouillage de la même manière que pour les autres thread. (Attention l'état Process à deux transition entrante cette fois-ci).
Ce modèle de thread a une particularité propre au modèle d'automates temporisés d'UPPAAL : les lieux dit urgents. Il faut les voir comme des états où il est impossible au système d'attendre. Ainsi, toutes les valeurs d'horloges sont bloquées. Soit une transition est franchissable soit l'automate est bloqué.
Vous devez être capable de comprendre la signification des transitions rajoutées. Que se passe-t-il lorsque ce thread a attendu plus de 100 unités de temps dans l'état Safe ?
Ce scénario n'est pas totalement factice puisque les mutuxes POSIX peuvent être utilisés de telle sorte qu'un thread peut déverrouiller un verrou sans l'avoir pris au préalable.
Revérifiez les propriétés associées au modèle
Modifiez le modèle pour que l'on soit capable d'identifier l'émetteur de l'événement release. A partir de la, vous pourrez utiliser une garde pour vous assurer que seul le détenteur de la ressource puisse la libérer lorsqu'elle est utilisée. Complétez l'ensemble du modèle pour que la propriété 1 soit à nouveau vraie.
Grâce à la possibilité de définir des variables internes aux automates, il est possible de représenter un mécanisme de contrôle d'accès légèrement plus réaliste : une file d'attente FIFO. La description de ce mécanisme est dans le fichier RcontrolB.xml
Consultez le section Project -> Declaration pour identifier les nouveaux canaux de communication (en particulier entre la file et le gestionnaire de la ressource.
Le principe de la file d'attente est le suivant :
Vérifiez la propriété 1. Quelle erreur a été commise ? Combien les thread devraient ils avoir de lieux bien distincts ?.
Indice : est ce que le thread possède réellement la ressource juste après avoir fait get ! ?
Modifiez l'architecture du système pour mettre en place une description plus adaptée du comportement des threads. Vérifiez votre conception.