B-Method

Last updated

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. [1] [2]

Contents

Overview

B was originally developed in the 1980s by Jean-Raymond Abrial [3] [4] 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 automatic Paris Métro lines 14 and 1 and the Ariane 5 rocket). [5] [6] [7] 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. The same language is used in specification, design and programming. Mechanisms include encapsulation and data locality.

Event-B

Subsequently, another formal method called Event-B [8] [9] [10] has been developed based on the B-Method, support by the Rodin Platform. [11] [12] Event-B is a formal method aimed at system-level modelling and analysis. Features of Event-B are the use of set theory for modelling, the use of refinement to represent systems at different levels of abstraction, and the use of mathematical proof for verifying consistency between these refinement levels.

The main components

The B notation depends on set theory and first order logic in order to specify different versions of software that covers the complete cycle of project development.

Abstract machine

In the first and the most abstract version, which is called Abstract Machine, the designer should specify the goal of the design.

Refinement

Implementation

Software

B-Toolkit

The B-Toolkit [13] [14] is a collection of programming tools designed to support the use of the B-Tool, [15] is a set theory-based mathematical interpreter, for the purposes of supporting the B-Method. Development was originally undertaken by Ib Holm Sørensen and others, at BP Research and then at B-Core (UK) Limited. [16]

The toolkit uses a custom X Window Motif Interface [17] for GUI management and runs primarily on the Linux, Mac OS X and Solaris operating systems.

The B-Toolkit source code is now available. [18]

Atelier B

Developed by ClearSy, Atelier B [19] [20] is an industrial tool that allows for the operational use of the B Method to develop defect-free proven software (formal software). Two versions are available: 1) Community Edition available to anyone without any restriction; 2) Maintenance Edition for maintenance contract holders only. Atelier B has been used to develop safety automatisms for the various subways installed throughout the world by Alstom and Siemens, and also for Common Criteria certification and the development of system models by ATMEL and STMicroelectronics.

Rodin

The Rodin Platform is a tool that supports Event-B. [8] [21] [11] Rodin is based on an Eclipse software IDE (integrated development environment) and provides support for refinement and mathematical proof. The platform is open source and forms part of the Eclipse framework It is extendable using software component plug-ins. The development of Rodin has been supported by the European Union projects DEPLOY (2008–2012), RODIN (2004–2007), and ADVANCE (2011–2014). [8]

BHDL

BHDL provides a method for the correct design of digital circuits, combining the advantages of the hardware description language VHDL with the formality of B. [22]

APCB

APCB (French : Association de Pilotage des Conférences B, the International B Conference Steering Committee) has organized meetings associated with the B-Method. [23] It has organized ZB conferences with the Z User Group and ABZ conferences, including Abstract State Machines (ASM) as well as the Z notation.

Books

Conferences

The following conferences have explicitly included the B-Method and/or Event-B:

See also

Related Research Articles

<span class="mw-page-title-main">Z notation</span> Formal specification language used for describing and modelling computing systems

The Z notation 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.

The Vienna Development Method (VDM) is one of the longest-established formal methods for the development of computer-based systems. Originating in work done at the IBM Laboratory Vienna in the 1970s, it has grown to include a group of techniques and tools based on a formal specification language—the VDM Specification Language (VDM-SL). It has an extended form, VDM++, which supports the modeling of object-oriented and concurrent systems. Support for VDM includes commercial and academic tools for analyzing models, including support for testing and proving properties of models and generating program code from validated VDM models. There is a history of industrial usage of VDM and its tools and a growing body of research in the formalism has led to notable contributions to the engineering of critical systems, compilers, concurrent systems and in logic for computer science.

A specification language is a formal language in computer science used during systems analysis, requirements analysis, and systems design to describe a system at a much higher level than a programming language, which is used to produce the executable code for a system.

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

In computer science, communicating sequential processes (CSP) is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi, based on message passing via channels. CSP was highly influential in the design of the occam programming language and also influenced the design of programming languages such as Limbo, RaftLib, Erlang, Go, Crystal, and Clojure's core.async.

<span class="mw-page-title-main">Entity–relationship model</span> Model or diagram describing interrelated things

An entity–relationship model describes interrelated things of interest in a specific domain of knowledge. A basic ER model is composed of entity types and specifies relationships that can exist between entities.

Jean-Raymond Abrial is a French computer scientist and inventor of the Z and B formal methods.

In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.

The Z User Group (ZUG) was established in 1992 to promote use and development of the Z notation, a formal specification language for the description of and reasoning about computer-based systems. It was formally constituted on 14 December 1992 during the ZUM'92 Z User Meeting in London, England.

<span class="mw-page-title-main">BCS-FACS</span> Specialist Group of the BCS

BCS-FACS is the BCS Formal Aspects of Computing Science Specialist Group.

<span class="mw-page-title-main">Egon Börger</span> German computer scientist (born 1930)

Egon Börger is a German-born computer scientist based in Italy.

The Toolkit for Conceptual Modeling (TCM) is a collection of software tools to present specifications of software systems in the form of diagrams, tables, trees, and the like. TCM offers editors for techniques used in Structured Analysis as well as editors for object-oriented (UML) techniques. For some of the behavior specification techniques, an interface to model checkers is offered. More in particular, TCM contains the following editors.

<span class="mw-page-title-main">Michael Butler (computer scientist)</span> Irish computer scientist

Michael J. Butler is an Irish computer scientist. As of 2022, he is professor of computer science and Dean of the Faculty of Engineering and Physical Sciences at the University of Southampton, England.

The Meta-IV was an early version of the specification language of the Vienna Development Method formal method for the development of computer-based systems.

<span class="mw-page-title-main">Martin Henson (computer scientist)</span> English computer scientist

Professor Martin C. Henson FBCS FRSA is an English computer scientist based at the University of Essex. He is dean for international affairs and is affiliated to the School of Computer Science & Electronic Engineering. Henson was head of the department of computer science from 2000 to 2006.

Charles Carroll Morgan is an American computer scientist who moved to Australia in his early teens. He completed his education there, including a Doctor of Philosophy (Ph.D.) degree from the University of Sydney, and then moved to the United Kingdom in the early 1980s. In 2000, he returned to Australia.

The Rodin tool is a software tool for formal modelling in Event-B. It was developed as part of several collaborative European Union projects, including initially the RODIN project (2004–2007).

<span class="mw-page-title-main">Dansk Datamatik Center</span> Danish software research and development centre

Dansk Datamatik Center (DDC) was a Danish software research and development centre that existed from 1979 to 1989. Its main purpose was to demonstrate the value of using modern techniques, especially those involving formal methods, in software design and development.

<span class="mw-page-title-main">Ken Robinson (computer scientist)</span> Australian computer scientist (1938–2020)

Kenneth ("Ken") Arthur Robinson was an Australian computer scientist. He has been called "The Father of Formal Methods in Australia".

References

  1. ↑ Cansell, Dominique, and Dominique Méry. "Foundations of the B method." Computing and informatics 22, no. 3-4 (2003): 221-256.
  2. ↑ Butler, Michael, Philipp Körner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, and Laurent Voisin. "The first twenty-five years of industrial use of the B-method." In International Conference on Formal Methods for Industrial Critical Systems, pp. 189-209. Springer, Cham, 2020.
  3. ↑ Jean-Raymond Abrial (1988). "The B Tool (Abstract)" (PDF). In Bloomfield, Robin E.; Marshall, Lynn S.; Jones, Roger B. (eds.). VDM – The Way Ahead, Proc. 2nd VDM-Europe Symposium. Lecture Notes in Computer Science. Vol. 328. Springer. pp. 86–87. doi:10.1007/3-540-50214-9_8. ISBN   978-3-540-50214-2.
  4. ↑ Abrial, J-R., Matthew KO Lee, D. S. Neilson, P. N. Scharbach, and Ib Holm Sørensen. "The B-method." In International Symposium of VDM Europe, pp. 398-405. Springer, Berlin, Heidelberg, 1991.
  5. ↑ Gerhart, Susan, D. Craigen, and Ted Ralston. "Case study: Paris metro signaling system." IEEE Software 11, no. 1 (1994): 32-28.
  6. ↑ Behm, Patrick, Paul Benoit, Alain Faivre, and Jean-Marc Meynadier. "METEOR: A successful application of B in a large project." In International Symposium on Formal Methods, pp. 369-387. Springer, Berlin, Heidelberg, 1999.
  7. ↑ Lecomte, Thierry. "Applying a formal method in industry: a 15-year trajectory." In International workshop on formal methods for industrial critical systems, pp. 26-34. Springer, Berlin, Heidelberg, 2009.
  8. 1 2 3 "Event-B and the Rodin Platform". Event-B.org.
  9. ↑ Butler, Michael. "Decomposition structures for Event-B." In International Conference on Integrated Formal Methods, pp. 20-38. Springer, Berlin, Heidelberg, 2009.
  10. ↑ Abrial, Jean-Raymond. Modeling in Event-B: system and software engineering. Cambridge University Press, 2010.
  11. 1 2 Abrial, Jean-Raymond, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, and Laurent Voisin. "Rodin: an open toolset for modelling and reasoning in Event-B." International journal on software tools for technology transfer 12, no. 6 (2010): 447-466.
  12. ↑ Hoang, Thai Son, Andreas Fürst, and Jean-Raymond Abrial. "Event-B patterns and their tool support." Software & Systems Modeling 12, no. 2 (2013): 229-244.
  13. ↑ "The B-Toolkit". [B-Core (UK) Limited]. 2004. Archived from the original on October 12, 2004. Retrieved February 22, 2012.
  14. ↑ Haughton, Howard, and Kevin Lano. Specification in B: An introduction using the B toolkit. World Scientific, 1996.
  15. ↑ Abrial, Jean-Raymond. "The B Tool." In International Symposium of VDM Europe, pp. 86-87. Springer, Berlin, Heidelberg, 1988.
  16. ↑ Bowen, Jonathan (July 2022). "Ib Holm Sørensen: Ten Years After" (PDF). FACS FACTS . No. 2022–2. BCS-FACS. pp. 41–49. Retrieved 3 August 2022.
  17. ↑ B-Toolkit Requirements Archived 2004-10-12 at the Wayback Machine
  18. ↑ Crichton, Edward. "B-Toolkit source code". GitHub .
  19. ↑ "AtelierB.eu".
  20. ↑ Mentré, David, Claude Marché, Jean-Christophe Filliâtre, and Masashi Asuka. "Discharging proof obligations from Atelier B using multiple automated provers." In International Conference on Abstract State Machines, Alloy, B, VDM, and Z, pp. 238-251. Springer, Berlin, Heidelberg, 2012.
  21. ↑ Abrial, J-R. "A system development process with Event-B and the Rodin platform." In International Conference on formal engineering methods, pp. 1-3. Springer, Berlin, Heidelberg, 2007.
  22. ↑ Aljer, Ammar, Philippe Devienne, Sophie Tison, J-L. Boulanger, and Georges Mariano. "BHDL: Circuit design in B." In Third International Conference on Application of Concurrency to System Design, 2003. Proceedings., pp. 241-242. IEEE, 2003.
  23. ↑ "Association de pilotage des conférences B". librairiecosmopolite.com. Retrieved 27 July 2022.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.