Sebastian Krings, Michael Butler, Philipp Koerner, Thierry Lecomte, Michael Leuschel & Laurent Voison

The History and Evolution of B and Event-B

The specification language B and its successor Event-B are used for the formal development of software and systems following the correct-by-construction approach. Both are based on first order predicate logic with higher-order sets, relations, functions.

B has originally been developed as a successor to Z by Jean-Raymond Abrial in the 1990s, focusing on two key concepts: using refinement to gradually develop models and tool support for proof and model checking. There are three classes of industrial applications of B:

• B for software (classical B) [1]: refine specifications until B0, a low-level subset of B, is reached and apply code generators
• B for system modelling (Event-B) [2]: verify critical properties, understand why a system is correct
• B for data validation: express properties in B and check data (possibly using a double chain)

In our article, we will first give a primer on B and Event-B, introducing the main language features and how they are used. Afterwards, we will describe the history of B, starting with B's genesis as a tool for software validation [3, 4], discussing industrial applications of B in projects such as train speed control [5] and signalling [6] and other projects with RATP and SNCF performed by Alstom, Line 14 (Meteor) [7] or Canarsie [8].

Following, we will focus on the evolution of B into Event-B and from software to systems modelling, again focusing on industrial applications such as the flushing line NY [9], OCTYS [10], GIK/Railground [11], the HL3 standard [12] and cooperations with Peugeot. Additionally, we will discuss ventures of using B in other domains such as smart cards [13, 14].

The latest language evolution, B for data validation will be presented by discussing its use for Paris Line 1 [15] and the (subway) trains in Barcelona, Amsterdam, Calcutta, Cairo, Singapore and many more locations.

Language evolution aside, we want to discuss tool evolution in the B ecosystem. Both B and Event-B are supported by a range of tools, from provers to animators to model checkers. We want to give an overview over the B-method tools currently in use and their development and history, starting with early tools such as the B-Toolkit [16] to Atelier-B [3] and to Rodin [17] for Event-B. As not all tools are still available, we will also discuss the ones that disappeared or never really appeared.

In addition to industrial success stories, the academic reception of the Bmethod and its tools is notable as well and will be a distinct part of the article. Starting with the B User Workshop, to the ZB conference and further to the ABZ conference series, which brings together researchers working on different specification languages.

Switching from history and evolution to outlook, we want to discuss new language features such as extensions to Event-B and Rodin, and the extended classical B as understood by ProB. Furthermore, we intend to discuss new areas of application both for B as a language as well as for the B-method tools.

References

1. Jean-Raymond Abrial. The B-Book. Cambridge University Press, 1996.
2. Jean-Raymond Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
3. ClearSy. Atelier B, User and Reference Manuals. Aix-en-Provence, France, 2009. Available at http://www.atelierb.eu/.
4. J. R. Abrial. The B tool (Abstract). In Robin E. Bloomfield, Lynn S. Marshall, and Roger B. Jones, editors, VDM ’88 VDM — The Way Ahead, pages 86–87, Berlin, Heidelberg, 1988. Springer Berlin Heidelberg.
5. M. Carnot, C. DaSilva, B. Dehbonei, and F. Mejia. Error-free software development for critical systems using the B-Methodology. In [1992] Proceedings Third International Symposium on Software Reliability Engineering, pages 274–281, Oct 1992.
6. Babak Dehbonei and Fernando Mejia. Formal methods in the railways signalling industry. In Maurice Naftalin, Tim Denvir, and Miquel Bertran, editors, FME ’94: Industrial Benefit of Formal Methods, pages 26–34, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg.
7. Daniel Dollé, Didier Essamé, and Jérôme Falampin. B dans le transport ferroviaire. L’expérience de Siemens Transportation Systems. Technique et Science Informatiques, 22(1):11–32, 2003.
8. Didier Essamé and Daniel Dollé. B in Large-Scale Projects: The Canarsie Line CBTC Experience. In Jacques Julliand and Olga Kouchnarenko, editors, Proceedings B’2007, LNCS 4355, pages 252–254. Springer-Verlag, 2007.
9. Denis Sabatier. Using Formal Proof and B Method at System Level for Industrial Projects. In Proceedings RSSRail 2016, pages 20–31, 2016.
10. Mathieu Comptier, David Déharbe, Julien Molinero Perez, Louis Mussat, Pierre Thibaut, and Denis Sabatier. Safety Analysis of a CBTC System: A Rigorous Approach with Event-B. In Proceedings RSSRail 2017, pages 148–159, 2017.
11. Michael J. Butler, Dana Dghaym, Tomas Fischer, Thai Son Hoang, Klaus Reichl, Colin F. Snook, and Peter Tummeltshammer. Formal Modelling Techniques for Efficient Development of Railway Control Products. In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification - Second International Conference, RSSRail 2017, Pistoia, Italy, November 14-16, 2017, Proceedings, pages 71–86, 2017.
12. Dominik Hansen, Michael Leuschel, David Schneider, Sebastian Krings, Philipp Körner, Thomas Naulin, Nader Nayeri, and Frank Skowron. Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains. In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Southampton, UK, June 5-8, 2018, Proceedings, pages 292–306, 2018.
13. J-L Lanet. The use of B for Smart Card. In Forum on Design Languages (FDL02), September 2002.
14. Marc Benveniste. On Using B in the Design of Secure Micro-controllers: An Experience Report. Electronic Notes in Theoretical Computer Science, 280:3–22, 12 2011.
15. Michael Leuschel, Jérôme Falampin, Fabian Fritz, and Daniel Plagge. Automated Property Verification for Large Scale B Models. In A. Cavalcanti and D. Dams, editors, Proceedings FM 2009, LNCS 5850, pages 708–723. Springer-Verlag, 2009.
16. Matthew Lee and Ib. H. Sørensen. B-tool. In S. Prehn and W. J. Toetenel, editors, VDM’91 Formal Software Development Methods, pages 695–696, Berlin, Heidelberg, 1991. Springer Berlin Heidelberg.
17. Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, and Laurent Voisin. An open extensible tool environment for event-b. In Zhiming Liu and Jifeng He, editors, Formal Methods and Software Engineering, pages 588–605, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg.