Preuve de propriétés dynamiques en B

Un système d’information est un ensemble organisé de ressources permettant d’acquérir, de stocker et de traiter des informations sous forme de données au sein d’une ou plusieurs organisations [25]. Un tel système peut contenir des failles qui conduiraient à des pertes considérables comme des pertes matérielles très importantes. De telles failles peuvent être très pénalisantes surtout dans le cas des systèmes critiques qui ne tolèrent aucun dysfonctionnement, car des vies humaines sont mises en jeu. Ainsi pour avoir la garantie qu’un système ne se comportera pas de façon inattendue ou incorrecte, des vérifications doivent être réalisées dès ses premières phases de conception pour réduire le coût souvent élevé de la correction des bugs détectés tardivement.

Depuis quelques années, la nécessité d’utiliser des méthodes formelles s’est fait ressentir dans le développement des logiciels car ces dernières, fondées sur des notions mathématiques et rigoureuses, permettent de garantir la correction du logiciel ainsi obtenu. Cependant, et bien qu’elles permettent d’assurer l’absence de bugs dans les logiciels, l’utilisation de ces méthodes est souvent jugée coûteuse en termes de ressources matérielles et humaines. De ce fait, les méthodes formelles sont plus utilisées dans le cadre du développement des systèmes critiques. Le présent travail a pour but de contribuer à l’utilisation des méthodes formelles dans le développement de systèmes d’information sûrs.

Dans la littérature, les méthodes formelles de vérification les plus utilisées sont principalement le model checking et la preuve. Le model checking (appelé aussi exploration de modèles), une technique le plus souvent automatique, effectue une énumération exhaustive des différents états du système [14] et par conséquent devient inadapté pour les systèmes à nombre d’états élevé ou infini en raison de l’explosion combinatoire de l’espace des états. Par opposition au model checking, la preuve formelle a l’avantage d’être indépendante de la taille de l’espace des états du système à vérifier. Cependant, l’activité de preuve n’est généralement supportée que par des assistants à la preuve qui peuvent échouer sur des preuves trop complexes. Dans ce cas, l’intervention humaine devient nécessaire pour indiquer à l’assistant les bonnes règles d’inférence et de réécriture à appliquer.

Problématique

Jusqu’à présent, l’utilisation des méthodes formelles dans le cadre de la conception des systèmes d’information considère essentiellement les propriétés statiques qu’on désigne par le terme d’invariant. Un invariant est une propriété qui doit être toujours vérifiée sur tous les états possibles du système. De plus, de telles propriétés dépendent d’un seul état du système, i.e., les valeurs des variables du système sont toutes prises au même instant. La vérification de ces propriétés est réalisée sur chaque état du système sans considérer ni son passé ni son futur. D’un point de vue pratique, pour vérifier un invariant, il suffit de s’assurer que ce dernier est satisfait par l’état initial du système et est maintenu par chacune de ses opérations.

Cependant, garantir la qualité et le bon fonctionnement d’un système d’information ne peut pas se restreindre à la vérification de propriétés statiques; d’autres types de propriétés, dites dynamiques ou temporelles, doivent être considérées. Contrairement aux propriétés statiques, les propriétés dynamiques dépendent de plusieurs états du système pris à des instants différents et qui doivent donc être considérés lors de la vérification. De telles propriétés permettent par exemple de s’assurer que le système de gestion de prêts d’une bibliothèque offre à un lecteur inscrit la possibilité d’emprunter un livre et de le restituer. De même, un système de vente de billets ne doit pas envoyer le billet à un voyageur avant que ce dernier ait payé sa facture.

La logique temporelle

La logique temporelle ou modale trouve de nombreuses applications en informatique: traitement du langage naturel, représentation des connaissances [16], spécification de systèmes [19], etc. Cette logique étend la logique conventionnelle (propositionnelle) en introduisant de nouveaux opérateurs qui permettent de référencer plusieurs instants différents de l’exécution d’un système. La logique temporelle permet ainsi d’exprimer des propriétés dynamiques portant sur plusieurs états des traces d’exécution d’un système. Dans la littérature, nous distinguons les deux classes principales de logique temporelle suivantes :
– La logique linéaire comme LTL (Linear Temporal Logic) permettant d’exprimer des propriétés portant sur des chemins individuels issus de l’état initial du programme.
– La logique arborescente comme CTL (Computation Tree Logic) permettant d’exprimer des propriétés portant sur les arbres d’exécution issus de l’état initial du programme. Il existe aussi la logique CTL* qui permet de décrire à la fois des propriétés linéaires et arborescentes. La logique CTL* est souvent considérée comme une fusion des logiques LTL et CTL puisque les formules LTL et CTL sont des sous-ensembles des formules CTL*.

La logique LTL

LTL est définie sur un ensemble de variables propositionnelles {p, q, .. .}, de connecteurs logiques propositionnels habituels ¬, ∧, ∨, → et de connecteurs temporels (G, F, U et X). La grammaire associée à la logique LTL est comme suit :

– les formules atomiques :
ψ, φ := p | q | . . . | true | false

– les formules construites à partir de connecteurs propositionnels :
ψ := φ | ¬φ | φ ∧ φ | φ ∨ φ | φ ⇒ φ | φ ⇔ φ

– les formules construites à partir de connecteurs temporels :
– Gφ : (G comme Globally) spécifie que φ est toujours vrai
– Fφ : (F comme Futur) indique que φ sera vrai dans le futur
– φUψ : (U comme Until) spécifie que φ reste vrai jusqu’à ce que ψ devienne vrai. Cet opérateur impose que le système atteigne un état où ψ devient vrai.
– Xφ : (X comme Next) spécifie que φ sera vrai à l’étape suivante de l’exécution

La logique CTL

Contrairement à la logique LTL qui considère une vue linéaire du système, la logique CTL (Computation Tree Logic) permet de prendre en compte plusieurs futurs possibles à partir d’un état donné du système. La logique CTL a donc une vision arborescente de l’évolution du système. Elle étend la grammaire de LTL en incluant deux quantificateurs de chemins : l’un universel (A) et un second existentiel (E).
– A signifie : « pour tous les chemins possibles de calcul à partir de l’état courant »
– E signifie : « pour un certain chemin de calcul à partir de l’état courant » Les formules CTL sont donc toutes précédées des quantificateurs A ou E et sont définies par la grammaire suivante :

φ, ψ :=EGφ | EFφ | EφUψ | EXφ | AGφ | AFφ | Aφ U ψ | AXφ

avec φ, ψ désignant des formules LTL. La logique CTL introduit également quelques notions d’équité afin de ne considérer que les chemins où aucun événement du système ne prend indéfiniment le contrôle. Par exemple, dans un système d’allocation de ressources partagées par plusieurs utilisateurs, on ne voudrait pas s’intéresser aux chemins où un utilisateur garde la ressource indéfiniment. Pour ce faire, CTL introduit deux opérateurs Af et Ef pour préciser qu’on ne considère que les chemins jugés équitables.

La logique CTL∗

La logique CTL∗ est la logique temporelle la plus générale. Comme en LTL et CTL, une formule CTL∗ est donc construite à partir de propositions atomiques, de connecteurs propositionnels, de connecteurs temporels et de quantificateurs de chemins. Les opérateurs propositionnels et les quantificateurs de chemins restent les mêmes que dans CTL. Ajouté à ces différents connecteurs, CTL∗ introduit un cinquième connecteur temporel noté W et dont la sémantique est comme suit : étant donné deux prédicats p et q, pWq signifie que p doit rester vrai jusqu’à ce que q soit établi. Contrairement au connecteur U, le connecteur W n’impose pas que le prédicat q devienne vrai durant l’exécution du programme. En CTL∗ , on distingue les formules d’états de celles de chemins :

– Une formule d’état φ est définie comme suit :
φ := p | ¬φ | φ ∧ φ | φ ∨ φ | Aψ | Eψ

avec ψ désignant une formule de chemin.

– Une formule de chemin ψ est quant à elle définie par :
ψ := φ | ¬ψ | ψ ∧ ψ | ψ ∨ ψ | Xψ | Fψ | Gψ | ψUψ | ψWψ

Notons, qu’une nouvelle notation des connecteurs temporels F et G, très utilisée dans la littérature, a été introduite dans la logique CTL∗ . Les connecteurs F et G sont notés ♦ et respectivement. Ces nouvelles notations s’expriment comme suit :
– ♦p=⊤Up signifie que p sera vrai dans le futur.
– p=¬♦¬p signifie que p est toujours vrai. Par conséquent, l’opposé de p ne sera jamais vrai dans le futur.

Table des matières

1 Introduction générale
1.1 Contexte
1.2 Problématique
1.3 Contributions
2 État de l’art
2.1 La logique temporelle
2.1.1 La logique LTL
2.1.2 La logique CTL
2.1.3 La logique CTL∗
2.2 Vérification de propriétés de vivacité d’UNITY avec Event B
2.2.1 Preuve des propriétés basiques de vivacité
2.2.2 Preuve de propriétés générales de vivacité
2.2.3 Exemple illustratif
2.2.3.1 Vérification sous l’hypothèse du progrès minimum
2.2.3.2 Vérification sous l’hypothèse d’équité faible
2.3 Vérification de propriétés dynamiques en Event B
2.3.1 Preuve de propriétés élémentaires
2.3.1.1 Propriété LeadsTo
2.3.1.2 Propriété de convergence
2.3.1.3 Propriété de divergence
2.3.1.4 Propriété de non-blocage
2.3.2 Propriété d’existence
2.3.3 Propriété de progression
2.3.4 Application à un cas d’étude
2.4 Vérification de propriétés dynamiques en Event B étendue avec PLTL
2.4.1 Reformulation de propriétés
2.4.2 Vérification d’une propriété reformulée
2.4.3 Application à un cas d’étude
2.5 Vérification de propriétés dynamiques sur un système FDS
2.5.1 Représentation des hypothèses d’équité
2.5.2 Système FDS
2.5.3 Preuve de propriétés de sécurité sous hypothèse de forte équité
2.5.4 Un système de preuve déductive pour CTL∗
2.5.5 Application à un cas d’étude
2.6 Commentaires généraux
2.7 Conclusion
3 Preuve de propriété d’atteignabilité par génération formelle d’assertions
3.1 Notions et définitions
3.2 Algorithme de génération d’obligations de preuve : version simplifiée
3.2.1 Méthode de preuve
3.2.2 Application à un cas d’étude
3.3 Algorithme de génération d’obligations de preuve : version améliorée
3.3.1 Méthode de preuve
3.3.2 Application à un cas d’étude
3.4 Preuve de propriété d’atteignabilité par la plus faible précondition
3.4.1 Méthode de preuve
3.4.2 Application à un cas d’étude
3.5 Comparaison des différentes approches
3.6 Conclusion
Conclusion générale

Télécharger le rapport complet