B-Method
Encyclopedia
The B method is method of software development
based on B, a tool-supported formal method based around an abstract machine notation
, used in the development of computer software. It was originally developed by Jean-Raymond Abrial
in France
and the UK
. B is related to the Z notation
(also originated by Abrial) and supports development of programming language
code from specifications. B has been used in major safety-critical system applications in Europe
(such as the Paris Métro Line 14
), and is attracting increasing interest in industry. It has robust, commercially available tool support for specification, design
, proof and code generation
.
Compared to Z, B is slightly more low-level and more focused on refinement to code rather than just formal specification
— hence it is easier to correctly implement a specification written in B than one in Z. In particular, there is good tool support for this.
Recently, another formal method called Event-B has been developed. Event-B is considered an evolution of B (also known as classical B). It is a simpler notation, which is easier to learn and use. It comes with tool support in the form of the Rodin Platform.
The toolkit uses a custom X Window Motif Interface for GUI management and runs primarily on the Linux
and Solaris operating systems. It has been developed by the UK based company B-Core Limited.
Software development
Software development is the development of a software product...
based on B, a tool-supported formal method based around an abstract machine notation
Abstract Machine Notation
The abstract machine notation is a specification language and programming language for specifying abstract machines in the B method, based on the mathematical theory of generalised substitutions....
, used in the development of computer software. It was originally developed by Jean-Raymond Abrial
Jean-Raymond Abrial
Jean-Raymond Abrial is a French computer scientist and inventor of the Z and B formal methods.J.-R. Abrial is the father of the Z notation , during his time at the Programming Research Group within the Oxford University Computing Laboratory, and later the B-Method , two leading...
in France
France
The French Republic , The French Republic , The French Republic , (commonly known as France , is a unitary semi-presidential republic in Western Europe with several overseas territories and islands located on other continents and in the Indian, Pacific, and Atlantic oceans. Metropolitan France...
and the UK
United Kingdom
The United Kingdom of Great Britain and Northern IrelandIn the United Kingdom and Dependencies, other languages have been officially recognised as legitimate autochthonous languages under the European Charter for Regional or Minority Languages...
. B is related to the Z notation
Z notation
The Z notation , named after Zermelo–Fraenkel set theory, is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.-History:...
(also originated by Abrial) and supports development of programming language
Programming language
A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....
code from specifications. B has been used in major safety-critical system applications in Europe
Europe
Europe is, by convention, one of the world's seven continents. Comprising the westernmost peninsula of Eurasia, Europe is generally 'divided' from Asia to its east by the watershed divides of the Ural and Caucasus Mountains, the Ural River, the Caspian and Black Seas, and the waterways connecting...
(such as the Paris Métro Line 14
Paris Metro Line 14
Line 14 of the Paris Métro system connects the stations Saint Lazare and Olympiades on a north-west south-east diagonal across the centre of Paris. It is the twelfth busiest of sixteen lines on the network, and as of 2011, the only one to be operated completely automatically; the second such line...
), and is attracting increasing interest in industry. It has robust, commercially available tool support for specification, design
Software design
Software design is a process of problem solving and planning for a software solution. After the purpose and specifications of software are determined, software developers will design or employ designers to develop a plan for a solution...
, proof and code generation
Automatic programming
In computer science, the term automatic programming identifies a type of computer programming in which some mechanism generates a computer program to allow human programmers to write the code at a higher abstraction level....
.
Compared to Z, B is slightly more low-level and more focused on refinement to code rather than just formal specification
Formal specification
In computer science, a formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not how the system should do it...
— hence it is easier to correctly implement a specification written in B than one in Z. In particular, there is good tool support for this.
Recently, another formal method called Event-B has been developed. Event-B is considered an evolution of B (also known as classical B). It is a simpler notation, which is easier to learn and use. It comes with tool support in the form of the Rodin Platform.
The main components
B notation depends on group theory and first order logic in order to specify different versions of software that covers the complete cycle of project developmentAbstract machine
In the first and the most abstract version, which is called Abstract Machine, designer should specify the goal of the design.Refinement
- Then, during a refinement step, he may pad the specification in order to clarify the goal or to turn the abstract machine more concert by adding more details about data structures and algorithms that explain how the goal may be achieved.
- The new version, which is called Refinement, should be proven to be coherent and including all the properties of the Abstract Machine.
- Designer may make use of many B libraries in order to see data structure, to include or import some components.
Implementation
- The Refinement in its turn may be refined one or many times to obtain a deterministic version which is called Implementation.
- During all of the development steps the same notation is used and the last version may be translated to Ada, C or C++ language.
Some B method characteristics
- Use same language in specification , design and programation.
- Mechanism include encapsulationEncapsulation- Chemistry :* Molecular encapsulation, in chemistry, the confinement of an individual molecule within a larger molecule* Capsule , in pharmacy, the enclosure of a medicine within a relatively stable shell for administration...
and data locality - Clear and close introduction for refinementRefinementIn formal methods, program refinement is the verifiable transformation of an abstract formal specification into a concrete executable program. Stepwise refinement allows this process to be done in stages...
concept - Born in eighteenth by Jean-Raymond AbrialJean-Raymond AbrialJean-Raymond Abrial is a French computer scientist and inventor of the Z and B formal methods.J.-R. Abrial is the father of the Z notation , during his time at the Programming Research Group within the Oxford University Computing Laboratory, and later the B-Method , two leading...
- B method is a tool-supported formal methodsFormal methodsIn computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...
based around AMN (Abstract Machine NotationAbstract Machine NotationThe abstract machine notation is a specification language and programming language for specifying abstract machines in the B method, based on the mathematical theory of generalised substitutions....
), used in the development of correct software - B method has been used in some major safety-critical system applications in EuropeEuropeEurope is, by convention, one of the world's seven continents. Comprising the westernmost peninsula of Eurasia, Europe is generally 'divided' from Asia to its east by the watershed divides of the Ural and Caucasus Mountains, the Ural River, the Caspian and Black Seas, and the waterways connecting...
(such as in Paris Métro Line 14Paris Metro Line 14Line 14 of the Paris Métro system connects the stations Saint Lazare and Olympiades on a north-west south-east diagonal across the centre of Paris. It is the twelfth busiest of sixteen lines on the network, and as of 2011, the only one to be operated completely automatically; the second such line...
and Ariane 5Ariane 5Ariane 5 is, as a part of Ariane rocket family, an expendable launch system used to deliver payloads into geostationary transfer orbit or low Earth orbit . Ariane 5 rockets are manufactured under the authority of the European Space Agency and the Centre National d'Etudes Spatiales...
rocket).
B-Toolkit
The B-Toolkit is a collection of programming tools designed to support the use of the B-Tool, a set theory based mathematical interpreter, for the purposes of a formal software engineering methodology known as the B method.The toolkit uses a custom X Window Motif Interface for GUI management and runs primarily on the Linux
Linux
Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds...
and Solaris operating systems. It has been developed by the UK based company B-Core Limited.
Books
- The B-Book: Assigning Programs to Meanings, Jean-Raymond AbrialJean-Raymond AbrialJean-Raymond Abrial is a French computer scientist and inventor of the Z and B formal methods.J.-R. Abrial is the father of the Z notation , during his time at the Programming Research Group within the Oxford University Computing Laboratory, and later the B-Method , two leading...
, Cambridge University PressCambridge University PressCambridge University Press is the publishing business of the University of Cambridge. Granted letters patent by Henry VIII in 1534, it is the world's oldest publishing house, and the second largest university press in the world...
, 1996. ISBN 0-521-49619-5. - The B-Method: An Introduction, Steve Schneider, PalgravePalgrave- Companies :*Palgrave Macmillan, an academic publishing company[The Palgrave Society], studying the history and genealogy of families with the surname Palgrave or any of its many variants.- People :*John Palsgrave - Companies :*Palgrave Macmillan, an academic publishing company[The Palgrave...
, Cornerstones of Computing series, 2001. ISBN 0-333-79284-X. - Software Engineering with B, John Wordsworth, Addison Wesley Longman, 1996. ISBN 0-201-40356-0.
- The B Language and Method: A Guide to Practical Formal Development, Kevin LanoKevin LanoKevin C. Lano is a British computer scientist.Kevin Lano studied at the University of Reading and the University of Bristol. He was an originator of formal object-oriented techniques, and developed a combination of UML and formal methods in a number of papers and books...
, Springer-VerlagSpringer Science+Business Media- Selected publications :* Encyclopaedia of Mathematics* Ergebnisse der Mathematik und ihrer Grenzgebiete * Graduate Texts in Mathematics * Grothendieck's Séminaire de géométrie algébrique...
, FACIT series, 1996. ISBN 3-540-76033-4. - Specification in B: An Introduction using the B Toolkit, Kevin LanoKevin LanoKevin C. Lano is a British computer scientist.Kevin Lano studied at the University of Reading and the University of Bristol. He was an originator of formal object-oriented techniques, and developed a combination of UML and formal methods in a number of papers and books...
, World Scientific Publishing Company, Imperial College PressImperial College PressImperial College Press was formed in 1995 and is a partnership between Imperial College of Science, Technology and Medicine in London and World Scientific publishing....
, 1996. ISBN 1-86094-008-0.
External links
- B Method.com: this site is designed to present different work and subjects concerning the B method, a formal method with proof
- Atelier B.eu: Atelier B is a systems engineering workshop, which enables software to be developed that is guaranteed to be flawless
- The B-Method in the Virtual Library formal methods pages
- Site B Grenoble
Tools (alphabetical order)
- Atelier B tool
- Batcave A Proof Obligation Generator
- B-Core (UK) Ltd
- B2EXPRESS Animator
- B4free freeware tools
- BRILLANT open sourceOpen sourceThe term open source describes practices in production and development that promote access to the end product's source materials. Some consider open source a philosophy, others consider it a pragmatic methodology...
platform (Parser + Proof Obligation generator + B/COQ prover) Wiki - DumBeX B notation to
- ProB Animator and Model Checker
- RodinRodin toolThe Rodin tool, for formal modelling in Event-B. Event-B is a notation and method developed from the B-Method and is intended to be used with an incremental style of modelling. The idea of incremental modelling has been taken from programming: modern programming languages come with integrated...
event-B open sourceOpen sourceThe term open source describes practices in production and development that promote access to the end product's source materials. Some consider open source a philosophy, others consider it a pragmatic methodology...
platform