Séminaire QSL du Pôle ``Intelligence Logicielle''

La Méthode B

28 février 2002

ATTENTION CHANGEMENT DE LIEU
LORIA
salle A008
Campus Scientifique
Vandoeuvre-les-Nancy
 

Repas : servis sur place

Initialement, la Méthode B a été conçue par Jean-Raymond Abrial comme une approche originale de la spécification et de la conception des logiciels en vue d'obtenir des produits d'une très grande fiabilité. Elle a été utilisée avec succès dans le monde industriel, en particulier à l'occasion de la réalisation du logiciel temps-réel assurant la sécurité des rames du métro sans conducteur Météor de la RATP. Ce succès est en partie dû à un ensemble d'outils, appelés collectivement l' Atelier B, dont le développement s'est déroulé sur plusieurs années durant la décennie 90. L'Atelier B a été conçu par Jean-Raymond Abrial et développé et commercialisé par la société ClearSy.

La caractéristique essentielle des logiciels développés en B réside dans le fait que l'ensemble de leur processus de spécification, de conception et de codage est entièrement basé sur la réalisation d'un certain nombre de preuves mathématiques. L'Atelier B contient pour cela un composant spécialisé original, le prouveur, qui est utilisé pour effectuer de façon plus ou moins automatique les preuves en question.

Le but de cette journée est de présenter les différentes facettes de la méthode B. Nous allons montrer que la méthode B, avec l'aide de l'Atelier B et du raffinement permet

• des développements entièrement prouvés de systèmes (académiques ou industriels),
• de prouver des théorèmes en mathématique,
• de trouver des erreurs, des pannes et des défaillances.
• ...

8h30	Accueil des participants
9h00	Modélisation formelle par événements. Jean-Raymond Abrial, Consultant, Marseille On présente la synthèse de travaux récents sur la construction de modèles de systèmes dynamiques discrets. On précise le cadre formel de cette approche. On explique comment le concept de raffinement peut y être défini rigoureusement. On montre le type de raisonnement que l'on peut mettre en oeuvre par la preuve formelle. On présente enfin le panorama de l'utilisation de cette approche: construction d'algorithmes (séquentiels, distribués), construction de circuits électroniques, construction de systèmes complexes, analyse de défaillances, description de mécanismes physiques.
10h00	Les principes de fonctionnements formalisés: modélisation, en B événementiel, des fonctions mécaniques, électriques et informatiques d'un véhicule. Guilhem Pouzancre, ClearSy, Aix en Provence Avec la multiplicité et la complexité des fonctions présentes sur les voitures modernes, l'activité de diagnostic se complique fortement, d'autant plus que les calculateurs multifonctions et les connexions multiplexées obscurcissent le fonctionnement. Pour répondre à ce besoin de diagnostic, nous avons employé la méthode B pour améliorer les descriptions comportementales du véhicule. Le comportement de chaque élément fonctionnel a été décrit dans un modèle B, assurant ainsi une absence totale d'ambiguïtés et un niveau de détail constant. La constitution de ces principes de fonctionnement formalisés a nécessité une méthodologie spécifique, que nous décrivons ici. Ainsi, nous présentons la méthodologie employée pour construire des modèles formels en B qui décrivent le fonctionnement d'éléments mécaniques, électriques ou informatiques à un coût économiquement viable..
10h40	Pause
11h00	Conception incrémentale du protocole d'élection d'un leader du IEEE 1394 (FireWire) Dominique Méry, LORIA-UHP, Nancy Ce travail a été effectué en collaboration avec Jean-Raymond Abrial et Dominique Cansell. Le gros du travail a été réalisé par mail entre Marseille, Nancy et Metz. L'exposé détaillera un développement complet et entièrement prouvé de ce protocole, en utilisant la méthode B-système. Nous expliquerons comment, à partir d'une abstraction initiale où le leader et l'arbre de recouvrement sont construits en un seul coup, nous introduisons les différents messages qui transitent sur le réseau, pour que l'ensemble des sites désigne un leader. A la fin, nous obtenons un raffinement où toutes les décisions d'un site peuvent être prises localement comme dans la réalité. Nous montrerons également l'effort qui a été nécessaire pour définir une théorie des arbres et des théorèmes sur les arbres entièrement prouvés avec l'Atelier B.
11h40	From Formal Specification to an Implementation of an Embedded Verifier for Java Card Lilian Burdy, Gemplus Research Lab, Gémenos The Java security policy is implemented by security components such as the Java Virtual Machine (JVM), the API, the verifier, the loader. It is of prime importance to ensure that the implementation of these components is in accordance with their specifications. In the smart card case study of the Matisse project, one aims to model the Java Card verifier taking into account the whole language and using the B method. The verifier helps the smart card ensuring its own security by checking the downloaded applet before its on-card installation: if the verification fails, the applet is not installed into the card. The byte code verification aims to enforce static constraints on downloaded byte code. Those constraints ensure that the byte code can be safely executed by the virtual machine, and cannot bypass the higher-level security mechanisms. The byte code verification consists in a static analysis of the downloaded applet and ensures that the downloaded applet file is a valid file, there are no stack overflow or underflow, the execution flow is confined to valid byte code, each instruction argument is of the correct type and methods calls are performed in accordance with their visibility attributes (public, protected, etc?). The first point corresponds to the structural verification, and the next points are performed by the type verification. One provides a formal model of each verifier, i.e. the structural verifier and the type verifier. The type verifier is entirely modelled in B. Its development is made simpler as it relies on many services provided by the structural verifier and expressed through an interface. One proves that its implementation is consistent with its specification. The B method allows us to provide a very abstract specification that is split in several modules. In fact, we do not use a simple scheme where the specification is in the abstract machine which is refined and implemented. We provide a formal specification which is made of several modules (abstract machines, refinements and implementation). This formal specification is then refined in order to obtain an implementation. The verifier is then translated into C code automatically from B specification. The C code is compiled and embedded into an ATMEL chip and a demonstration is available. We then discuss the result of such an experiment. In particular, the architecture needed to perform this development and the proof effort is analysed.
12h20	Déjeuner
13h40	Méthodologie de conception et de développement de composants avioniques et utilisations de techniques formelles Yamine Ait-Ameur, Sup'Aero - Toulouse Les systèmes aéronautiques embarqués comprennent un ensemble de programmes répartis sur différents éléments de matériel (calculateurs reliés par des bus, etc). Nous nous intéressons à la partie logicielle de ces systèmes, dits systèmes avioniques, en tenant compte du fait que ce logiciel est plongé dans un environnement matériel avec lequel il interagit. Les logiciels développés pour les systèmes aéronautiques sont des logiciels complexes qui doivent respecter de nombreuses contraintes de sûreté et de fiabilité. La satisfaction de ces contraintes nécessite la mise en ouvre de méthodes et de techniques rigoureuses permettant d'assurer des propriétés des logiciels développés qui expriment ces différentes contraintes. L'utilisation de techniques formelles permet d'exprimer des propriétés traduisant les différents besoins exprimés pour la conception de ces logiciels. La démarche consiste à représenter formellement un modèle du système ainsi que les propriétés qu'il doit satisfaire. La procédure de satisfaction de ces propriétés utilise des techniques formelles de vérification, de preuve, de validation, etc. Il est souvent nécessaire de disposer de plusieurs modèles, pour traiter différents aspects du système (fonctionnel, sûreté de fonctionnement, temps par exemple). De même, il est intéressant d'utiliser différentes techniques de vérification et validation, adaptées aux divers points de vue. Par ailleurs, dans le domaine des systèmes aéronautiques, la conception de logiciels fait souvent appel à des composants logiciels déjà développés pour d'autres systèmes aéronautiques voisins ou similaires. Mais, la réutilisation immédiate de ces composants peut entraîner des dysfonctionnements sur le nouveau système qui n'apparaissaient pas sur l'ancien. Il faut donc être capable de déterminer les propriétés du composant réutilisé qui restent vraies quand on le plonge dans un nouvel environnement. Réciproquement, il faut s'assurer que l'environnement remplit bien certaines conditions nécessaires au bon fonctionnement du composant. Notre exposé comporte deux parties. La première partie présente une notation méthodologique permettant de représenter les composants avioniques ainsi que les opérateurs de composition. Cette notation prend en compte les spécificités du domaine de l'avionique modulaire intégrée. Dans la seconde partie de l'exposé, nous montrons une représentation, dans différentes techniques formelles, de ces notions de composant et de composition. Nous nous intéresserons particulièrement à B et à Lustre. La première est peu utilisée dans ce domaine alors que la seconde est largement utilisée par les concepteurs de systèmes avioniques. Nous discuterons les avantages et inconvénients de chacune de ces techniques du point de vue de la représentation mais aussi du point de vue de l'utilisation. Une étude de cas représentant une partie d'un pilote automatique sera mise en pratique pour illustrer ce travail.
14h20	High-Order Mathematics in B Dominique Cansell, LORIA, INRIA, Metz Ce travail a été réalisé avec la collaboration de Jean-Raymond Abrial et Guy Laffitte. La méthode B ne permettait pas de faire des preuves en logique d'ordre supérieur. Pour faire des preuves par récurrence il faut pouvoir quantifier sur les prédicats. Cela a été permis en quantifiant sur les ensembles car en théorie des ensembles on peut quantifier sur tous les sous-ensembles d'un ensemble. Pour simplifier les preuves et surtout pour faire des preuves "abstraites", comme les mathématiciens, nous avons défini un langage de structuration qui permet de définir des structures mathématiques et leurs théorèmes associés. Nous avons également développé un outil qui traduit des structures en machine B. Nous pouvons, ainsi, utiliser l'Atelier B pour prouver les théorèmes de ces structures. A titre d'exemple nous avons défini des structures qui permettent de démontrer le théorème de Zermelo qui dit que tout ensemble peut être bien ordonné (si l'on dispose de l'axiome du choix). Pour cela il a fallu définir les transfinis associés à un ensemble qui sont eux-mêmes un point fixe, etc.
15h	Pause
15h20	Analyse formelle de défaillance Jean-Raymond Abrial, Consultant, Marseille On présente l'une des utilisations de la modélisation formelle: l'analyse des défaillances de systèmes complexes. On fixe d'abord le cadre méthodologique de cette problématique. On présente ensuite un exemple complet. Les scénarios de défaillance y sont étudiés et prouvés. La complétude de ces scénarios est ensuite complètement prouvée elle aussi. On utilise largement le concept de raffinement pour enfin déployer ces scénarios dans une réalisation pratique.
16h00	Fin de la journée