Précédent Remonter Suivant

Chapitre 4  B et les méthodes formelles



4.1  Les méthodes formelles

4.1.1  Motivation

Les méthodes formelles, issues des travaux du Programming Research Group de l'université d'Oxford, ont été proposées afin d'exprimer le besoin par un formalisme rigoureux, permettant de :

4.1.2  Définition

Une spécification formelle est exprimée dans un langage à syntaxe et sémantique précises, construit sur une base théorique solide et permettant des vérifications automatisées : grâce aux règles de déduction du système formel, on peut démontrer des propriétés de la spécification. Des exemples de cette technique sont : les réseaux de Petri, les grammaires formelles, les automates à états finis, la théorie des graphes et le -calcul.

Un projet est structuré par à un ensemble de relations entre les spécifications, et certaines de ces relations peuvent être prouvées formellement.

4.1.3  Classification

On peut classer les méthodes formelles en quatres catégories :
Approche algébrique.
Types abstraits de données (aucune structure de donnée n'est décrite, seules les opérations le sont), déduction équationnelle : SACSO, LARCH, LPG, OBJ.
Approche dynamique.
Modélisation de l'interaction entre différents processus : CSP, CCS.
Approche logique.
Théorie des types et logiques d'ordre supérieur : PVS, Isabelle/HOL, Coq.
Approche par modèle abstrait.
Définition d'une structure de données et d'un ensemble d'opérations, approche constructive : VDM, Z, B.

4.1.4  Apports aux logiciels critiques

Les logiciels dits critiques sont chargés de piloter des systèmes sensibles, dans lesquels la moindre défaillance peut avoir des conséquences catastrophiques. Le plus souvent, des vies humaines sont en jeu (dans le secteur des transports ou du nucléaire, par exemple). C'est pourquoi les logiciels critiques doivent être tout particulièrement fiables et robustes. Il est donc nécessaire de les certifier, en validant pour cela leurs mécanismes de fonctionnement.

Aux vues des inconsistances du langage naturel et des langages de programmation, il semble alors raisonnable de se tourner vers les méthodes formelles. L'abstraction des fonctionnalités du système à l'aide de formules mathématiques permet en effet d'effectuer le processus de vérification (preuve de propriétés) sur des bases saines et rigoureuses.

4.2  La méthode B

4.2.1  Généralités

Historique

La méthode B1 a été introduite au milieu des années 80 par J.-R. Abrial. Sans entrer dans les détails, il est possible de situer B comme une méthode sous-jacente aux méthodes formelles VDM2 et Z3. Cependant, à la différence de ces dernières, B ne se limite pas à la phase de description : elle permet d'établir une chaîne de production qui va de la spécification du programme au code source associé.

Présentation

L'objectif initial de B est de fournir une technique et des outils associés capables d'aider la construction de logiciels de la façon la plus sûre possible. C'est une méthode transformationnelle : on part d'un modèle abstrait (une machine abstraite), puis on en réduit le niveau d'abstraction, étape par étape (par des raffinements), jusqu'à l'obtention d'un modèle concret, proche du code source (l'implémentation).

L'ensemble des composants spécifiant un comportement (du plus abstrait au plus concret) est appelé module. Un module peut dépendre de plusieurs autres modules, les principes de dépendance seront vus par la suite.

Il est alors possible, pour un projet (un ensemble de modules) donné, de générer un code exécutable sécurisé, car totalement prouvé.

Outils

Il existe deux ateliers de génie logiciel qui permettent la mise en oeuvre de la méthode B dans des projets industriels : l'AtelierB, diffusé par la société française ClearSy, et le B-Toolkit de la société britannique B-Core. Tous deux disposent d'outils pour : Grâce à ces outils, la méthode B a pu être utilisée pour développer des systèmes critiques, dans le domaine des transports4 notamment.

4.2.2  La notation B

Structure d'une machine abstraite

Une machine abstraite est un sous-système de la spécification du logiciel, caractérisé par : Les variables d'état ne peuvent être directement modifiées de l'extérieur de la machine (elles sont encapsulées), c'est pourquoi il est nécessaire d'introduire non seulement des opérations de modification, mais aussi des opérations de consultation permettant aux utilisateurs extérieurs de connaître l'état de la machine.

Une machine abstraite peut être décrite au moyen de nombreuses clauses, dont les plus courantes sont présentées dans le tableau 4.1.

Nom Description
MACHINE en-tête de la machine : nom et paramètres éventuels.
SETS ensembles de base manipulables par la machine. Ces ensembles peuvent être abstraits (aucune indication sur le type des éléments) ou énumérés (définis par la liste de leurs éléments).
DEFINITIONS abréviations utilisables dans le texte des autres classes.
VARIABLES variables de la machine, représentant l'état de la machine. Les variables sont les seules entités qui peuvent être modifiées dans l'étape d'initialisation et dans les opérations de la machine. Toute clause VARIABLES doit être accompagnée des clauses INVARIANT (typage des variables) et INITIALISATION.
INVARIANT ensemble de prédicats (formules logiques) permettant de typer les variables de la machine, de définir des propriétés mathématiques sur les variables, mais aussi de définir certaines contraintes que doit vérifier l'état de la machine à tout moment.
INITIALISATION valeurs initiales des variables de la machine. Toute variable doit être initialisée en satisfaisant l'invariant.
OPERATIONS déclaration et définition des opérations. Les opérations peuvent être paramétrées en entrée et en sortie. Le corps d'une opération définit un comportement, et peut être accompagné d'une pré-condition (PRE) qui fixe les conditions sous lesquelles un appel de l'opération garantit ce comportement.

Table 4.1 : Clauses d'architecture d'une machine abstraite B


La figure 4.1 présente un exemple de machine, dans laquelle on considère un ensemble fini y d'entiers non nuls : . À l'initialisation, cet ensemble est vide : y := Ø. Les seules manipulations autorisées sur cet ensemble sont définies par les opérations lire et maximum, qui permettent respectivement d'ajouter une valeur à l'ensemble y et de récupérer le plus grand entier appartenant à y à un moment donné.


Figure 4.1 : Exemple de machine abstraite


Raffinement

Le raffinement en B permet d'obtenir une machine plus concrète : c'est le moyen de lever le non-déterminisme et de préciser les choix de réalisation, tout en conservant un comportement compatible avec la machine raffinée. L'invariant d'un raffinement contient, en plus du typage des variables et des contraintes liées au modèle, des prédicats de liaison entre les nouvelles variables et les variables du composant raffiné : ils forment l'invariant de collage.

La structure d'un raffinement est très similaire à celle d'une machine abstraite. Seul l'en-tête change : la clause MACHINE est remplacée par une clause REFINEMENT (ou IMPLEMENTATION, s'il s'agit de l'ultime raffinement du module), suivie d'une clause REFINES introduite pour désigner le nom du composant raffiné.

La figure 4.2 propose un raffinement de la machine PetitExemple (vue en figure 4.1) : le composant encapsule une variable z, qui n'est plus un ensemble mais un entier, initialisé à 0. Les manipulations autorisées sur cet entier ont les même signatures que les opérations décrites dans PetitExemple : lire, qui modifie la valeur de z (z := max(z, n)), et maximum, qui fournit la valeur actuelle de z (m := z). On a juste affiné la description du traitement de ces opérations.


Figure 4.2 : Un raffinement possible de PetitExemple


Dépendances entre modules

Un projet B est constitué de différents modules reliés entre eux par des clauses de visibilité, dont les plus importantes sont présentées au tableau 4.2.

Nom Description
INCLUDES composition de plusieurs machines (utilisé dans les machines abstraites et les raffinements intermédiaires). Une machine ne peut être incluse qu'une seule fois dans l'ensemble d'un projet.
IMPORTS même principe que la clause INCLUDES, mais pour les implémentations.
USES partage de données entre machines (aucun accès aux opérations d'une machine utilisée).
SEES accès en lecture seule aux constituants d'une machine (impossibilité d'appeler une opération de modification).

Table 4.2 : Clauses de visibilité d'un composant B


4.2.3  Fondements théoriques

Nous évoquons dans ce paragraphe les principales notions théoriques utilisées dans la méthode B. Toute la théorie de la méthode B est présentée dans l'ouvrage [1].

La théorie des ensembles et les types

La théorie des ensembles est la base des modèles mathématiques en B. Les relations et les fonctions (partielles ou totales) sont représentées par des ensembles de couples. Les variables sont typées par des prédicats (situés dans l'invariant et les pré-conditions), qui expriment une condition d'appartenance de chaque variable à un ensemble donné.

Le langage des substitutions généralisées

Chaque machine abstraite B englobe un état et fournit des opérations permettant d'accéder à celui-ci ou de le modifier. Les mécanismes qui déterminent ou changent l'état sont appelées substitutions, et l'ensemble des substitutions utilisables dans le langage B pour décrire les initialisations et le corps des opérations constitue le langage des substitutions généralisées.




Une substitution modélise ainsi une transaction entre un état pré et un état post, qui correspond, dans les langages de programmation, à une suite d'instructions non interruptible. Les principales substitutions sont :
substitution neutre
SKIP, qui aboutit à un état post identique à l'état pré
substitution simple
x := E, qui a pour effet d'affecter à la variable x la valeur de l'expression E
substitution multiple
x, y := E, F, qui exécute en parallèle les substitutions simples x := E et y := F (on peut également noter x := E || y := F)
substitution devient tel que
, qui affecte à x une valeur (indéterminée) de l'ensemble S




Les substitutions peuvent ensuite être combinées entre elles au moyen d'opérateurs de composition (par la suite, P et R désignent des prédicats, G et H des substitutions) :
séquencement
G ; H, correspondant à l'application successive des substitutions G et H
()
substitution pré-conditionnée
P | G, assurant que la substitution G aboutira à un état post correct si le prédicat P est vérifié à l'état pré ()
substitution gardée
, qui ne peut être appliquée que dans le cas où l'état pré satisfait P ()
substitution de choix borné
, qui résulte en l'application de l'une ou l'autre (indéterminisme) des substitutions G ou H ()
substitution de choix non borné
@z.G, correspondant à l'application de la substitution G pour une valeur quelconque (indéterminisme) de la variable z (, z étant non libre dans R)

La preuve

À chaque étape du développement, des obligations de preuve sont imposées par la méthode B. Une obligation de preuve est une propriété qui doit être satisfaite pour que le système construit soit correct.

Au niveau des machines abstraites, la preuve consiste à vérifier l'établissement et la conservation de l'invariant :
  1. l'initialisation U doit établir l'invariant I : [U]I
  2. si l'invariant I est établi, alors toute opération de la forme PRE P THEN G END (substitution P | G) doit le garder établi, en vérifiant pour cela le prédicat
Au niveau d'un raffinement, les obligations de preuve consistent à montrer que le modèle raffiné est cohérent avec le modèle abstrait :
  1. il s'agit d'abord de montrer que l'initialisation Ur du raffinement ne fait rien qui soit contraire à l'initialisation U du composant abstrait : [Ur] ¬ [U] ¬ Ir
  2. il s'agit ensuite de montrer que l'exécution d'une opération du raffinement qui établit l'invariant correspond à une exécution de l'opération respective du niveau abstrait :

1
Le choix de la lettre B est un hommage à Bourbaki, groupe de mathématiciens français qui entreprit en 1939 une refonte des mathématiques, en les reprenant à leur point de départ logique.
2
Vienna Development Method, issue de recherches réalisées au laboratoire IBM de Vienne dans les années 60. Mise au point par Bjorner et Jones au cours des années 70.
3
Notation introduite par Abrial dans les années 70 (Z comme Zermelo).
4
La méthode B a été utilisée dans le cadre du projet de métro sans conducteur METEOR (actuellement en exploitation à Paris sur la ligne n14 de la RATP), afin de prouver que les parties de logiciel concernant la sécurité des voyageurs étaient complètement sûres.

Précédent Remonter Suivant