Méthode B

Restez toujours informé : suivez-nous sur Google (☆)

Introduction

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 implantations concrètes avec le modèle abstrait).

On distingue le :

  • B classique tel qu'il est définit dans le B Book de 1996 . L'outil logiciel de support est l'atelierB .
  • 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). Du coup la méthode peut s'appliquer sur des systèmes variés comme de l'électronique et non plus seulement des programmes. On réalise alors des développements incrémentaux de systèmes prouvés. Pour cela on utilise toujours l'atelierB mais conjointement avec Click'n'Prove
  • 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.
Vue d'un projet et d'une machine dans Click'n'Prove.

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 Click'n'Prove.

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. Meija 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 utilisation 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.

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
/* noter que 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