Méthode B

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 27 novembre 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.

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.

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.

• « NAT » correspond quant à lui à l'ensemble des entiers naturels.

 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

 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

• Première conférence B de Nantes (nov. 25-27 1996)
• Deuxième conférence B à Montpellier (avril 22-24 1998),
• ZB'2000 à York (U.K.) 28 août, 2 sept. 2000),
• ZB'2002 Grenoble (F) (23-25 janv. 2002)
• ZB'2003, Turku (Finlande) (4-6 juin)
• ZB'05, Guildford (U.K.)
• B'2007 Besançon (France)
• B, from research to teaching, Nantes, (France), Cité Internationale des Congrès (16 juin 2008)
• ABZ Conference, September 16-18, 2008 BCS London Offices, Covent Garden, London,
• B, from research to teaching, Nantes, (France), Cité Internationale des Congrès (8 juin 2009)
• ABZ 2010 Conference, Orford, Québec, Canada February 22-25, 2010
• B, from research to teaching, Nantes, (France), Cité Internationale des Congrès (7 juin 2010)
• ABZ conference: ABZ 2012, Pisa, Italy, 18-22 June 2012
• ABZ conference: ABZ 2014, Toulouse, France, 2-6 June 2014
• ABZ conference: ABZ 2016, Linz, Austria, 23-27 May 2016
• 6th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z, 5-8 June 2018

• 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

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

• http://www.methode-b.com/ : Présente différents travaux et sujets de réflexion de la société Clearsy sur la méthode B.
• http://www.clearsy.com/ : la société assurant le développement de l'Atelier B.
• http://tools.clearsy.com/ : Ressources open-source (outils, documents) relatives à B / Event-B, pour faciliter leur exploitation et dissémination.
• http://teachingbconference.blogspot.fr/: From Research to Teaching and Using

• 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 Février 2009 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.
  • Le wiki pour participer au développement : http://vda-wikis.inrets.fr/index.php/Projet_BRILLANT
• jBtools
• DumBeX Traducteur de notation B vers  

•   Portail de la programmation informatique