Ex1: Digicode
(cid:1)
Rappel de l’automate:
B, C
A
1
A
2
C
B, C
B
A
3
4
1.
2.
3.
4.
Transformer cet automate en un Kripke K
Ecrire la formule temporelle de la propriété P suivante: « toute suite de
lettres tapées finissant par ABA ouvre la porte ».
Vérifier si K |= P ?
Modifier l’automate afin de:
(cid:2)
(cid:2)
Permettre de tolérer au maximum trois erreurs,
Ajouter des transitions déclenchant une alarme lorsque quatre erreurs
sont commises.
R.DRIRA
ENSI-GLII
Chapitre4: Model checking
79
Réponse
B, C
A
A
1
B
2 pA
3 pB
pA: On vient nécessairement de taper A
pB: On vient nécessairement de taper B
pC: On vient nécessairement de taper C
PO: Porte ouverte
C
B, C
A
4 pA
PO
Q = {1, 2, 3, 4}
q0 = 1
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)}
E = {A, B, C}
l = {1 ↦ {PF}, 2 ↦ {pA,PF}, 3 ↦ {pB, PF}, 4 ↦ {pA, PO}}
Propriété P: G(X PA (cid:217) XX PB (cid:217) XXX PB ⇒ XXX PO)
R.DRIRA
ENSI-GLII
Chapitre4: Model checking
80
40
Réponse: Quelques variables en plus
digicode avec transitions gardées
Advertisement
Si ctr< 3
B, C
ctr := ctr +1
Si ctr < 3
A
ctr := ctr +1
Si ctr < 3
B, C
ctr := ctr +1
A
1
B
2
A
3
4
Si ctr < 3
C
ctr := ctr +1
Si ctr = 3
B, C
ctr := ctr +1
err
Si ctr = 3
A, C
ctr := ctr +1
Si ctr = 3
B, C
ctr := ctr +1
R.DRIRA
ENSI-GLII
Chapitre4: Model checking
81
Remarques: Quelques variables en plus
(cid:2) Lorsqu’on modélise des systèmes réels, il est souvent
commode de permettre aux automates de manipuler des
variables d’états.
(cid:2) Les liens entre un automate et les variables peuvent être
de deux types:
(cid:2) Affectations : Une transition peut modifier la valeur
d’une ou de plusieurs variables.
(cid:2) Exemple: toutes les transitions sauf (1, A, 2), (2, B, 3) et
(3, A, 4) incrémentent le compteur.
(cid:2) Gardes : Une transition peut être gardée par une
condition sur les variables. Ainsi, le franchissement de la
transition n’est possible que si la condition est vérifiée.
(cid:2) Exemple: les transitions correspondant à une erreur (1, B,
1), (1, C, 1), (2, C, 1), etc. sont gardées par la condition
ctr < 3.
R.DRIRA
ENSI-GLII
Chapitre4: Model checking
82
41
Réponse: Quelques variables en plus
R.DRIRA
ENSI-GLII
Chapitre4: Model checking
83
Ex2: Un robot de transport de pièces
(cid:1) L'objectif de la modélisation est le développement
du logiciel de commande du bras de transport de
pièces
Advertisement
(cid:1) Il est composé de 3 dispositifs :
(cid:2) un dispositif d'arrivée des pièces appelé Da
(cid:2) un dispositif de transport de pièces appelé Dt
qui est un bras muni d'une pince,
(cid:2) Un dispositif d'évacuation de pièces appelé De
sur lequel Dt transporte les pièces arrivant sur
Da.
R.DRIRA
ENSI-GLII
Chapitre4: Model checking
84
42
Ex2: Un robot de transport de pièces
1. Proposer une structure Kripke du robot de
transport:
(cid:2) On se concentre sur l'essentiel : le transport des
pièces.
(cid:2) pour simplifier on ignore Da,
(cid:2) on s'intéresse uniquement à l'introduction de la
pièce dans Dt et à sa sortie sur De,
(cid:2) nous ne regardons pas le fonctionnement
(ouverture, fermeture, etc.) de la pince,
2. Propriété à vérifier Pr: si le dispositif de
transport Dt décharge alors De est libre.
L’écrire en logique temporelle
3. Vérifier si votre Kripke satisfait Pr
R.DRIRA
ENSI-GLII
Chapitre4: Model checking
85
Réponse
e0
DtL DeL
chargt
e1
DeL
Déchargt
e2
DtL
e3
chargt
Evac
DtL: Dispositif de transport libre
DeL: Dispositif d’évacuation libre
Evac
Propriété Pr à vérifier:
AG ((┐DtL ∧∧∧∧ EX(DtL)) ⇒⇒⇒⇒ DeL)
R.DRIRA
ENSI-GLII
Chapitre4: Model checking
86
43
Vérifier si le Kripke satisfait Pr
Pr AG ((┐DtL ∧∧∧∧ EX(DtL)) ⇒⇒⇒⇒ DeL), Pr est notre Φ si on veut utiliser le même symbole que l’algorithme.
Il faudra décomposer Pr en sous formules. Chaque sous formule devra retrouver un cas correspondant parmi
les 6 cas supportés par l’algorithme de marquage de CTL.
Rappel: les 6 cas sont exhaustifs et en se basant sur les abréviations (diapo71) on pourra réécrire et vérifier
toute formule CTL en se basant sur ces 6 cas.
AG ((┐DtL ∧ EX(DtL)) ⇒ DeL)
P1= ┐DtL (cas2)
P2=EX(DtL) (cas4)
P3= P1 ∧ P2 (cas3)
Pr devient : AG (P3 ⇒ DeL)
Advertisement
P4= P3 ⇒ DeL= ┐(P3 ∧ ┐DeL)
P41= ┐DeL (cas2)
P42= P3 ∧ P41 (cas3)
P4= ┐P42 (cas2)
Pr devient : AG (P4)
Pr=AG(P4)= ┐E (true U ┐P4)
┐P4=P42
P51=true (true=p ∨ ┐p) (cas1)
P52= E(P51 U P42) (cas5)
Pr= ┐P52 (cas2)
Maintenant, on fait le marquage (diapo suivant) et pour connaître si notre Kripke vérifie Pr, on consulte l’état initial: s’il
est marqué par Pr alors notre modèle satisfait Pr. S’il est marqué par ┐ Pr, c’est que notre Kripke ne satisfait pas
Pr.
R.DRIRA
ENSI-GLII
Chapitre4: Model checking
87
Marquage
┐P1, ┐P2, ┐P3
┐P41, ┐P42, P4
P51, ┐P52, DV=F
e0
DtL DeL
Pr
P1, P2, P3
┐P41, ┐P42, P4
P51, ┐P52, DV=F
e1
DeL
Pr
┐P1, P2, ┐P3
P41, ┐P42, P4
P51, ┐P52, DV=F
P1, ┐P2, ┐P3
P41, ┐P42, P4
P51, ┐P52, DV=F
e2
DtL
e3
Pr
Pr
P1= ┐DtL (cas2)
P2=EX(DtL) (cas4)
P3= P1 ∧ P2 (cas3)
P41= ┐DeL (cas2)
P42= P3 ∧ P41 (cas3)
P4= ┐P42 (cas2)
P51=true (true=p ∨ ┐p) (cas1)
P52= E(P51 U P42) (cas5)
Pr= ┐P52 (cas2)
R.DRIRA
ENSI-GLII
Chapitre4: Model checking
88
44
Ex3: tunnel
(cid:1) On considère un tunnel de montagne spécialement étroit qui ne
permet le passage que d’un seul train à la fois. Deux trains circulent
sur cette ligne. Afin d’assurer la sécurité des voyageurs, chaque train
peut échanger des signaux avec l’ordinateur qui assure le trafic dans le
tunnel (le médiateur). Ces signaux sont de trois types :
(cid:2) attente : le train veut traverser le tunnel et attend une autorisation,
(cid:2) entrée : le train obtient l’autorisation d’entrer dans le tunnel,
Advertisement
(cid:2) sortie : le train sort du tunnel.
Chaque signal est indexé par le numéro du train concerné.
1. Construire un automate modélisant le système.
2. Exprimer en CTL les propriétés suivantes :
(cid:2) Les deux trains ne traversent jamais en même temps le tunnel
(sûreté de l’accès).
(cid:2) Un train en attente fini toujours par traverser le tunnel (vivacité).
(cid:2) Un train qui est sorti peut toujours se mettre en attente (non-
blockage).
3. Utiliser l’algorithme de marquage de CTL pour vérifier chaque propriété
R.DRIRA
ENSI-GLII
Chapitre4: Model checking
89
Réponse
sortie1
1
sortie2
attente1
attente2
2
3
entrée1
attente2
4
5
attente2
entrée1
7
attente1
6
entrée2
9
entrée2
attente1
8
sortie1
sortie2
ni: train i neutre
ai: train i en attente
ti: train i dans le tunnel
R.DRIRA
ENSI-GLII
Chapitre4: Model checking
90
45
Réponse
(cid:1) Les deux trains ne traversent jamais en
même temps le tunnel (sûreté de
l’accès).
AG ┐ (t1 ∧∧∧∧ t2)
(cid:1) Un train en attente fini toujours par
traverser le tunnel (vivacité).
AG(a1(cid:1) AF t1) ∧∧∧∧ AG(a2(cid:1) AF t2)
(cid:1) Un train qui est sorti peut toujours se
mettre en attente (non-blockage).
AG(n1 (cid:1) EX a1) ∧∧∧∧ AG(n2 (cid:1) EX a2)
R.DRIRA
ENSI-GLII
Chapitre4: Model checking
91
46