Soutenance mémoire
Si nous observons notre environnement, nous pouvons constater qu’une multitude de systèmes informatiques nous entourent. Ces systèmes sont devenus au cours de ces dernières années de plus en plus complexes, requérant une pluridisciplinarité très large pour les concevoir. Ils représentent également des enjeux stratégiques (économiques, sociétaux) importants, puisqu’ils interviennent dans des composantes critiques de systèmes aussi divers que l’aérospatial, l’aéronautique, les systèmes nucléaires, la télécommunication, le transport terrestre, la santé, le commerce électronique… Intervenant dans des domaines stratégiques, ces systèmes informatiques doivent être vérifiés, la moindre défaillance pouvant coûter très cher et causer des pertes irrémédiables : pertes d’informations, pertes financières ou même pertes humaines. Nous distinguons deux types de dysfonctionnement des systèmes. Le premier type concerne les problèmes matériels, qui se produisent lorsqu’un système connait une panne physique. Le deuxième type concerne les problèmes logiciels, appelés erreurs par abus de langage, qui surviennent lorsqu’un composant ne réalise pas précisémment les fonctionnalités pour lesquels il a été conçu. Parmi les erreurs qui ont marqué l’histoire, nous pouvons citer par exemple celle de la fusée Ariane 5 [34] (700 millions de dollars de perdus) ou celle du missile Patriot [43] (28 morts).
La production de systèmes informatiques sûrs est ainsi une activité complexe qu’il est difficile de mettre en oeuvre. La garantie de fonctionnement de ces systèmes est un enjeu crucial lors de leur développement et qui doit être pris en considération dès les premières étapes du développement. Face à ce besoin croissant et nécessaire de produire des systèmes informatiques sûrs, de nombreuses solutions de développement ont été proposées. La plupart des méthodes de développement classiques ne permettent pas de décrire d’une manière concise et correcte le comportement des systèmes. La limitation principale concerne l’activité de vérification qui n’est pas bien développée dans ces méthodes. Généralement, cette activité s’applique avant la phase d’implantation d’un système. Partant d’une spécification détaillée d’un système exprimée dans un modèle possédant une sémantique formelle, cette activité consiste à vérifier les propriétés comportementales de la spécification afin de détecter et corriger le plus tôt possible les éventuelles erreurs de conception. Notons que plus les erreurs de conception sont détectées tardivement, plus les coûts de corrections sont élevés. Afin de s’assurer du bon fonctionnement d’un système, une solution est donc d’adopter une démarche formelle de spécification et de vérification.
Contexte scientifique : l’utilisation des méthodes formelles
Les méthodes formelles regroupent tout un ensemble de notations et de concepts mathématiques et logiques permettant une description mathématique du système et une vérification basée sur les éléments de base de ces notations et concepts. Cette démarche consiste à vérifier si un modèle mathématique regroupant les comportements possibles du système satisfait ou non les propriétés à vérifier (souvent exprimées sous forme de fomules de logiques mathématiques). Les comportements du système sont spécifiés à l’aide d’un langage formel ayant une sémantique précise souvent basée sur des systèmes de transitions. Cette description doit éliminer toute ambiguité existante au niveau de l’expression de ces comportements en langage naturel. La vérification formelle doit montrer que tous les comportements du système satisfont les propriétés désirées. L’utilisation des méthodes formelles dans une démarche de développement peut se diviser en deux grandes phases : la spécification et la vérification.
La phase de spécification formelle
La spécification formelle est la première étape d’un processus formel de développement. Elle consiste à donner une description formelle d’un système et de ses propriétés en utilisant un langage ayant une syntaxe et une sémantique définies mathématiquement. Cette description formelle permet de lever toutes les ambiguités rencontrées dans la description donnée en langage naturel et de fournir ainsi une description rigoureuse et claire du système et des propriétés à vérifier. Une pléthore de méthodes de spécification formelle existent. Ces méthodes sont adaptées à plusieurs types de systèmes informatiques (systèmes distribués, systèmes synchrones, systèmes concurents, etc.). Deux grandes familles de formalismes de modélisation se distinguent : les formalismes à base de preuve tels que la méthode B [16], la méthode B événementiel [17], VDM [66], Action Systems [25] ou le langage Z [89] et les formalismes à base de systèmes de transitions tels que les Statecharts [55, 56], TLA [71], etc. Chacune de ces familles offre des avantages et des inconvénients spécifiques. Dans ce document, nous considérons un formalisme à base de preuve, le B événementiel.
Pour la modélisation des systèmes réels (matériels, logiciels ou encore naturels), il est nécessaire de prendre en compte des aspects quantitatifs tels que le temps, les ressources énergétiques, les incertitudes comportementales, la qualité des matériels, etc. Il devient ainsi compliqué de modéliser ces systèmes de manière exacte et discrète et les méthodes de spécification présentées précédemment ne permettent pas la prise en compte de ces aspects. Une solution est d’utiliser la théorie des probabilités pour modéliser les aspects “incertains” de ces systèmes : les incertitudes sont modélisées par des distributions de probabilité, et on parle ainsi de modèles stochastiques. Au lieu de vérifier des propriétés exactes de manière binaire, on s’intéresse dans ce cas à la vérification formelle des propriétés quantitatives. Cela permet de prendre en considération d’autres propriétés telles que la fiabilité [96], la réactivité [38, 94], le temps de réponse, la disponibilité des systèmes, l’évolution continue, la consommation énergétique, etc. Afin de modéliser ces aspects probabilistes, des formalismes probabilistes de modélisation ont été développés dans la littérature. La plupart de ces formalismes étendent d’autres formalismes de modélisation standards. En effet, de nombreux travaux [51, 86, 57, 48, 29, 64, 22, 63] ont traité l’introduction du raisonnement probabiliste dans des formalismes de modélisation à base de preuve comme la méthode B, Z, Action Systems, etc. Dans [86], les auteurs ont étudié l’expression des probabilités dans le formalisme Action Systems et dans [52], les auteurs ont étudié l’analyse de performance des systèmes dans ce formalisme. Dans [50], Haghighi et ses coauteurs ont proposé une extension probabiliste au formalisme Z. Ils ont aussi étudié dans [51] la spécification des chaines de Markov dans Z. La méthode B a aussi été l’objet de plusieurs travaux d’extension pour supporter le raisonnement probabiliste [57, 59]. De nombreux travaux de recherche [78, 54, 58, 98, 53, 91, 92, 93] ont également étudié l’intégration des probabilités dans la méthode B événementiel, nous détaillerons ces travaux plus loin dans ce manuscrit. Nous notons également que les formalismes à base de systèmes de transitions ont aussi été étendus pour prendre en compte des aspects probabilistes [90, 84, 84, 90].
La phase de vérification
Nous rappelons que l’objectif principal de l’utilisation des méthodes formelles est la vérification du comportement des systèmes. Après la spécification formelle d’un système, c’est le tour de la vérification qui vient : il faut s’assurer que la spécification est correcte et que les propriétés que le système doit satisfaire, sont toutes bien vérifiées. Étant donné un modèle M et une propriété φ, le but de la vérification est de garantir formellement que M respecte cette propriété (M |= φ) ou de fournir un contre-exemple dans le cas contraire. L’objectif de cette phase de vérification est de détecter les erreurs commises durant la phase de développement et les diagnostiquer pour pouvoir les corriger au plus tôt et de préférence avant la mise en production du système. Plusieurs méthodes sont utilisées pour la vérification des propriétés des systèmes, nous présentons dans ce qui suit les deux méthodes les plus utilisées, le model checking et le theorem proving.
• Le model checking [65, 40, 31] ou vérification de modèles est une méthode de vérification qui consiste en l’exploration de l’ensemble des exécutions et des états du modèle. Les propriétés sont exprimées la plupart du temps par des formules des logiques temporelles (LTL,CTL,CTL*,CSL…) [83, 30, 39, 87]. Le model checking est l’une des méthodes de vérification les plus outillées. De nombreux vérificateurs de modèles ont été développés dans la littérature pour la mise en pratique de cette méthode [61, 72, 47, 99]. Cependant, les techniques de vérification basées sur le model checking représentent un problème fondamental que l’on rencontre pour une grande gamme de système réels : le phénomène de l’explosion combinatoire de l’espace d’états [41], qui rend impossible en pratique la phase de vérification car le modèle à vérifier est trop complexe. Les techniques de vérification par model checking ont aussi été développées pour les systèmes probabilistes [33, 28]. De nombreuses techniques de manipulation et de combinaison de modèles telles que l’abstraction [68, 44], qui permet de réduire la taille des modèles ou le raffinement [67] qui permet de leur ajouter des détails ont été développées dans ce contexte.
• Le Theorem proving : Les méthodes de preuve ou Theorem proving ont été introduites par Hoare [60]. Elles permettent de vérifier si un programme satisfait une spécification. Le problème de vérification (le programme satisfait-il la spécification) est exprimé comme un théorème que l’on cherche à prouver à partir d’un ensemble d’axiomes du modèle. Ces méthodes ont été outillées et plusieurs assistants de preuve existent. Nous citons à titre d’exemples les assistants PVS [81], Coq [62], HOL [49], et Isabelle [82]. Ces assistants permettent l’automatisation d’une partie de la preuve. Contrairement au model checking, les techniques de preuve ne souffrent pas de l’explosion combinatoire de l’espace d’états. Néanmoins, une intervention humaine est souvent nécessaire pour guider les assistants de preuve, ce qui rend difficile l’utilisation de ces techniques dans le contexte industriel. Les techniques de vérification par preuve ont été étendues pour supporter la vérification des comportements probabilistes. Nous notons à titre d’exemples des travaux traitant l’extension probabiliste des formalismes Z [51], Action Systems [86], B [57], HOL [64], Coq [22]. Plusieurs autres travaux ont traité la vérification d’algorithmes probabilistes par des techniques de preuve dédiées [48, 29, 63].
B événementiel et systèmes de transitions
De nombreux formalismes de spécification de haut niveau existent et permettent la description des comportements des systèmes. Nous présentons dans ce chapitre la méthode B événementiel et le formalisme systèmes de transitions. Le B événementiel[15, 21] est une méthode de spécification et de vérification proposée par Jean-Raymond Abrial comme une évolution de la méthode B classique[16]. Le B événementiel a gardé la puissance et la simplicité de la méthode B, mais il a apporté des améliorations sur plusieurs autres aspects. Les deux méthodes ont le même fondement mathématique[16], elles sont basées sur la logique du premier ordre et la théorie des ensembles. Le B événementiel permet la description de systèmes distribués, parallèles, multi-modals, réactifs et interactifs. Cela peut être, par exemple, un système de train[17], un protocole de communication[20] ou un système de gestion (réservation) de vol[17]. Contrairement à la méthode B, le B événementiel considère un système fermé pour représenter l’ensemble des composants dans un seul modèle. De même, le B événementiel définit le comportement dynamique du système sous forme d’événements et non par des opérations comme en B classique. Un modèle B événementiel représente une abstraction mathématique d’un système. Il prend en compte tous les aspects du système, statique et dynamique. Les éléments statiques d’un système se placent dans un type de composant B événementiel appelé ‘contexte’ alors que les aspects dynamiques d’un système se placent dans un type de composant B événementiel appelé ‘machine’. Un contexte décrit les aspects statiques d’un système. Il peut contenir des définitions d’ensembles, des constantes, des axiomes caractérisant les constantes et des propriétés que l’on démontre.
Modèle B événementiel
Un modèle B événementiel décrit le comportement global d’un système, il est formé par une suite de paires où chaque paire est constitué d’une machine et d’un contexte tel que le contexte est “vu” par la machine.
Contexte
Dans un projet de développement en B événementiel, les contextes permettent de spécifier les éléments ainsi que les propriétés statiques d’un système. Un contexte peut contenir des ensembles et des constantes. Les constantes sont des éléments dont la valeur ne change pas durant le déroulement du système étudié et qui sont définies par des axiomes. Les ensembles contiennent des éléments statiques qui ne changent pas durant le déroulement du système. Les contextes peuvent être liés entre eux. Comme une machine peut raffiner une autre machine, un contexte peut étendre un ou plusieurs contextes, et ainsi avoir accès aux éléments des précédents.
|
Table des matières
1 Introduction
2 B événementiel et systèmes de transitions
2.1 Introduction
2.2 Modèle B événementiel
2.2.1 Contexte
2.2.2 Machine
2.2.3 Événement
2.2.4 Substitution généralisée
2.3 Cohérence d’un modèle B évenementiel
2.3.1 Correction des expressions
2.3.2 Obligations de preuve de machine
2.4 Raffinement
2.4.1 Raffinement en B événementiel
2.4.2 Exactitude du raffinement
2.4.3 Convergence des nouveaux événements
2.5 Étude de cas : Protocole Pair à Pair
2.5.1 Stratégie du développement du protocole en B événementiel
2.5.2 La première machine
2.5.3 Deuxième machine
2.5.4 Troisième machine
2.6 Systèmes de transitions
2.6.1 Systèmes de transitions
2.6.2 Systèmes de transitions et probabilités
2.6.3 Sémantique opérationnelle d’une machine B événementiel
2.7 B Événementiel et probabilités
3 B événementiel probabiliste
3.1 Introduction
3.2 Introduction des probabilités en B événementiel
3.2.1 Non-déterminisme en B événementiel : Exemple
3.2.2 Introduction des probabilités dans la machine Mch
3.3 B événementiel probabiliste
3.3.1 Choix de l’événement à exécuter
3.3.2 Choix uniforme des valeurs des paramètres
3.3.3 Les substitutions probabilistes
3.3.4 Machine B événementiel probabiliste
3.3.5 Étude de cas : protocole pair à pair en B événementiel probabiliste
3.4 Cohérence d’une machine B évenementiel probabiliste
3.4.1 Nouvelles obligations de preuve
3.4.2 Adaptation des obligations de preuve standard
3.4.3 Étude de cas : obligations de preuve appliquées au protocole pair à pair
3.5 Sémantique opérationnelle d’une machine B événementiel probabiliste
3.5.1 Notations
3.5.2 Construction du système de transitions probabiliste correspondant à une machine probabiliste
3.5.3 Sémantique opérationnelle exprimée en termes de chaîne de Markov discrète
3.5.4 Étude de cas : sémantique opérationnelle de la machine P2Pp du protocole pair à pair
4 B Événementiel mixte
4.1 Introduction
4.2 Machine B événementiel mixte
4.2.1 Description
4.3 Cohérence d’une machine B événementiel mixte
4.3.1 Cas général
4.3.2 Cas des machines mixtes partielles
4.4 Sémantique opérationnelle d’une machine B événementiel mixte
4.4.1 Construction de la sémantique opérationnelle d’une machine B événementiel mixte
4.4.2 Exemples d’illustration
4.4.3 Sémantique opérationnelle
4.5 Etude de cas : protocole pair à pair
5 Raffinements probabilistes
5.1 Introduction
5.2 Probabilisation
5.2.1 Obligations de preuve de faisabilité de la probabilisation
5.2.2 Automatisation du processus de probabilisation
5.2.3 Étude de cas
5.3 Introduction de nouveaux événements par raffinement
5.3.1 Convergence presque certaine en B événementiel dans la littérature
5.3.2 Convergence presque certaine dans notre proposition de B événementiel probabiliste
5.3.3 Étude de cas : convergence presque certaine dans le protocole P2P
5.4 Généralisation de l’introduction d’événements par raffinement
5.4.1 Ajout de nouveaux événements probabilistes au sein d’une machine B événementiel standard ou mixte
5.4.2 Ajout d’événements standard dans une machine B événementiel mixte ou probabiliste
5.4.3 Ajout simultané d’événements standard et probabilistes
6 Études de cas
6.1 Système d’atterrissage d’un avion
6.2 Stratégie de développement du train d’atterrissage en B événementiel
6.2.1 La première machine
6.2.2 La deuxième machine
6.3 Système de freinage
6.3.1 Stratégie du développement du système de freinage en B événementiel
6.3.2 La première machine
6.3.3 La deuxième machine
6.3.4 La troisième machine : version probabiliste
6.3.5 La quatrième machine
6.3.6 La cinquième machine
7 Conclusion
Télécharger le rapport complet
