Soutenance mémoire
De nos jours, l’informatique est partout dans notre quotidien. Nos téléphones portables et nos voitures sont dotés de logiciels dont le but est de faciliter certaines tâches. De la même manière, les métros automatiques et les centrales électriques sont désormais gérés à l’aide de logiciels, permettant d’assurer plus de disponibilité et de fiabilité. Les conséquences d’une défaillance sur notre téléphone ne sont évidemment pas les mêmes que dans un métro automatique. Par exemple, une défaillance dans un métro ne doit jamais engendrer de collision entre deux rames pour respecter la sécurité des voyageurs. Afin de répondre à ces exigences, des solutions sont proposées dès la phase de spécification des logiciels. Dans ce cadre, comment garantir que ces solutions sont correctement mises en œuvre et qu’ainsi la sécurité est réellement assurée ?
Les méthodes formelles répondent à cette problématique puisqu’elles regroupent un ensemble de méthodes et d’outils permettant d’analyser et de raisonner formellement sur un logiciel. Ces méthodes comprennent un langage formel et, un mécanisme de raisonnement formel ou des techniques de vérification comme dans le model-checking par exemple. Le langage formel est utilisé pour écrire les spécifications du logiciel dans un langage non ambigu, avec une syntaxe et une sémantique précises, exprimées à l’aide de la logique ou de théories logiques comme la théorie des ensembles, théorie des types, . . . Le mécanisme de raisonnement formel permet de prouver des formules à partir d’autres formules ou d’hypothèses. Toutes ces méthodes ont pour objectif de développer le logiciel tout en gardant l’assurance de sa correction vis-à-vis des spécifications.
La méthode B[1] est une méthode formelle qui permet de spécifier, concevoir et implanter un logiciel. Des propriétés peuvent être démontrées sur la spécification à l’aide d’un système de preuve. De plus, toutes les étapes de développement doivent être prouvées correctes vis-à-vis des spécifications formelles et des propriétés qu’elles doivent respecter. Ainsi, le logiciel obtenu respectera les propriétés définies dans les spécifications. Le formalisme sous-jacent à la méthode B combine le langage des prédicats et une théorie des ensembles typée. Dans la suite, nous appellerons théorie B les axiomes et règles d’inférence qui définissent la théorie ensembliste de B. Cette méthode a été utilisée avec succès à de nombreuses reprises par le passé. En particulier, elle a permis à MATRA Transport International (racheté depuis par Siemens) de réaliser la première ligne de métro automatique de Paris (avec le projet Meteor pour la ligne 14) en 1998. Plus récemment, Siemens a aussi automatisé la ligne de métro de New York (Canarsie line) ainsi que le métro de la ligne 1 de Paris, là aussi en utilisant la méthode B.
Plus généralement, Siemens se positionne sur le marché des transports automatisés de personnes avec le VAL (Véhicule Automatique Léger), les automatismes d’aide à la conduite et le guidage optique. Les solutions clés en main, comme le système VAL (un métro entièrement automatique sans conducteur), sont déclinées pour les navettes d’aéroport (Roissy CDG), ou en transport urbain, comme la ligne de métro en service à Rennes. Siemens propose également des automatismes d’aide à la conduite, comme Trainguard MT CBTC : solution de contrôle et commande de trains à forte capacité utilisant un système radio, qui est en service sur la ligne 14 parisienne. Pour finir, Siemens propose le dispositif Optiguide de guidage optique pour bus et trolleys, en service à Rouen et à l’étranger.
Méthode B
La méthode B [1] est une méthode formelle qui permet de spécifier, concevoir et implanter des logiciels. L’étape initiale consiste à définir un modèle abstrait, composé d’un état, un invariant (représentant les propriétés abstraites que le modèle doit respecter) et des opérations qui modifient cet état. Le modèle est ensuite raffiné en plusieurs étapes jusqu’à l’obtention d’un modèle concret à partir duquel du code exécutable peut être généré. Une étape de raffinement consiste à se rapprocher d’une solution algorithmique (supprimer le non-déterminisme, utiliser des structures de données proches de celles que l’on trouve dans les langages de programmation . . . ) tout en respectant les propriétés précédemment définies. Vérifier la cohérence d’un modèle consiste à vérifier que l’invariant est préservé par les opérations. De plus, lorsqu’un modèle résulte d’un raffinement, il faut également vérifier que ce modèle préserve les propriétés établies dans le modèle précédent. Pour vérifier la cohérence de chaque modèle et des raffinements, des obligations de preuve sont générées. Celles-ci doivent être démontrées pour assurer la correction du logiciel développé.
Chez Siemens IC-MOL, l’outil de développement relatif à la méthode B utilisé est l’Atelier B. Il couvre toutes les étapes de développement d’un logiciel, à savoir la spécification (grâce à un modèle abstrait), les étapes de raffinement pour obtenir un modèle concret ainsi que la génération de code. Toutes les obligations de preuve pour vérifier la correction sont générées automatiquement. L’Atelier B offre un prouveur automatique ainsi qu’un environnement de preuve interactif utilisé dans le cas où le prouveur automatique échoue.
Dans cette partie, nous présentons uniquement les notions théoriques relatives à la méthode B, qui sont nécessaires pour la compréhension des chapitres suivants. Des informations complémentaires peuvent être trouvées dans [1]. Le formalisme sous-jacent à la méthode B combine le calcul des prédicats (sur une logique classique) et une théorie ensembliste typée. La syntaxe des formules B est définie inductivement ainsi :
V := I | V 7→ V
E := V | [V := E]E | E 7→ E | S
S := S × S | P(S) | {V |P} | BIG | I
P := P ∧ P | P ⇒ P | ¬P | ∀V.P | [V := E]P | E = E | E ∈ S | I
où V est l’ensemble représentant les variables, I les identificateurs, E les expressions, S les ensembles et P les prédicats. B utilise les notations ensemblistes usuelles, ainsi P(S) désigne l’ensemble des parties de S. On peut remarquer que les substitutions sont explicites dans le langage et que ce ne sont pas des opérations méta. La substitution [V := E]P représente le prédicat P dans lequel les occurrences libres de la variable V sont substituées par l’expression E. Enfin BIG est un ensemble infini. Les autres connecteurs logiques (tels que ⇔, ∨ et ∃) sont définis à partir de ceux donnés ci-dessus. Dans la suite, nous appellerons les notations introduites par la syntaxe et les connecteurs dérivés des constructions B.
Théorie des ensembles de B
Le langage de spécification de la méthode B est une théorie des ensembles proche de la théorie des ensembles de Zermelo-Fraenkel. Cette théorie est typée afin d’éviter le paradoxe de Russell. Six schémas d’axiomes définissent les opérateurs et prédicats de base dont le produit cartésien, l’ensemble des parties, l’ensemble en compréhension et l’égalité ensembliste : Soient deux ensembles s et t, deux expressions E et F, un prédicat P, et une variable x.
SET 1 : (E 7→ F) ∈ (s × t) ⇔ (E ∈ s ∧ F ∈ t).
SET 2 : s ∈ P(t) ⇔ ∀x.(x ∈ s ⇒ x ∈ t), si x\(s, t).
SET 3 : E ∈ {x|x ∈ s ∧ P} ⇔ (E ∈ s ∧ [x := E]P), si x\s.
SET 4 : ∀x.(x ∈ s ⇔ x ∈ t) ⇒ s = t si x\(s, t).
SET 5 : ∃x ∈ s ⇒ choice(s) ∈ s
SET 6 : inf inite(BIG) .
où BIG est un ensemble constant, et x\s signifie que x est non libre dans s, c’est-à-dire que soit x est sous la portée d’un lieur dans s, soit x n’apparaît pas dans s. Nous appelons lieur les constructions suivantes : {V |P},[V := E], ∀V.P et ∃V.P. Les quatres premiers axiomes définissent respectivement le produit cartésien, l’ensemble des parties, l’ensemble en compréhension et l’égalité ensembliste. Le cinquième axiome signifie que si un ensemble a un membre alors l’opérateur choice appliqué à cet ensemble dénote un certain membre de cet ensemble. Enfin, le sixième axiome spécifie que l’ensemble constant BIG est un ensemble infini. Le quatrième axiome peut être considéré comme une équivalence étant donnée que l’implication dans l’autre sens peut être démontrée grâce à la REGLE 9, qui est la règle de remplacement par les égaux. Dans la suite nous considérerons uniquement la version de cet axiome avec l’équivalence que nous appelons SET 4’. Les quatre premiers axiomes (dont SET 4’) permettent de transformer une formule ensembliste en une formule du premier ordre (en utilisant les équivalences de gauche à droite pour les trois premiers et de droite à gauche pour le quatrième). Les opérateurs (∪, ∩, etc.) sont définis à partir des opérateurs de base précédents. Par exemple, l’union est définie à l’aide d’un ensemble en compréhension :
Définition 1 (Union)
Soient a une variable et u, s, t des ensembles.
Si s ⊆ u et t ⊆ u alors
s ∪ t , {a|a ∈ u ∧ (a ∈ s ∨ a ∈ t)} .
Le typage en B
Comme nous l’avons dit précédemment, la méthode B est basée sur une théorie des ensembles typée afin d’éliminer des formules incohérentes, comme le paradoxe de Russell par exemple. Ainsi, la formule ∃x.x ∈ x est mal typée, elle est donc rejetée. En B, les ensembles servent à contraindre les données puisqu’ils peuvent représenter des types. Par exemple, N est un type et des variables d’ensemble arbitraire sont aussi des types. Si T1 et T2 sont des types alors le produit cartésien de ces types T1 × T2 est le type des paires t1 → t2 où t1 est de type T1 et t2 est de type T2. Si T est un type alors les sous-ensembles de T sont de type P(T). Ainsi, si e1 et e2 sont de type T, alors {e1, e2} est de type P(T). La méthode B impose de vérifier le typage d’une formule avant d’essayer de la prouver. Pour cela, chaque variable doit être contrainte par un ensemble que l’on appelle son type support, et tous les ensembles mis en jeu doivent s’organiser de manière cohérente c’est-à-dire avoir des relations d’inclusion ou avoir des types différents.
|
Table des matières
Introduction
1 État de l’art
1.1 Méthode B
1.1.1 Le système d’inférence de B
1.1.2 Théorie des ensembles de B
1.1.3 Le typage en B
1.2 Preuve de formules ensemblistes
1.2.1 État de l’art sur les prouveurs
1.2.2 Plongements de la méthode B
1.2.3 Prouveurs automatiques
1.2.4 Interaction entre les assistants à la preuve et les prouveurs automatiques
2 BCARe : un outil pour la vérification des règles ajoutées de l’Atelier B
2.1 Les règles ajoutées de l’Atelier B
2.1.1 Preuves dans l’Atelier B
2.1.2 Règles
2.1.3 Application d’une règle dans l’Atelier B
2.2 BCARe : les motivations
2.3 Vérification d’une règle
2.4 Le plongement BCoq
2.5 La réification des règles
2.6 Vérification de la non capture de variable
2.7 Vérification du typage
2.7.1 Extension du système de types de B
2.7.2 Inférence de type
2.7.3 Génération du lemme de vérification
2.8 Vérification de la bonne définition
2.9 Vérification de la validité de la règle
3 Automatisation des preuves de vérification avec Ltac
3.1 Vérification du typage
3.2 Vérification de la bonne définition
3.3 Vérification de la validité de la règle
3.3.1 Normalisation
3.3.2 Mise en forme prénexe
3.3.3 Élimination des quantificateurs
3.3.4 Exemple complet de normalisation
3.3.5 Limitations
3.4 Résultats expérimentaux
4 Automatisation de la preuve B avec Zenon
4.1 Motivations
4.2 L’outil de déduction automatique Zenon
4.3 Processus de preuve avec Zenon
4.3.1 Prénormalisation
4.3.2 Interprétation et preuve
4.3.3 Preuve générée par Zenon
4.3.4 Reconstruction de la preuve
4.3.5 Implantation
4.4 Résultats expérimentaux
5 Extension de Zenon à la théorie de B
5.1 Raisonner modulo une théorie
5.1.1 Déduction modulo
5.1.2 Superdéduction
5.2 La superdéduction pour la méthode des tableaux
5.3 Application à la théorie de B
5.3.1 Génération des super-règles
5.3.2 Traitement des relations
5.3.3 Correction et complétude
5.3.4 Traitement des métavariables
5.4 Implantation
5.4.1 Validation avec Coq
5.4.2 Validation avec BCoq
5.5 Résultats expérimentaux
6 Extension de Zenon à toute théorie : Super Zenon
6.1 Calcul des super-règles
6.2 Correction et complétude
6.3 Implantation
6.4 Application à la méthode B
6.5 Traces de Super Zenon
6.5.1 Preuve d’une règle ajoutée
6.5.2 Preuve d’un problème TPTP
6.6 Résultats expérimentaux sur la base de règles
6.7 Résultats expérimentaux sur les problèmes TPTP
7 Résultats expérimentaux et interface graphique
7.1 Comparaison des approches
7.2 Utilisation industrielle de BCARe
7.3 Interface graphique
Conclusion
