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 .
14-705: 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 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 . Compared to Z, B
28-610: A custom X Window Motif Interface for GUI management and runs primarily on the Linux , Mac OS X and Solaris operating systems. The B-Toolkit source code is now available. 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
42-446: A high-level specification to an executable program , including the Rodin tool . These are two important formal methods approaches for software engineering . He is the author of The B-Book: Assigning Programs to Meanings . For much of his career he has been an independent consultant. He was an invited professor at ETH Zurich from 2004 to 2009. Abrial was elected to be a Member of
56-591: 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). 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. APCB ( French : Association de Pilotage des Conférences B ,
70-480: Is a French computer scientist and inventor of the Z and B formal methods . Abrial was a student at the École Polytechnique (class of 1958). Abrial's 1974 paper Data Semantics laid the foundation for a formal approach to Data Models ; although not adopted directly by practitioners, it directly influenced all subsequent models from the Entity-Relationship Model through to RDF . J.-R. Abrial
84-452: 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. Subsequently, another formal method called Event-B has been developed based on
98-663: Is the father of the Z notation (typically used for formal specification of software), during his time at the Programming Research Group under Prof. Tony Hoare within the Oxford University Computing Laboratory (now Oxford University Department of Computer Science ), arriving in 1979 and sharing an office and collaborating with Cliff Jones . He later initiated the B-Method , with better tool-based software development support for refinement from
112-492: The Academia Europaea in 2006. This article about a French computer specialist is a stub . You can help Misplaced Pages by expanding it . 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 during
126-568: The FM'99 World Congress on Formal Methods in Toulouse, France, in 1999. The group and the associated Z notation have been studied as a community of practice . The following proceedings were produced by the Z User Group: The following ZB conference proceedings were jointly produced with the Association de Pilotage des Conférences B (APCB), covering the Z notation and the related B-Method : From 2008,
140-518: The International B Conference Steering Committee ) has organized meetings associated with the B-Method. It has organized ZB conferences with the Z User Group and ABZ conferences, including Abstract State Machines (ASM) as well as the Z notation . The following conferences have explicitly included the B-Method and/or Event-B: Jean-Raymond Abrial Jean-Raymond Abrial (born 6 November 1938)
154-536: The B-Method, support by the Rodin Platform. 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 B notation depends on set theory and first order logic in order to specify different versions of software that covers
SECTION 10
#1732863353392168-736: The ZUM'92 Z User Meeting in London , England . ZUG has organised a series of Z User Meetings approximately every 18 months initially. From 2000, these became the ZB Conference (jointly with the B-Method , co-organized with APCB ), and from 2008 the ABZ Conference (with abstract state machines as well). In 2010, the ABZ Conference also includes Alloy , a Z-like specification language with associated tool support. The Z User Group participated at
182-557: The complete cycle of project development. In the first and the most abstract version, which is called Abstract Machine , the designer should specify the goal of the design. 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
196-462: 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 . The Rodin Platform is a tool that supports Event-B . Rodin is based on an Eclipse software IDE ( integrated development environment ) and provides support for refinement and mathematical proof . The platform
#391608