Méthode B

Page d’aide sur l’homonymie

Ne doit pas être confondu avec B (langage).

Si ce bandeau n'est plus pertinent, retirez-le. Cliquez ici pour en savoir plus.
Si ce bandeau n'est plus pertinent, retirez-le. Cliquez ici pour en savoir plus.

Le fond de cet article sur l'informatique est à vérifier ().

Améliorez-le ou discutez des points à vérifier. Si vous venez d’apposer le bandeau, merci d’indiquer ici les points à vérifier.

La méthode B est une méthode formelle qui permet le raisonnement sur des systèmes complexes[1] ainsi que le développement logiciel.

La méthode B permet de modéliser de façon abstraite le comportement et les spécifications d'un logiciel dans le langage de B, puis par raffinements successifs d'aboutir à un modèle concret dans un sous-ensemble du langage B transcodable en Ada ou en C, exécutables par une machine concrète. Elle permet de formaliser le système et son environnement de manière abstraite, puis par raffinements successifs, de rajouter les détails au modèle du système. 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[2]. L'outil logiciel de support est l'atelier B ou le B-Toolkit [3], [4].
  • le 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 pour l'étude des systèmes de domaines variés, 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[3].
  • le 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.

Historique de B

[modifier | modifier le code]

Le langage B a été conçu par J.R.Abrial, qui était un des principaux concepteurs de Z dans les années 1980, avec le concours de G. Laffitte, F. Mejia et I. Mc Neal. Il est fondé sur les travaux scientifiques de E.W. Dijkstra, C.A.R. Hoare, C.B. Jones, C. Morgan, He Jifeng (du 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

La première conférence sur le B a eu lieu en France à Nantes les 25, 26 et 1996.

La méthode B a été utilisé avec succès pour plusieurs applications industrielles. On peut citer le développement du logiciel embarqué pour la ligne 14 du métro parisien (METEOR) qui a été modélisé, prouvé et généré à partir de spécifications formelles B. En 2005, la RATP décide d'automatiser la ligne 1 et fait de nouveau appel à la méthode B pour le logiciel embarqué. 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 ou encore Singapour. Le pilote automatique de canton de la navette de l'aéroport Charles de Gaulle fait partie des développements B. Enfin plusieurs métros en cours de développement ou de rénovation font appel à la méthode B pour le développement de logiciels embarqués : Istanbul, Le Caire, Milan, Sao Paulo, Shangai ou encore Toronto.

En 1996, J.R. Abrial publie l'ouvrage The B-Book, Assigning programs to meanings. Il publie en 2010 un autre ouvrage sur le B événementiel : Modeling in Event-B, Hardback.

Objectifs de B

[modifier | modifier le code]

D'un point de vue purement théorique, l'objectif de la méthode B est de prouver qu'il n'y a pas d'écart entre la spécification et le code exécuté.

Alors que les méthodes basées sur des tests permettent juste d'affirmer que les testeurs n'en ont pas trouvé ; et ce, quel que soit le niveau d'automatisation de la génération des scénarios de tests et les moyens mis en œuvre.

Ainsi, le manque de temps et de moyens (forte contrainte dans l'industrie), conduira à un programme inutilisable (car non prouvé), là où les méthodes concurrentes conduisent à des programmes "bugués".

De ce fait, l'utilisateur final ou le commanditaire peut avoir une grande confiance dans le programme. Cette confiance est en particulier essentielle, voire obligatoire, dans le secteur des transports, notamment en aéronautique avec la norme DO-178B ou en ferroviaire (CENELEC EN 50128) car la sécurité des usagers est primordiale.

B couvre la spécification, la conception par raffinements successifs, l'architecture en couches et la traduction en code source (exemple : Ada, C) ; cela permet la mise en œuvre d'optimisations de "haut niveau" ; par exemple :

  • d'écrire les propriétés des éléments à sélectionner dans un ensemble (de contrainte à faire respecter à un train) de manière compréhensible du client final,
  • d'implémenter cette recherche de manière efficace d'un point de vue temps d'exécution (grâce à toute sorte d'optimisations très éloignées de la spécification initiale, notamment du pré-calcul des informations constantes ou des tables de recherches "inversées")
  • de prouver ensuite que la spécification est respectée quelle que soit la branche du code parcourue (y compris dans les cas atypiques mais qui finiront par arriver)

B ne couvre pas la génération du programme exécutable final (exemple .exe) et donc l'optimisation bas niveau, laissant cela aux compilateurs spécialisés.

Exemples

[modifier | modifier le code]

Un exemple de machine abstraite et de son raffinement

[modifier | modifier le code]

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

[modifier | modifier le code]
 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

[modifier | modifier le code]

Références

[modifier | modifier le code]
  1. ↑ JR. Abrial et Dominique.Cansell, « Click’n Prove: Interactive Proofs Within Set Theory », Theorem proving in higher order logics, Springer Berlin Heidelberg,‎ , p. 1-24 (lire en ligne)
  2. ↑ Jean-Raymond Abrial, The B-Book, Assigning Programs to Meanings, Cambridge University Press, 1996, (ISBN 0521496195)
  3. ↑ a et b http://www.atelierb.eu/ : un outil de développement en B
  4. ↑ http://www.b-core.com/btoolkit.html : un outil de développement en B
  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

[modifier | modifier le code]
  • 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

Articles connexes

[modifier | modifier le code]

Sur les autres projets Wikimedia :

  • B-Toolkit, outil développé par la société B-Core

Liens externes

[modifier | modifier le code]

Les outils

[modifier | modifier le code]
  • ABTools Another B Tool : suite d'outils B développé avec ANTLR
  • Atelier B : outil industriel permettant une utilisation opérationnelle de la méthode B pour des développements logiciels.
  • B4free est la version gratuite [obsolète] du cœur de l'atelierB, s'utilise avec Click'n Prove. Il est remplacé depuis par la version communautaire de l'Atelier B.
  • 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, plateforme B-évènementiel basée sur Eclipse
  • ABtools
  • BATCAVE
  • BRILLANT: projet de développement open-source d'outils supportant la méthode B.
  • jBtools
  • DumBeX Traducteur de notation B vers \LaTeX