Méthode B

Méthode B

La méthode B est une méthode formelle de développement logiciel qui permet de modéliser de façon abstraite dans le langage de B le comportement d'un programme, puis par raffinements successifs, d'aboutir à un modèle concret, sous-ensemble du langage transcodable en Ada ou en C.

Une activité de preuve formelle permet de vérifier la cohérence du modèle abstrait et la conformité de chaque raffinement avec le modèle supérieur (prouvant ainsi la conformité de l'ensemble des implémentations concrètes avec le modèle abstrait).

On distingue le :

  • B classique tel qu'il est défini dans le B Book de 1996[1]. L'outil logiciel de support est l'atelier B[2], ou le B-Toolkit [3].
  • B événementiel qui est une évolution utilisant uniquement la notion d'événements pour décrire les actions et non plus les opérations (qui sont proches des routines informatiques). Par conséquent, la méthode peut s'appliquer à des domaines variés comme l'électronique, plus seulement à des programmes. On réalise alors des développements incrémentaux de systèmes prouvés. Pour cela on utilise toujours l'atelier B[2] mais conjointement avec Click'n'Prove [4]
  • B# (B sharp) qui est une reprise du B événementiel avec des éléments de la notation Z. L'atelier logiciel change et s'appelle Rodin[5].
Vue d'un projet et d'une machine dans Click'n'Prove.
Travail sur une preuve dans Click'n'Prove.
Travail sur une preuve dans Rodin.

Sommaire

Historique de B

B, déjà une longue histoire (source : cours vidéo de J.R. Abrial)

  • A été conçu par J.R.Abrial (un des principaux concepteurs de Z dans les années 80).
  • Concours de : G. Laffitte, F. Mejia et I. Mc Neal.
  • Fondé sur les travaux scientifiques de E.W. Dijkstra, C.A.R. Hoare, C.B. Jones, C. Morgan, He Jifeng (Programming Research Group Université d'Oxford).

B s'inscrit dans une longue filiation de recherches fondamentales :

  • 1949 Alan M. Turing, Checking a large routine, Cambridge University
  • 1967 Robert Floyd, Assigning meanings to programs, AMS
  • 1969 C.A.R. Hoare, An axiomatic basis for computer programming,
    CACM
  • 1972 D.L. Parnas, A Technique for Software Module Specification with Examples, CACM
  • 1975 Edsger Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, CACM
  • 1981 David Gries, The Science of Programming, Springer, 1981
  • 1986 Roland Backhouse, Program Construction and Verification, Prentice-Hall, 1986
  • 1986 Cliff B. Jones, Systematic Software Development using VDM, Prentice-Hall
  • 1988 C.A.R. Hoare, Jifeng He, Natural transformations and data refinement, PRG, Oxford
  • 1990 C. Morgan, Programming from Specifications, Prentice-Hall
  • 1996 J.R. Abrial, The B-Book, Assigning programs to meanings, Cambridge University Press
  • 1996 25-26-27 novembre, First B conference in Nantes (France)

Et présente également plusieurs utilisations industrielles exemplaires dont :

  • 1998 Mise en service par la RATP de la ligne de métro 14 (METEOR). Le logiciel critique embarqué a été modélisé, prouvé et généré à partir de spécifications formelles B.
  • 2005 La RATP décide d'automatiser la ligne 1 (La défense/Vincennes) et d'utiliser à nouveau la méthode B.
  • Depuis 1995, de nombreux pilotes automatiques de métros ont été développés, notamment Barcelone, Delhi, Lausanne, Madrid, New York, Pékin (à l'occasion des Jeux Olympiques), Séoul, Singapour, etc. Le pilote automatique de canton de la navette de l'aéroport Charles de Gaule fait partie des développements B. Enfin plusieurs métros en cours de développement / rénovation font appel à B pour le développement de logiciels sécuritaires: Istanbul, Le Caire, Milan, Sao Paulo, Shangai, Toronto, etc.

Objectifs de B

  • Formaliser la spécification,
  • Expliciter la conception,
  • Simplifier la programmation.

B méthode formelle

  • Car toutes les activités sont validées par des preuves formelles.

Couverture de B

B couvre :

  • La spécification,
  • La conception par raffinements successifs,
  • L'architecture en couches,
  • La génération du code exécutable.

Un exemple de machine abstraite et de son raffinement

Nous avons utilisé la notation ASCII de B (: représente l'appartenance ensembliste, <: l'inclusion, & le "et" logique, :: le "devient appartient" (un choix indéterministe d'un élément d'un ensemble), les || la substitution parallèle.)

MACHINE
        swap
VARIABLES
        xx, yy
INVARIANT
        xx : NAT & yy : NAT
INITIALISATION
        xx :: NAT ||
        yy :: NAT
OPERATIONS
        echange =
        BEGIN
                xx := yy
        ||      yy := xx
        END
END

/* La substitution séquencement est interdite dans
   les machines abstraites, ceci afin de forcer à l'abstraction */
REFINEMENT
        swapR
REFINES
        swap
VARIABLES
        xr, yr, zr
INVARIANT
        xr= xx & yr = yy & zr : NAT
INITIALISATION
        xr, yr, zr:= 0, 0, 0
OPERATIONS
        echange =
        BEGIN
                zr := xr
        ;       xr := yr
        ;       yr := zr
        END
END

Un exemple d'utilisation de primitives de composition de machines, le SEES et l'INCLUDES

MACHINE
        trucM4(AA, maxe)
/* machine paramétrée par un SET et un scalaire */
CONSTRAINTS
        maxe : 5..10 &
        card(AA) >maxe
VARIABLES
        var
INVARIANT
        var <: AA &
        card(var) < maxe +1
INITIALISATION
        var := {}
OPERATIONS
        trucM1op =
                ANY ens WHERE ens <: AA & card(ens) < maxe+ 1 THEN
                        var := ens
                END
END
MACHINE
        trucM5(AA,maxe)
CONSTRAINTS
        maxe : 5..10 & card(AA)> maxe
INCLUDES
        tien.trucM4(AA, maxe), mon.trucM4(AA, maxe)
OPERATIONS
        optrucM2 =
                BEGIN
                tien.trucM1op ||
                mon.trucM1op
                END
END

Conférences internationales sur B

Références

  1. ↑ Jean-Raymond Abrial, The B-Book, Assigning Programs to Meanings, Cambridge University Press, 1996, (ISBN 0521496195)
  2. ↑ a et b http://www.atelierb.eu/ : un outil de développement en B
  3. ↑ http://www.b-core.com/btoolkit.html : un outil de développement en B
  4. ↑ http://www.loria.fr/~cansell/cnp.html : le site de la balbulette (Click'n'Prove en Anglais), interface xemacs gratuite pour B4free.
  5. ↑ http://rodin-b-sharp.sourceforge.net/ : Le projet Rodin qui a pour objectif de développer une plate-forme de développement ouverte.

Bibliographie

  • Recensement bibliographique au format BibTeX (lien externe)
  • The B Book, Assigning Programs to Meanings, Cambridge University Press, Cambridge, 1996, (ISBN 0521496195), ouvrage fondateur de la méthode B.
  • Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, LNCS, Springer, 1997
  • Steve Schneider, The B-method, an introduction, Palgrave, 2001, (ISBN 033379284X) (lien externe)
  • E. Sekerinski and K. Sere (editors ), Case Studies Using the B Method, Springer, (ISBN 0-52149619-5)
  • John Wordsworth, Software Engineering with B, Addison-Wesley, (ISBN 0201403560)
  • Kevin Lano, The B Language and Method: A guide to Practical Formal Development, Springer Verlag London Ltd., (ISBN 3-540-76033-4)
  • Henri Habrias et al., Spécification formelle avec B, Hermes Lavoisier, (ISBN 2-7462-0302-2) ([1]
  • J.R. Abrial, Extending B without changing it" in H. Habrias (edit), First B Conference, p. 160-170, 1996
  • J.R. Abrial, Cours d'introduction à B, Etudes de cas et Cours Logique et Preuve, Cassettes vidéo, diffusées par le département informatique de l'I.U.T. de Nantes, 1997
  • J.R. Abrial, Modeling in Event-B, Hardback, Cambridge University Press, 2010, (ISBN 9780521895569) ([2])
  • J.R. Abrial, The B Book en chinois http://www.china-pub.com/19779

Liens externes

Sur les autres projets Wikimedia :

Les outils

  • Atelier B : outil industriel permettant une utilisation opérationnelle de la méthode B pour des développements logiciels.
  • B4free est la version gratuite du cœur de l'atelierB, s'utilise avec Click'n Prove
  • Bart : outil de raffinement automatique
  • Brama Outil de modélisation graphique appliqué aux méthodes formelles. B.
  • ComenC Traducteur de modèles B vers le langage C.
  • CompoSys Méthode et outil pour des descriptions formelles de systèmes.
  • RODIN, la plateforme B-évènementiel basée sur Eclipse
  • ABtools
  • BATCAVE
  • B-Toolkit, outil développé par la société B-Core
  • BRILLANT: projet de développement open-source d'outils supportant la méthode B.
  • jBtools
  • DumBeX Traducteur de notation B vers \LaTeX

A noter : l'Atelier B est maintenant distribué gratuitement par la société Clearsy. Il fonctionne sous Linux, Windows, MacOs et Solaris.

Les sites

  • http://www.methode-b.com/ : Ce site a pour but de présenter différents travaux et sujets de réflexion de la société ClearSy sur la méthode B.

Utilisateurs industriels de la méthode B


Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Méthode B de Wikipédia en français (auteurs)

Игры ⚽ Нужно сделать НИР?

Regardez d'autres dictionnaires:

  • MÉTHODE — Le mot «méthode», d’origine grecque, signifie chemin: celui, tracé à l’avance, qui conduit à un résultat. La méthode ou bien se rapporte à la meilleure façon de conduire un raisonnement, ou bien est un programme de recherche (Aristote: Essayer… …   Encyclopédie Universelle

  • Methode — Méthode Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom …   Wikipédia en Français

  • Methode B — Méthode B Wikibooks propose un ouvrage abordant ce sujet : la méthode B …   Wikipédia en Français

  • Méthode FG — Méthode GF La méthode GF de Wilson, parfois appelée méthode FG, est une méthode de mécanique classique d obtention de certaines coordonnées internes pour une molécule semi rigide vibrante, les coordonnées normales Qk. Les coordonnées normales… …   Wikipédia en Français

  • methode — METHODE. s. f. Maniere de dire ou de faire quelque chose avec un certain ordre & suivant certains principes. Bonne methode. methode facile, aisée, courte, mauvaise. il se sert d une tres bonne methode. sa methode ne vaut rien. c est un homme qui… …   Dictionnaire de l'Académie française

  • Methode S + n — Méthode S+7 La méthode S + 7 est une méthode de création de textes littéraires inventée par l Oulipo consistant à remplacer dans un texte source chaque substantif par le septième substantif qui le suit dans un dictionnaire donné. Pour exemple,… …   Wikipédia en Français

  • Methode S n — Méthode S+7 La méthode S + 7 est une méthode de création de textes littéraires inventée par l Oulipo consistant à remplacer dans un texte source chaque substantif par le septième substantif qui le suit dans un dictionnaire donné. Pour exemple,… …   Wikipédia en Français

  • Méthode S + N — Méthode S+7 La méthode S + 7 est une méthode de création de textes littéraires inventée par l Oulipo consistant à remplacer dans un texte source chaque substantif par le septième substantif qui le suit dans un dictionnaire donné. Pour exemple,… …   Wikipédia en Français

  • Méthode S + n — Méthode S+7 La méthode S + 7 est une méthode de création de textes littéraires inventée par l Oulipo consistant à remplacer dans un texte source chaque substantif par le septième substantif qui le suit dans un dictionnaire donné. Pour exemple,… …   Wikipédia en Français

  • Méthode s + n — Méthode S+7 La méthode S + 7 est une méthode de création de textes littéraires inventée par l Oulipo consistant à remplacer dans un texte source chaque substantif par le septième substantif qui le suit dans un dictionnaire donné. Pour exemple,… …   Wikipédia en Français

  • Methode — steht für: Methode (Erkenntnistheorie), das systematisierte Verfahren zur Gewinnung von Erkenntnissen Methode (Programmierung), in der objektorientierten Programmierung ein ausführbarer Bestandteil einer Objektklasse Methode (Softwaretechnik),… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”