Preuve De Propriété D’atteignabilité Par génération formelle d’assertions

Preuve De Propriété D’atteignabilité Par génération formelle d’assertions

 Algorithme de génération d’obligations de preuve : version simplifiée

Méthode de preuve L’approche que nous proposons pour prouver une propriété d’atteignabilité (AG(ψ ⇒ EF φ)) consiste à démontrer qu’il existe au moins un chemin, (cond ❀ (act1;…;actn)), qui mène de ψ à φ. Pour ce faire, nous devons établir que : 1. l’exécution de chaque chemin mène à φ : ψ ∧cond ⇒[(act1;…;actn)]φ (3.1) 2. pour un ensemble de chemins {ch1,…,chm}, au moins un des chemins chi menant à φ peut être exécuté : ψ ⇒( condi) (3.2) avec condi représentant la garde du chemin chi. L’utilisation de l’AtelierB pour la preuve de ces formules est évidemment possible.

Néanmoins, les preuves générées sont très nom breuses et assez complexes à décharger (voir section 3.4). C’est pour cette raison que nous avons développé une autre approche de preuve qui permet d’avoir des obligations beaucoup plus simples à établir. L’idée clé de notre approche peut être résumée par les trois points suivants : 1. Dans l’état s où ψ et cond sont vrais, l’action act1 est exécutable,

c.à.d., sa précon dition est satisfaite, 54 2. à tout point du chemin i (1 ≤ i ≤ (n−1)), après l’exécution de chaque action acti, les valeurs des variables vérifient la précondition de l’action suivante acti+1, 3. Après exécution de la dernière action actn, les valeurs des variables satisfont φ. Pour faciliter la présentation de l’algorithme de génération d’obligations de preuve, nous avons défini les fonctions γ, Ajout et Cons_PO comme suit :– la fonction γj fait le renommage, dans une action act, de chaque variable x par la variable xj−1 : γj(act) = [ → x := → xj−1]act avec → xj−1 désignant les valeurs (x1j−1,…,xnj−1) des variables de la spécification à l’étape (j − 1) de l’exécution du chemin.

Application à un cas d’étude

Cette section présente un cas d’étude simplifié de gestion d’un club vidéo qui permet d’illustrer l’approche proposée. Nous considérons donc des clients qui peuvent emprunter des cassettes ou les réserver si ces dernières ne sont pas disponibles. On fait l’hypothèse qu’un client ne puisse pas emprunter plus de deux cassettes et que les réservations sur une cassette donnée sont stockées dans une file. Nous obtenons la spécification suivante avec 56 Algorithm 1 Génération des obligations de preuve : version

Entrées: La propriété d’atteignabilité F = (AG (ψ ⇒ EF φ)) et un ensemble de chemins chs = {ch1,…,chm} 1: Soit POs ← ∅ l’ensemble des obligations de preuve à établir 2: pour chaque (ch ∈ chs∧ch = (cond ❀ (act1;…;actn))) faire 3: Soit VSpec ← {x1,…,xk} l’ensemble des variables de la spécification /*Initialisation des variables Hyp and For*/ 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: 20: 21: 22: 23: 24: 25: 26: Soit Hyp ← True les hypothèses locales Soit For ← ∅ l’ensemble des formules à prouver /*Traitement de l’action act1*/ For ←For ∪ {Pre(act1)} si (act1 = LOOP(C,|oo∈E op(oo,…),V )) alors For ←For ∪ {Pre(op) ⇒ (V ∈ N ∧[n:=V][S](V < n))} /*Hyp doit mémoriser la variable locale x utilisée dans |x∈E op(…)*/ sinon si (act1 = |x∈E _) alors Hyp ←∀x.(x ∈ E) f insi Hyp ← Ajout(Hyp,∀ → xi 1 .Postxi 0,xi 1(Sact1 )) /*Traitement des actions {a2,…,an}*/

pour chaque (action actj telle que (j ∈ 2..n)) faire actj ← γj(actj) For ←For ∪ {Cons_PO(Hyp,Pre(actj))} si (actj = LOOP(C,|oo∈E op(oo,…),V )) alors For ←For ∪ {Cons_PO(Hyp,Pre(op) ⇒ (V ∈ N∧ [n := V][S](V < n)))} sinon si (actj = |x∈E _) alors Hyp ←Ajout(Hyp,∀x.(x ∈ E)) f insi Hyp ←Ajout(Hyp,∀→ xi j−1 .Postxi j−1,xi j(Sactj )) f in pour For ←For ∪ {Cons_PO(Hyp,γn+1(φ)} Soit VF l’ensemble des variables de F Soit VF −VSpec = {y1,…,yl} l’ensemble des variables de F qui n’appartiennent pas à VSpec.

Ces variables sont libres et sont implicitement quantifiées universellement. L’obligation de preuve du chemin ch est PO(ch) ← ∀(y1,…,yl).(ψ ∧ cond ⇒ ( for∈For for)) 27: fin pour/*une obligation de preuve additionnelle est générée pour assurer que l’en sembles des chemins couvre, dans l’état s (où ψ est vrai), toutes les valeurs possibles des variables VSpec.*/ 28: POs ← i=1,m PO(chi)∪{∀(y1,…,yl).(ψ ⇒ i=1..m condi)