Method B

The method B is a formal method of software development which makes it possible to model in an abstract way in the language of B the behavior of a program, then by successive refinements, to lead to a concrete model, subset of the language transcodable in Ada or C.

An activity of formal evidence makes it possible to check the coherence of the abstract model and the conformity of each refinement with the higher model (thus proving the conformity of the whole of the concrete establishments with the abstract model).

It is distinguished:

  • B traditional such as it east defines in B Book of 1996. The software tool of support is the atelierB.
  • B event-driven which is an evolution using only the concept of events to describe the actions and either the operations (which are close to the data-processing routines). Blow the method can apply to systems varied like electronics and either only of the programs. One then carries out incrémentaux developments of proven systems. For that one always uses the atelierB
  • B# (B sharp) which is a resumption of B event-driven with elements of the Notation Z. The software workshop changes and is called Rodin.

History of B

B, already a long story (source: video course of J.R. Abrial)

  • was conceived by J.R.Abrial (one of the principal originators of Z in the Eighties).

  • Contest of: G. Laffitte, F. Meija and I. Mc Neal.

  • Founded on the scientific work of E.W. Dijkstra, C.A.R. Hoare, C.B. Jones, C. Morgan, He Jifeng (Programming Research Group University of Oxford).

B falls under a long filiation of basic research:

  • 1949 Alan Mr. Turing, Checking has broad 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, has Technical for Software Modulates Specification with Examples, CACM
  • 1975 Edsger Dijkstra, Guarded commands, nondeterminacy and formal derivation off programs, CACM
  • 1981 David Gries, The Science off 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 dated refinement, PRG, Oxford
  • 1990 C. Morgan, Programming from Specifications, Prentice-Hall
  • 1996 J.R. Abrial, The B-Book, Assigning programs to meanings, Cambridge University Close
  • 1996 25-26- November 27th, First B conference in Nantes (France)

And also several use presents industrial specimens of which:

  • 1998 Startup by the RATP of the underground line 14 (METEOR). The embarked critical software was modelled, proven and generated starting from formal specifications B.

  • the 2005 RATP decides to automate line 1 (defense/Vincennes) and to use the method B again.

Objectives of B

  • To formalize the specification,

  • To clarify the design,
  • To simplify the programming.

B formal method

  • Because all the activities are validated by formal evidences.

Cover of B

B covers:
  • specification,
  • design by successive refinements,
  • architecture in layers,
  • the generation of the achievable code.

An example of abstract machine and its refining

We used the ASCII notation of B (: represent the membership ensemblist, <: inclusion, & the " et" logic,
the " becomes appartient" (a indeterminist choice of an element of a unit), them || parallel substitution.

MACHINE swap VARIABLES xx, yy INVARIANT xx: NAT & yy: NAT INITIALIZATION xx:: NAT || yy:: NAT OPERATIONS exchange = BEGIN xx: = yy || yy: = xx END END /* to note that substitution sequencing is prohibited in abstract machines. This in order to force with the abstraction * REFINEMENT swapR REFINES swap VARIABLES xr, yr, Zr INVARIANT xr= xx & yr = yy & Zr: NAT INITIALIZATION xr, yr, Zr: = 0,0,0 OPERATIONS exchange = BEGIN Zr: = xr; xr: = yr; yr: = Zr END END

An example of use of primitives of composition of machines, the SEES and the INCLUDES

MACHINE trucM4 (AA, maxe) /* machine parameterized by a SET and a scalar * CONSTRAINTS maxe: 5..10 & card (AA) >maxe VARIABLES VAr INVARIANT VAr <: AA & card (VAr) < maxe +1 INITIALIZATION 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

International Conferences on B

  • After conference Z2B of Nantes (Oct. 10-12 1995),
      • * then the first conference B of Nantes (Nov. 25-27 1996),
      • * then the second in Montpellier (April 22 - 24 1998),
  • there were conferences about every 18 months
    • ZB' 2000 in York (the U.K.) August 28th, Sept. 2, 2000),
    • ZB' 2002 Grenoble (F) (23-25 janv. 2002),
    • ** ZB' 2003, Turku (Finland) (4 June 6th),
      • ** ZB' 05, Guildford (the U.K.)
      • ** B' 2007 Besancon (France)
      • the site, the bibtex, the acts
    • B, from research to teaching, Nantes, (France), Quoted International of the Congresses, June 16th, 2008
    • ABZ Conference, September 16-18, 2008 BCS London Offices, Covent Garden, London,
      • == Références ==
Random links:Aywaille | Offense of initiate | District of Briançon | Échalou | Francis Cabrel | Relampago,_le_Texas