Un système de preuve déductive pour CTL

Reformulation de propriétés

En B, le mécanisme de raﬃnement permet de passer d’un modèle abstrait vers un modèle plus concret. Dans cette approche, les auteurs proposent un raﬃnement conjoint de la spécification abstraite et des propriétés. Le raﬃnement des propriétés, appelé ici reformulation, est représenté par un modèle ♯♯′ avec P 1 : (p1 ⇒ ♯q1) représentant la propriété abstraite, P 2 : (p2 ⇒ ♯′q2) la propriété reformulée et ♯, ♯′ ∈ {⊖, −⋄, S}. Par conséquent, pour prouver que le raﬃnement est correct, on doit s’assurer que : si une propriété P1 est vérifiée sur la spécification abstraite d’un système T S1 alors la propriété P2 qui raﬃne P1 est aussi vérifiée sur le système T S2 qui raﬃne T S1.
Définition (Système de transitions) Un système de transitions est un quintuplet T S = (Q, Q0, L, T, l) avec
– Q représentant l’ensemble des états du système.
– Q0 représentant l’ensemble des états initiaux : Q0 ⊆ Q.
– L = {a0, a1, . . . , an} est l’ensemble des étiquettes appelées actions.
– T ∈ P (Q × L × Q) dénotant la relation de transition.

Vérification d’une propriété reformulée

De manière générale, pour vérifier une propriété de sécurité sur un modèle, il suﬃt de la prouver sur le modèle abstrait et de garantir que cette propriété est préservée par le mécanisme de raﬃnement. En outre, étant donné que le raﬃnement ajoute au système de nouveaux détails (événements, variables, etc.), les variables du niveau abstrait et celles du niveau raﬃné doivent être reliées par un invariant de collage. L’approche présentée dans cette section consiste à définir de nouvelles propriétés à partir des propriétés abstraites et à vérifier le respect de ces nouvelles propriétés sur la spécification raﬃnée à l’aide des théorèmes qu’ils ont eux-mêmes définis. La reformulation des propriétés abstraites a pour but de générer de nouvelles propriétés qui sont plus faciles à prouver sur la spécification concrète.
Pour vérifier les propriétés reformulées, des patterns de reformulation ont été proposés. Pour chaque pattern, des théorèmes sont définis afin d’assurer la correction de la reformula-tion appliquée. Cette section présente quelques uns de ces patterns ainsi que les théorèmes qui leur sont associés. Pour tous ces théorèmes, on considère T S1 et T S2 deux systèmes de transitions tels que T S2 raﬃne T S1 par l’invariant de collage I1,2 (noté T S1 ⊑ T S2), et φ1 et φ2 deux formules PLTL qui doivent être vérifiées respectivement sur les systèmes T S1 et T S2.
Cette propriété spécifie que si le système se trouve dans l’état S22 (raﬃnement de l’état S2), alors il s’est trouvé dans le passé dans l’état S12 (raﬃnement de l’état S1). Pour prouver cette propriété, nous devons utiliser le pattern ⊖⋄− présenté précédemment. Par conséquent, nous devons établir les preuves suivantes :
– (ss2 = S22 ∧ S22 = S2 ∧ ss2 = ss1) ⇒ ss1 = S2
– (ss1 = S1 ∧ ss2 = ss1 ∧ S12 = S1) ⇒ ss2 = S12
Ces deux preuves sont déchargées automatiquement à partir de la partie gauche de chaque implication. On en déduit ainsi que la propriété reformulée P2 est vérifiée sur le raﬃnement du système.

Vérification de propriétés dynamiques sur un sys-tème FDS

Dans cette section, nous présentons deux approches, très proches, de vérification de propriétés dynamiques sur un système FDS (Fair Discrete System) doté d’un ensemble d’hypothèses de faible et forte équité. La première approche [24] propose une règle pour vérifier des propriétés dynamiques de la forme p ⇒ ♦q sous l’hypothèse de forte équité. Cette propriété signifie que si un prédicat p est vrai durant l’exécution d’un système alors on atteindra un état où le prédicat q sera vrai. La seconde approche [23] propose quand à elle un ensemble de règles de vérification de propriétés CTL∗ de la forme p ⇒ Af ♦q. Ces propriétés expriment que si un prédicat p est vrai, alors pour toute exécution possible et juste du système, à partir d’un état qui satisfait p, on aura le prédicat q qui sera vrai dans le futur. Le quantificateur Af a été introduit dans la section 2.1.2. Tout d’abord, nous allons montrer la façon dont sont représentées les hypothèses d’équité, ensuite nous définissons ce que c’est un système FDS, puis enfin nous présentons les règles de vérification proposées par les deux approches.

Représentation des hypothèses d’équité

Dans [24] et [23], deux types d’hypothèses sont considérées : les hypothèses de faible et de forte équité. Ces deux hypothèses sont représentées comme suit :
– Une hypothèse de faible équité est représentée par une assertion J. Une exécution respecte une hypothèse de faible équité J si elle contient un nombre infini d’états qui satisfont l’assertion J.
– Une hypothèse de forte équité (appelée aussi de compassion) C est représentée par un couple d’assertions noté p, q . Une exécution respecte l’hypothèse de forte équité C si elle contient soit un nombre fini d’états satisfaisant p soit un nombre infini d’états satisfaisant q.

Système FDS

Un système FDS est un quintuplet D = V, Θ, ρ, J, C tel que :
– V = {u1, …, un} représente l’ensemble des variables du système D.
– Θ est la condition initiale du système. Par conséquent, l’état initial s0 de toute exécution (σ = {s0, s1, …}) du système D doit satisfaire la condition : s0 |= Θ.
– ρ(V, V ′) est une assertion reliant V et V ′, avec V et V ′ étant respectivement les valeurs des variables du système aux états s et s′.
– J ={J1, …, Jk} est l’ensemble des assertions de faible équité.
– C ={ p1, q1 , …, pn, qn} est l’ensemble des assertions de forte équité.
Un système FDS qui ne comprend que des hypothèses de forte équité est appelé CDS (pour Compassion Discrete System). De même, un système FDS qui ne considère que des hypothèses de faible équité est appelé JDS (pour Justice Discrete System).

Preuve de propriétés de sécurité sous hypothèse de forte équité

Dans [24], des règles de vérification de propriétés de sécurité, qui ne reposent que sur des hypothèses de forte équité, ont été proposées. Pour ce faire, les auteurs ont ré-exprimé les hypothèses de faible équité en termes d’hypothèses de forte équité.
Soit En(T) et Taken(T) deux assertions définies comme suit :
– En(T) est vraie pour tous les états où la transition T est active. Cette assertion indique ainsi si la transition T est franchissable.
– Taken(T) est vraie pour tous les états où la transition T est réellement franchie.
L’assertion JT suivante :
JT = (¬En(T ) ∨ T aken(T ))
indique que si une transition peut être franchie alors elle l’est. Une exécution respecte l’hypothèse de faible équité correspondant à JT s’il existe un nombre infini d’états où JT est satisfaite comme le montre la figure ci dessous : Les auteurs ont montré que l’hypothèse de faible équité JT est équivalente à celle de forte équité true, JT car l’assertion true reste toujours vérifiée. Ainsi toute hypothèse de faible équité peut être exprimée sous la forme d’une hypothèse de forte équité. En se basant sur des hypothèses de forte équité, les auteurs ont proposé un ensemble de règles pour la vérification de propriétés CTL∗ sur des systèmes réactifs. Parmi ces règles, nous présentons ci-après la règle RESPONSE.