B-Method: Difference between revisions
Line 37: | Line 37: | ||
*[http://www.lisi.ensma.fr/members/idir/index.html B2EXPRESS] Animator |
*[http://www.lisi.ensma.fr/members/idir/index.html B2EXPRESS] Animator |
||
*[http://www.b4free.com/ B4free] freeware tools |
*[http://www.b4free.com/ B4free] freeware tools |
||
*[https://gna.org/projects/brillant/ BRILLANT] [[open source]] platform (Parser + Proof Obligation generator + B/COQ prover) |
*[https://gna.org/projects/brillant/ BRILLANT] [[open source]] platform (Parser + Proof Obligation generator + B/COQ prover) [http://vda-wikis.inrets.fr/index.php/Projet_BRILLANT Wiki] |
||
*[http://forum.atronach.com/viewtopic.php?f=15&t=159 DumBeX] B notation to [[Image:LaTeX logo.svg|48px|\LaTeX]] |
*[http://forum.atronach.com/viewtopic.php?f=15&t=159 DumBeX] B notation to [[Image:LaTeX logo.svg|48px|\LaTeX]] |
||
*[http://www.stups.uni-duesseldorf.de/ProB/ ProB] Animator and Model Checker |
*[http://www.stups.uni-duesseldorf.de/ProB/ ProB] Animator and Model Checker |
Revision as of 08:31, 18 August 2010
B is a tool-supported formal method based around AMN (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.
The method of software development based on B is known as the B-Method.
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[1] 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.
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[2] 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.
Books
- The B-Book: Assigning Programs to Meanings, Jean-Raymond Abrial, Cambridge University Press, 1996. ISBN 0-521-49619-5.
- The B-Method: An Introduction, Steve Schneider, 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 Lano, Springer-Verlag, FACIT series, 1996. ISBN 3-540-76033-4.
- Specification in B: An Introduction using the B Toolkit, Kevin Lano, World Scientific Publishing Company, Imperial College Press, 1996. ISBN 1-86094-008-0.
See also
- APCB (Association de Pilotage des Conférences B)
Notes
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 source platform (Parser + Proof Obligation generator + B/COQ prover) Wiki
- DumBeX B notation to
- ProB Animator and Model Checker
- Rodin event-B open source platform
This article is based on material taken from the Free On-line Dictionary of Computing prior to 1 November 2008 and incorporated under the "relicensing" terms of the GFDL, version 1.3 or later.