Model Checking in Automata

Ce laboratoire porte sur la vérification de modèles (model checking) appliquée à des automates et systèmes discrets. Il propose plusieurs exercices pratiques visant à modéliser des systèmes sous forme d'automates ou de structures de Kripke, à exprimer des propriétés en logique temporelle CTL, puis à vérifier ces propriétés à l'aide d'algorithmes de marquage. Ce TP nécessite des connaissances de base en automates, logique temporelle et structures de Kripke.

Objectifs

• Transformer un automate en une structure de Kripke.
• Exprimer des propriétés système en logique temporelle CTL.
• Vérifier la satisfaction de ces propriétés par le modèle via l’algorithme de marquage.
• Modéliser des systèmes avec variables d’état et conditions (gardes).
• Appliquer la méthode à des exemples concrets : digicode, robot de transport, gestion d’un tunnel.

Prérequis et mise en place

• Connaissance des automates finis et des structures de Kripke.
• Maîtrise de la logique temporelle CTL (Computation Tree Logic).
• Outils de modélisation et vérification formelle compatibles avec les algorithmes de marquage CTL.
• Matériel : ordinateur avec environnement de modélisation et vérification.

Exercice 1 : Digicode

Dans cet exercice, on modélise un digicode sous forme d’automate puis on le transforme en structure de Kripke. L’objectif est de vérifier une propriété temporelle sur les séquences de lettres tapées, et d’étendre le modèle pour gérer un nombre limité d’erreurs avec déclenchement d’alarme.

Étape 1 : Transformation de l’automate en Kripke

On part d’un automate avec états {1, 2, 3, 4} et alphabet {A, B, C} avec transitions :

T = {(1,A,2), (1,B,1), (1,C,1), (2,A,2), (2,B,3), (2,C,1), (3,A,4), (3,B,1), (3,C,1)}

Les états sont étiquetés par des propositions atomiques :

• pA : la dernière lettre tapée est A
• pB : la dernière lettre tapée est B
• pC : la dernière lettre tapée est C
• PO : porte ouverte

La fonction d’étiquetage l est définie par :

l(1) = {PF}
l(2) = {pA, PF}
l(3) = {pB, PF}
l(4) = {pA, PO}

Le Kripke K est donc défini par :

Q = {1, 2, 3, 4}
q0 = 1
T = transitions ci-dessus
E = {A, B, C}
l = fonction d’étiquetage ci-dessus

Étape 2 : Expression de la propriété temporelle

La propriété P à vérifier est :

« Toute suite de lettres tapées finissant par ABA ouvre la porte ».

Elle s’écrit en logique temporelle CTL :

P : G (X pA ∧ XX pB ∧ XXX pA ⇒ XXX PO)

où G est le quantificateur universel global (toujours), X est l’opérateur « au prochain état ».

Étape 3 : Vérification de la propriété

On vérifie si K satisfait P, noté K |= P, en appliquant l’algorithme de model checking sur la structure de Kripke et la formule CTL.

Étape 4 : Extension du modèle pour tolérer des erreurs

On modifie l’automate pour :

• Permettre jusqu’à trois erreurs (lettres incorrectes) tolérées.
• Déclencher une alarme dès la quatrième erreur.

Pour cela, on introduit une variable d’état ctr (compteur d’erreurs) et on ajoute des gardes et affectations :

• Les transitions correspondant à une erreur sont gardées par la condition ctr < 3 et incrémentent ctr.
• Lorsque ctr = 3, les transitions provoquent l’alarme et incrémentent ctr.

Exemple de transitions avec gardes :

Si ctr < 3 et lettre tapée ∈ {B, C} alors ctr := ctr + 1
Si ctr = 3 et lettre tapée ∈ {B, C} alors ctr := ctr + 1 (alarme)

Cette extension permet de modéliser précisément la gestion des erreurs dans le digicode.

Exercice 2 : Robot de transport de pièces

Le but est de modéliser un système robotisé composé de trois dispositifs :

• Da : arrivée des pièces (ignoré pour simplification)
• Dt : dispositif de transport avec pince
• De : dispositif d’évacuation où Dt dépose les pièces

On s’intéresse uniquement à l’introduction de la pièce dans Dt et à sa sortie sur De, sans modéliser la pince.

Étape 1 : Construction de la structure de Kripke

On définit les états :

• e0 : Dt libre, De libre
• e1 : Dt chargé, De libre
• e2 : Dt libre, De occupé
• e3 : Dt chargé, De occupé

Les propositions atomiques sont :

• DtL : Dt libre
• DeL : De libre
• chargt : Dt chargé
• Déchargt : Dt déchargé
• Evac : évacuation en cours

Étape 2 : Expression de la propriété à vérifier

La propriété Pr est :

« Si le dispositif Dt décharge, alors De est libre ».

Elle s’écrit en CTL :

Pr : AG ((¬DtL ∧ EX DtL) ⇒ DeL)

où AG signifie « pour tous les chemins, toujours », EX signifie « il existe un chemin où au prochain état ».

Étape 3 : Vérification de la propriété

On décompose Pr en sous-formules :

• P1 = ¬DtL (cas 2)
• P2 = EX DtL (cas 4)
• P3 = P1 ∧ P2 (cas 3)
• P4 = P3 ⇒ DeL = ¬(P3 ∧ ¬DeL)
• P41 = ¬DeL (cas 2)
• P42 = P3 ∧ P41 (cas 3)
• P4 = ¬P42 (cas 2)
• P51 = true (cas 1)
• P52 = E (P51 U P42) (cas 5)
• Pr = ¬P52 (cas 2)

On applique ensuite l’algorithme de marquage CTL sur les états de la structure de Kripke. Si l’état initial est marqué par Pr, la propriété est satisfaite.

Exercice 3 : Tunnel étroit pour trains

On modélise un tunnel de montagne très étroit où un seul train peut passer à la fois. Deux trains circulent et échangent des signaux avec un médiateur informatique. Les signaux sont :

• attente : demande d’autorisation d’entrée
• entrée : autorisation d’entrer dans le tunnel
• sortie : sortie du tunnel

Chaque signal est indexé par le numéro du train (1 ou 2).

Étape 1 : Construction de l’automate

On construit un automate avec états représentant les situations des trains :

• ni : train i neutre
• ai : train i en attente
• ti : train i dans le tunnel

Les transitions modélisent les changements d’état selon les signaux échangés.

Étape 2 : Expression des propriétés CTL

• Sûreté : Les deux trains ne traversent jamais le tunnel en même temps :

AG ¬(t1 ∧ t2)

• Vivacité : Un train en attente finit toujours par traverser :

AG (a1 ⇒ AF t1) ∧ AG (a2 ⇒ AF t2)

• Non-blockage : Un train qui est sorti peut toujours se remettre en attente :

AG (n1 ⇒ EX a1) ∧ AG (n2 ⇒ EX a2)

Étape 3 : Vérification des propriétés

On applique l’algorithme de marquage CTL sur l’automate construit pour vérifier chacune des propriétés exprimées. La satisfaction est déterminée en observant le marquage des états initiaux.

Résultats attendus

• Dans l’exercice du digicode, la propriété P doit être satisfaite par le Kripke initial. Après extension, la gestion des erreurs doit être correctement modélisée avec incrémentation du compteur et déclenchement d’alarme.
• Pour le robot de transport, la propriété Pr doit être vérifiée, indiquant que le dispositif d’évacuation est libre lorsque Dt décharge.
• Dans le modèle du tunnel, les propriétés de sûreté, vivacité et non-blockage doivent être validées, garantissant la sécurité et la bonne gestion du trafic des trains.

Pièges courants

• Confondre les opérateurs temporels CTL (AG, EX, AF) et leur portée dans la formule.
• Oublier d’inclure les gardes (conditions) sur les variables d’état lors de la modélisation des transitions.
• Ne pas vérifier le marquage de l’état initial pour conclure sur la satisfaction de la propriété.
• Dans l’exercice du digicode, ne pas incrémenter correctement le compteur d’erreurs ou mal gérer les transitions d’alarme.
• Dans le modèle du tunnel, mal représenter les états des trains (neutre, attente, tunnel) peut fausser la vérification des propriétés.