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.
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.
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.
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
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)
Kevin Lano, The B Language and Method: A guide to Practical Formal Development, Springer Verlag London Ltd., (ISBN3-540-76033-4)
Henri Habrias et al., Spécification formelle avec B, Hermes Lavoisier, (ISBN2-7462-0302-2) ()
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, (ISBN9780521895569) ()
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.