The B method is a method of

software development Software development is the process of conceiving, specifying, designing, programming, documenting, testing, and bug fixing involved in creating and maintaining applications, frameworks, or other software components. Software development invol ...

based on B, a tool-supported

formal method In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expec ...

based on an

abstract machine notation Abstract may refer to: * ''Abstract'' (album), 1962 album by Joe Harriott * Abstract of title a summary of the documents affecting title to parcel of land * Abstract (law), a summary of a legal document * Abstract (summary), in academic publishin ...

, used in the development of computer

software Software is a set of computer programs and associated documentation and data. This is in contrast to hardware, from which the system is built and which actually performs the work. At the lowest programming level, executable code consists ...

Overview

B was originally developed in the 1980s by

Jean-Raymond Abrial Jean-Raymond Abrial (born 1938) is a French computer scientist and inventor of the Z and B formal methods. Abrial's 1974 paper ''Data Semantics'' laid the foundation for a formal approach to Data Models; although not adopted directly by practit ...

France France (), officially the French Republic ( ), is a country primarily located in Western Europe. It also comprises of Overseas France, overseas regions and territories in the Americas and the Atlantic Ocean, Atlantic, Pacific Ocean, Pac ...

and the UK. B is related to the

Z notation 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. History In 1974, Jean-Raymond Abrial ...

(also originated by Abrial) and supports development of

programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming ...

code from specifications. B has been used in major

safety-critical system A safety-critical system (SCS) or life-critical system is a system whose failure or malfunction may result in one (or more) of the following outcomes: * death or serious injury to people * loss or severe damage to equipment/property * environme ...

applications in

Europe Europe is a large peninsula conventionally considered a continent in its own right because of its great physical size and the weight of its history and traditions. Europe is also considered a Continent#Subcontinents, subcontinent of Eurasia ...

(such as the automatic Paris Métro lines 14 and 1 and the

Ariane 5 Ariane 5 is a European heavy-lift space launch vehicle developed and operated by Arianespace for the European Space Agency (ESA). It is launched from the Centre Spatial Guyanais (CSG) in French Guiana. It has been used to deliver payloads int ...

rocket). It has robust, commercially available tool support for

specification A specification often refers to a set of documented requirements to be satisfied by a material, design, product, or service. A specification is often a type of technical standard. There are different types of technical or engineering specificati ...

design A design is a plan or specification for the construction of an object or system or for the implementation of an activity or process or the result of that plan or specification in the form of a prototype, product, or process. The verb ''to design'' ...

, proof and code generation. Compared to Z, B is slightly more low-level and more focused on

refinement Refinement may refer to: Mathematics * Equilibrium refinement, the identification of actualized equilibria in game theory * Refinement of an equivalence relation, in mathematics ** Refinement (topology), the refinement of an open cover in mathem ...

to code rather than just

formal specification 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 verif ...

— 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 has been developed based on the B-Method, support by the

Rodin François Auguste René Rodin (12 November 184017 November 1917) was a French sculptor, generally considered the founder of modern sculpture. He was schooled traditionally and took a craftsman-like approach to his work. Rodin possessed a uniqu ...

Platform.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. 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 Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly conce ...

and

first order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...

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

* Then, during a refinement step, they may pad the specification in order to clarify the goal or to turn the abstract machine more concrete by adding details about data structures and algorithms that define, how the goal is achieved. * The new version, which is called ''Refinement'', should be proven to be coherent and including all the properties of the abstract machine. * The designer may make use of B libraries in order to model data structures or to include or import existing components.

Implementation

* The refinement continues until a deterministic version is achieved: the ''Implementation''. * During all of the development steps the same notation is used and the last version may be translated to a

for compilation.

Software

B-Toolkit

The B-Toolkit is a collection of programming tools designed to support the use of the B-Tool, 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. The toolkit uses a custom

X Window The X Window System (X11, or simply X) is a windowing system for bitmap displays, common on Unix-like operating systems. X provides the basic framework for a GUI environment: drawing and moving windows on the display device and interacting wit ...

Motif Interface for GUI management and runs primarily on the

Linux Linux ( or ) is a family of open-source Unix-like operating systems based on the Linux kernel, an operating system kernel first released on September 17, 1991, by Linus Torvalds. Linux is typically packaged as a Linux distribution, which ...

Mac OS X macOS (; previously OS X and originally Mac OS X) is a Unix operating system developed and marketed by Apple Inc. since 2001. It is the primary operating system for Apple's Mac (computer), Mac computers. Within the market of ...

and

Solaris Solaris may refer to: Arts and entertainment Literature, television and film * ''Solaris'' (novel), a 1961 science fiction novel by Stanisław Lem ** ''Solaris'' (1968 film), directed by Boris Nirenburg ** ''Solaris'' (1972 film), directed by ...

operating systems. The B-Toolkit source code is now available.

Atelier B

Developed by ClearSy, Atelier B 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 Alstom SA is a French multinational rolling stock manufacturer operating worldwide in rail transport markets, active in the fields of passenger transportation, signalling, and locomotives, with products including the AGV, TGV, Eurostar, Avelia ...

and

Siemens Siemens AG ( ) is a German multinational conglomerate corporation and the largest industrial manufacturing company in Europe headquartered in Munich with branch offices abroad. The principal divisions of the corporation are ''Industry'', '' ...

, and also for Common Criteria certification and the development of system models by

ATMEL Atmel Corporation was a creator and manufacturer of semiconductors before being subsumed by Microchip Technology in 2016. Atmel was founded in 1984. The company focused on embedded systems built around microcontrollers. Its products included micr ...

and

STMicroelectronics STMicroelectronics N.V. commonly referred as ST or STMicro is a Dutch multinational corporation and technology company of French-Italian origin headquartered in Plan-les-Ouates near Geneva, Switzerland and listed on the French stock market. ST ...

Rodin

The Rodin Platform is a tool that supports Event-B. Rodin is based on an

Eclipse An eclipse is an astronomical event that occurs when an astronomical object or spacecraft is temporarily obscured, by passing into the shadow of another body or by having another body pass between it and the viewer. This alignment of three ce ...

software IDE (

integrated development environment An integrated development environment (IDE) is a software application that provides comprehensive facilities to computer programmers for software development. An IDE normally consists of at least a source code editor, build automation tools a ...

) and provides support for

and

mathematical proof A mathematical proof is an inferential argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every proo ...

. The platform is

open source Open source is source code that is made freely available for possible modification and redistribution. Products include permission to use the source code, design documents, or content of the product. The open-source model is a decentralized sof ...

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 The European Union (EU) is a supranational political and economic union of member states that are located primarily in Europe. The union has a total area of and an estimated total population of about 447million. The EU has often been des ...

projects DEPLOY (2008–2012), RODIN (2004–2007), and ADVANCE (2011–2014).

BHDL

BHDL provides a method for the correct design of

digital circuit In theoretical computer science, a circuit is a model of computation in which input values proceed through a sequence of gates, each of which computes a function. Circuits of this kind provide a generalization of Boolean circuits and a mathematical ...

s, combining the advantages of the hardware description language

VHDL The VHSIC Hardware Description Language (VHDL) is a hardware description language (HDL) that can model the behavior and structure of digital systems at multiple levels of abstraction, ranging from the system level down to that of logic gates ...

with the formality of B.

APCB

APCB (''Association de Pilotage des Conférences B'', in English the ''International B Conference Steering Committee'') has organized meetings associated with the B-Method. It has organized ZB conferences with the

Z User Group 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 du ...

and ABZ conferences, including

Abstract State Machines In computer science, an abstract state machine (ASM) is a state machine operating on states that are arbitrary data structures (structure in the sense of mathematical logic, that is a nonempty set together with a number of functions ( operations ...

(ASM) as well as the

Books

*''The B-Book: Assigning Programs to Meanings'',

Cambridge University Press Cambridge University Press is the university press of the University of Cambridge. Granted letters patent by Henry VIII of England, King Henry VIII in 1534, it is the oldest university press A university press is an academic publishing hou ...

, 1996. . *''The B-Method: An Introduction'', Steve Schneider,

Palgrave Macmillan Palgrave Macmillan is a British academic and trade publishing company headquartered in the London Borough of Camden. Its programme includes textbooks, journals, monographs, professional and reference works in print and online. It maintains off ...

, Cornerstones of Computing series, 2001. . *''Software Engineering with B'', John Wordsworth,

Addison Wesley Longman Addison-Wesley is an American publisher of textbooks and computer literature. It is an Imprint (trade name), imprint of Pearson PLC, a global publishing and education company. In addition to publishing books, Addison-Wesley also distributes its te ...

, 1996. . *''The B Language and Method: A Guide to Practical Formal Development'',

Kevin Lano Kevin C. Lano (born 1963) is a British computer scientist. Life and work Kevin Lano studied at the University of Reading, attaining a first class degree in Mathematics and Computer Science, and the University of Bristol where he completed his ...

Springer-Verlag Springer Science+Business Media, commonly known as Springer, is a German multinational publishing company of books, e-books and peer-reviewed journals in science, humanities, technical and medical (STM) publishing. Originally founded in 1842 in ...

, FACIT series, 1996. . *''Specification in B: An Introduction using the B Toolkit'',

World Scientific Publishing Company World Scientific Publishing is an academic publisher of scientific, technical, and medical books and journals headquartered in Singapore. The company was founded in 1981. It publishes about 600 books annually, along with 135 journals in various f ...

Imperial College Press Imperial College Press (ICP) was formed in 1995 as a partnership between Imperial College of Science, Technology and Medicine in London and World Scientific publishing. This publishing house was awarded the rights, by The Nobel Foundation, Swede ...

, 1996. . *''Modeling in Event-B: System and Software Engineering'',

, 2010. .

Conferences

The following conferences have explicitly included the B-Method and/or Event-B: *Z2B Conference,

Nantes Nantes (, , ; Gallo: or ; ) is a city in Loire-Atlantique on the Loire, from the Atlantic coast. The city is the sixth largest in France, with a population of 314,138 in Nantes proper and a metropolitan area of nearly 1 million inhabita ...

, 10–12 October 1995 *First B Conference, Nantes, France, 25–27 November 1996 *Second B Conference,

Montpellier Montpellier (, , ; oc, Montpelhièr ) is a city in southern France near the Mediterranean Sea. One of the largest urban centres in the region of Occitania (administrative region), Occitania, Montpellier is the prefecture of the Departments of ...

, France, 22–24 April 1998 *ZB 2000,

York York is a cathedral city with Roman origins, sited at the confluence of the rivers Ouse and Foss in North Yorkshire, England. It is the historic county town of Yorkshire. The city has many historic buildings and other structures, such as a ...

United Kingdom The United Kingdom of Great Britain and Northern Ireland, commonly known as the United Kingdom (UK) or Britain, is a country in Europe, off the north-western coast of the continental mainland. It comprises England, Scotland, Wales and North ...

, 28 August – 2 September 2000 *ZB 2002,

Grenoble lat, Gratianopolis , commune status = Prefecture and commune , image = Panorama grenoble.png , image size = , caption = From upper left: Panorama of the city, Grenoble’s cable cars, place Saint- ...

, France, 23–25 January 2002 *ZB 2003,

Turku Turku ( ; ; sv, Åbo, ) is a city and former capital on the southwest coast of Finland at the mouth of the Aura River, in the region of Finland Proper (''Varsinais-Suomi'') and the former Turku and Pori Province (''Turun ja Porin lääni''; ...

Finland Finland ( fi, Suomi ; sv, Finland ), officially the Republic of Finland (; ), is a Nordic country in Northern Europe. It shares land borders with Sweden to the northwest, Norway to the north, and Russia to the east, with the Gulf of B ...

, 4–6 June 2003 *ZB 2005,

Guildford Guildford () is a town in west Surrey, around southwest of central London. As of the 2011 census, the town has a population of about 77,000 and is the seat of the wider Borough of Guildford, which had around inhabitants in . The name "Guildf ...

, United Kingdom, 2005 *B 2007,

Besançon Besançon (, , , ; archaic german: Bisanz; la, Vesontio) is the prefecture of the department of Doubs in the region of Bourgogne-Franche-Comté. The city is located in Eastern France, close to the Jura Mountains and the border with Switzerl ...

, France, 2007 *B, from research to teaching, Nantes, France, 16 June 2008 *B, from research to teaching, Nantes, France, 8 June 2009 *B, from research to teaching, Nantes, France, 7 June 2010 *ABZ 2008,

British Computer Society Sir Maurice Wilkes served as the first President of BCS in 1957 BCS, The Chartered Institute for IT, known as the British Computer Society until 2009, is a professional body and a learned society that represents those working in infor ...

London London is the capital and largest city of England and the United Kingdom, with a population of just under 9 million. It stands on the River Thames in south-east England at the head of a estuary down to the North Sea, and has been a majo ...

, United Kingdom, 16–18 September 2008 *ABZ 2010, Orford,

Québec Quebec ( ; )According to the Government of Canada, Canadian government, ''Québec'' (with the acute accent) is the official name in Canadian French and ''Quebec'' (without the accent) is the province's official name in Canadian English is ...

Canada Canada is a country in North America. Its ten provinces and three territories extend from the Atlantic Ocean to the Pacific Ocean and northward into the Arctic Ocean, covering over , making it the world's second-largest country by tot ...

, 23–25 February 2010 *ABZ 2012,

Pisa Pisa ( , or ) is a city and ''comune'' in Tuscany, central Italy, straddling the Arno just before it empties into the Ligurian Sea. It is the capital city of the Province of Pisa. Although Pisa is known worldwide for its leaning tower, the cit ...

Italy Italy ( it, Italia ), officially the Italian Republic, ) or the Republic of Italy, is a country in Southern Europe. It is located in the middle of the Mediterranean Sea, and its territory largely coincides with the homonymous geographical re ...

, 18–22 June 2012 *ABZ 2014,

Toulouse Toulouse ( , ; oc, Tolosa ) is the prefecture of the French department of Haute-Garonne and of the larger region of Occitania. The city is on the banks of the River Garonne, from the Mediterranean Sea, from the Atlantic Ocean and from Par ...

, France, 2–6 June 2014 *ABZ 2016,

Linz Linz ( , ; cs, Linec) is the capital of Upper Austria and third-largest city in Austria. In the north of the country, it is on the Danube south of the Czech border. In 2018, the population was 204,846. In 2009, it was a European Capital of ...

Austria Austria, , bar, Östareich officially the Republic of Austria, is a country in the southern part of Central Europe, lying in the Eastern Alps. It is a federation of nine states, one of which is the capital, Vienna, the most populous ...

, 23–27 May 2016 *ABZ 2018,

Southampton Southampton () is a port city in the ceremonial county of Hampshire in southern England. It is located approximately south-west of London and west of Portsmouth. The city forms part of the South Hampshire built-up area, which also covers Po ...

, United Kingdom, 2018 *ABZ 2020,

Ulm Ulm () is a city in the German state of Baden-Württemberg, situated on the river Danube on the border with Bavaria. The city, which has an estimated population of more than 126,000 (2018), forms an urban district of its own (german: link=no, ...

Germany Germany,, officially the Federal Republic of Germany, is a country in Central Europe. It is the second most populous country in Europe after Russia, and the most populous member state of the European Union. Germany is situated betwe ...

, 2021 (delayed due to the

COVID-19 pandemic The COVID-19 pandemic, also known as the coronavirus pandemic, is an ongoing global pandemic of coronavirus disease 2019 (COVID-19) caused by severe acute respiratory syndrome coronavirus 2 (SARS-CoV-2). The novel virus was first identif ...

) *ABZ 2021, Ulm, Germany, 2021

References

External links

B Method.com
– work and subjects concerning the B method, a formal method with proof

{{Webarchive, url=https://web.archive.org/web/20080221232310/http://www.atelierb.eu/index_en.html , date=2008-02-21 : Atelier B is a systems engineering workshop, which enables software to be developed that is guaranteed to be flawless
Site B Grenoble
Formal methods Formal methods tools Formal specification languages