B-Method
Sign in to saveThe B-Method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software.
Article
19 sectionsContents
- Overview
- Event-B
- The main components
- Abstract machine
- Refinement
- Implementation
- Software
- Atelier B
- B-Toolkit
- Click'n'Prove
- ProB
- Rodin
- Others
- APCB
- Books
- Conferences
- See also
- References
- External links
The B-Method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software.
==Overview== thumb|upright|Jean-Raymond Abrial, the originator of the B-Method and Event-B B was originally developed in the 1980s by Jean-Raymond Abrial in France and the UK. B is related to the Z notation (also originated by Abrial) and supports the development of programming language code from specifications. B has been used in major safety-critical system applications in Europe (such as the automatic Paris Métro lines 14 and 1 and the Ariane 5 rocket). It has robust, commercially available tool support for specification, design, proof and code generation.