Université de La Manouba Année Universitaire 2022-2023
Ecole Nationale des Sciences de l’Informatique Date : le 16 Mai Juillet 2023
Module : Génie Logiciel II Enseignants :
Leila Ben Ayed - Hassen Gharbi – Fadoua Ouamani
Durée : 2h Doc : non autorisés Classe : II2
Examen
Tout au long de ce sujet, on travaille sur le modèle de kripke (M) représenté dans la Figure 1.
Ce modèle décrit un système d’impression. Il comporte cinq (05) états :
Q={q0, q1, q2, q3, q4} avec q0 comme état initial.
Les propositions atomiques associées aux états sont : OFF (système éteint), ON (système
allumé), READY(prêt pour imprimer), PRINT (impression terminée), ERROR (erreur
d’impression), CANCEL (impression annulée)
Figure 1: Modèle de Kripke
(M) à étudier
Exercice 1 : PLTL (4pts)
A) Formalisation : formaliser les énoncés des propriétés suivantes en PLTL.
1) Toujours le système est allumé (ON est vrai) (0.5pt)
2) Tout au long de l'exécution, il est possible d'éteindre le système (OFF
vrai).(0.5pt)
3) Tout au long de l'exécution, on peut se bloquer indéfiniment dans un état
d’erreur (ERROR).(0.5pt)
4) Si le système est infiniment souvent prêt (READY) alors on peut infiniment
souvent imprimer (PRINT)(0.5pt)
1/4
Université de La Manouba Année Universitaire 2022-2023
Ecole Nationale des Sciences de l’Informatique Date : le 16 Mai Juillet 2023
Module : Génie Logiciel II Enseignants :
Leila Ben Ayed - Hassen Gharbi – Fadoua Ouamani
Durée : 2h Doc : non autorisés Classe : II2
B) Vérification de formule PLTL
Soit la formule suivante : G (READY → ON ∪ PRINT)
5) Énoncer une phrase qui décrit le mieux cette formule (0.5pt)
6) Tracer l’arbre d'exécution correspondant au modèle de kripke de la Figure
1.(0.5pt)
7) Vérifier si cette formule est vraie ou non sur chaque chemin tout en justifiant
(1pt)
Exercice 2 : CTL (5pts)
A) Formalisation : formaliser les énoncés des propriétés suivantes en CTL.
1) Dans tous les états, le système est allumé (ON) (0.5pt)
2) On ne peut jamais avoir un système éteint (OFF) et allumé (ON) en même
temps. (0.5pt)
3) Pour toutes les exécutions, il est toujours possible d'éteindre le système (OFF)
(depuis n’importe quel état). (1pt)
4) Si le système se met en erreur (ERROR) alors il est possible de revenir à un
mode prêt (READY).(1pt)
B) Vérification de formule CTL
Soit la formule suivante : AG (READY → AX PRINT)
5) Énoncer une phrase qui décrit le mieux cette formule (1pt)
6) En s’appuyant sur l’arbre d'exécution, tracée dans le premier exercice, vérifier
si cette formule est vrai ou non en justifiant.(1pt)
Problème : Model-Checking (11pts)
Soit la propriété 𝛟 = AG ⅂( PRINT ∧ ⅂ E (ON ∪ OFF) )
On voudrait vérifier si le modèle de Kripke M satisfait 𝛟 , M ⊨ 𝛟? On procédera par étapes :
1. On pose P1 = E (ON ∪ OFF). Détailler les étapes permettant de vérifier si M ⊨ P1,
en appliquant l’algorithme adéquat.(2.5pts)
2. On pose P2 = ⅂ P1. Déduire si M ⊨ P2?(1pt)
3. On pose P3 = PRINT ∧ P2. Détailler les étapes permettant de vérifier si M ⊨ P3,
en appliquant l’algorithme adéquat.(1pt)
4. Réécrire la propriété 𝛟 en utilisant la formule P3.(1pts)
5. En partant de la question précédente, Montrer que 𝛟 = ⅂ E (TRUE ∪ P3) (1pts)
2/4
Université de La Manouba Année Universitaire 2022-2023
Ecole Nationale des Sciences de l’Informatique Date : le 16 Mai Juillet 2023
Module : Génie Logiciel II Enseignants :
Leila Ben Ayed - Hassen Gharbi – Fadoua Ouamani
Durée : 2h Doc : non autorisés Classe : II2
6. On pose P4 = E (TRUE ∪ P3). Détailler les étapes permettant de vérifier si M ⊨ P4,
en appliquant l’algorithme adéquat.(2.5pts)
7. En s’appuyant sur l’étape précédente, vérifier si M ⊨ 𝛟?(1pt)
8. Soit 𝛟1 =AG (PRINT → A (ON ∪ OFF)), vérifier en justifiant si M ⊨ 𝛟1?(1pts)
Annexe
1. Équivalences
Les cas de l’algorithme : Abréviations pour toutes formules logiques temporelle p et q
1. p V q = ¬ (¬ p ∧ ¬q) F : Fatalement, inévitablement
G : Toujours
2. A p = ¬ E¬p
E : il existe au moins un chemin
3. G p = ¬ F¬p A : pour tout chemin
X : Juste après (Next)
4. F p = (True U p)
U : Jusqu’à (Until)
2. Le model Checker CTL : Marquage des états
Cas de l’algorithme :
Cas 1: phi = p /* proposition atomique*/
Pour tout q dans Q faire
Si p dans l(q) alors marquer q avec phi
Sinon marquer q avec ¬ phi
FinPour
Cas 2: phi = not psi
marquage (psi);
Pour tout q dans Q faire
Si q est marqué avec psi alors marquer q avec ¬ phi
Sinon marquer q avec phi
FinPour
Cas 3: phi = psi1 ∧ psi2
marquage (psi1);
marquage (psi2);
Pour tout q dans Q faire
Si q est marqué avec psi1 et avec psi2 alors marquer q avec phi
Sinon marquer q avec ¬ phi
FinPour
Cas 4: phi = EX psi
marquage (psi);
Pour tout q dans Q faire
marquer q avec ¬ phi /*initialisation*/
FinPour
Pour tout (q,e,q’) dans T faire /* q prédécesseur de q’ */
Si q’ est marqué avec psi alors marquer q avec phi
Finpour
3/4
Université de La Manouba Année Universitaire 2022-2023
Ecole Nationale des Sciences de l’Informatique Date : le 16 Mai Juillet 2023
Module : Génie Logiciel II Enseignants :
Leila Ben Ayed - Hassen Gharbi – Fadoua Ouamani
Durée : 2h Doc : non autorisés Classe : II2
Cas 5: phi = E psi1 U psi2
marquage (psi1);
marquage (psi2);
Pour tout q dans Q faire
marquer q avec ⅂ phi;
q.dejavu:= false /*Initialisation*/
Finpour
L := {} /*L: Les états à traiter*/
Pour tout q dans Q faire
Si q est marqué avec psi2 alors L:= L U {q}
Finpour
Tant que L non vide faire
prendre un q dans L; L := L – {q}; marquer q avec phi
Pour tout (q’,e, q) dans T /* q’ est un prédecessur de q*/
Si q’.dejavu = false alors { q’.dejavu := true;
Si q’ est marqué avec psi1 alors L := L U {q’} }
Finpour
FinTq
Cas 6: phi = A psi1 U psi2
marquage (psi1);
marquage (psi2);
Pour tout q dans Q faire /*Initialisation*/
q.nb := degre(q); /*degre(q)=nbre de transitions dont q est source*/
marquer q avec ⅂ phi
Finpour
Pour tout q dans Q faire
Si q est marqué avec psi2 alors L:= L U {q};
Finpour
Tant que L non vide faire
prendre un q dans L /* marquer q*/
L := L – {q};
marquer q avec phi
Pour tout (q’, e, q) dans T faire /* q’ est un prédécesseur de q*/
q’.nb := q’.nb-1;
Si (q’.nb = 0) et (q’ est marqué avec psi1) et (q’ est marqué avec ⅂ phi)
alors L:= L U {q’};
Finpour
FinTq
4/4
