Correction TD 1 de Model Checking
Modélisation des systèmes réactifs
Exercice 1 (Exemple de l’ascenceur.). Le système de contrôle d’un ascenceur (pour 3 étages) est défini par :
– le contrôleur garde en mémoire l’étage courant et l’étage cible.
– en mode actif, quand l’étage cible est atteint, les portes s’ouvrent et le contrôleur passe en mode attente.
– en mode actif, quand l’étage cible est plus élevé que l’étage courant, le contrôleur fait s’élever l’as-
cenceur.
– en mode actif, quand l’étage cible est moins élevé que l’étage courant, le contrôleur fait descendre
l’ascenceur.
– en mode attente, il se peut que quelqu’un entre dans l’ascenceur et choisisse un nouvel étage cible.
L’ascenceur ferme alors les portes et redevient actif.
– initialement, l’ascenceur est à l’étage 0 et en mode attente.
Questions : 1. Proposez une machine à états modélisant le contrôle de l’ascenceur (définition formelle et
dessin). 2. Définissez et dessinez le système de transitions correspondant (en vous limitant aux configurations
accessibles depuis l’état initial). 3. Est-ce que les portes peuvent s’ouvrir quand l’ascenceur est actif ?
Correction.
1. Voici ma machine à états. Les variables sont courant :int[0..2], cible :int[0..2] et open :bool. L’action
random int retourne un entier entre 0 et 2 de manière non déterministe.
choice
true -> cible:=random_int up
open:=false courant < cible -> courant++
idle actif
ok
courant == cible -> open := true
down
courant > cible -> courant--
2. L’état initial est : état de contrôle idle, (open, cible, courant) := (true, 0, 0).
1
ok
idle, true, 0, 0
choice
choice choice
active, false, 0, 2
active, false, 0, 1
active,false,0,0
up
up
active, false, 1, 1 active, false, 1, 2
choice
ok choice up
idle, true, 1, 1 active, false, 2, 2
choice
ok
down
idle, true, 2, 2
down
choice
choice
active, false, 1, 0
active, false, 2, 1
down
choice
active, false, 2, 0
3. Non, trivial ici vu la modélisation.
Quelles sont les transitions du système concurrent dans les cas suivants :
1. sémantique synchrone ;
2. sémantique asynchrone (1) ;
3. sémantique asynchrone (2) ;
4. sémantique synchrone + synchronisation entre 1 et 3 ;
5. sémantique asynchrone (2) + synchronisation entre 1 et 3 ;
2
Quelles sont les transitions du système concurrent dans les cas suivants :
1. sémantique synchrone ;
2. sémantique asynchrone (1) ;
3. sémantique asynchrone (2) ;
4. sémantique synchrone + synchronisation entre 1 et 3 ;
5. sémantique asynchrone (2) + synchronisation entre 1 et 3 ;
3
Quel est le lien entre vecteur de synchronisations et rendez-vous ?
Correction.
1. les transitions de la machine produit sont : 1x3, 1x4, 1x5, 2x3, 2x4, 2x5.
2. les transitions de la machine produit sont : 1xε, 2xε, εx3, εx4, εx5.
3. les transitions sont celles de la question 1 plus celles de la question 2.
4. les transitions de la machine produit sont : 1x3, 2x4, 2x5.
5. les transitions de la machine produit sont : 1x3, 2x4, 2x5, 2xε, εx4, εx5.
6. Un RDV est un vecteur de synchronisation ne contenant que deux transitions.
Exercice 5 (Sûreté). On se donne un système de transitions S dont certaines transitions sont distinguées
et correspondent à des opérations d’aquisition de verrou (lock), de rendu de verrou (unlock), de lecture
(read) et d’écriture (write). On se donne la propriété ϕ suivante :
Si on ne regarde que les lock et unlock : unlock est toujours précédé directement de lock ET une suite
arbitraire de read,write est toujours précédée directement d’un lock .
Questions :
1. Est-ce que ϕ est une propriété de sûreté ? Sinon modifiez là en conséquence.
2. Écrivez un automate observeur pour vérifer ϕ (ou sa modification) et expliquez la nouvelle propriété à
vérifier.
3. On considère maintenant la spécification :
Si on ne regarde que les lock et unlock : unlock est toujours précédé directement de lock lock est
toujours suivi directement de unlock, ET une suite arbitraire de read,write est toujours précédée
directement d’un lock et fermée directement par un unlock.
Est-ce toujours une propriété de sûreté ?
Correction.
1. ϕ est bien une propriété de sûreté car (intuitivement) on peut reconnaitre une exécution incorrecte en considérant
juste une portion finie du passé de cette exécution. Ici, il suffit de regarder la trace d’exécution pour vérifier que les lock,
unlock, read, write sont bien mis correctement.
2. Voilà l’automate observeur ci-dessous. La propriété à vérifier (dans le système produit) est que l’état de contrôle
ERROR de l’automate oberveur n’est pas atteignable.
unlock
read
ERROR
write
unlock lock
read lock
write
3. Cette propriété n’est plus de la sûreté : pour savoir que tout lock est suivi d’une séquence éventuelle de read/write
puis d’un unlock, il faut “regarder” le futur de l’exécution. Ainsi, une exécution (infinie) fautive commence par exemple
par un lock et n’a jamais de unlock. Regarder le passé de cette exécution ne permet jamais de dire qu’elle est fautive.