# Méthode B

La méthode B est une méthode formelle qui permet le raisonnement sur des systèmes complexes 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. L'outil logiciel de support est l'atelier B ou le B-Toolkit$^,$.
* 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.
* 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.

## Historique de 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.

## Objectifs de B

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
### 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.
* « NAT » correspond quant à lui à l'ensemble des entiers naturels.

### Un exemple d'utilisation de primitives de composition de machines, le SEES et l'INCLUDES
## Conférences internationales sur B

* 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