Jean-Raymond Abrial (1996):
The B-Book.
Cambridge University Press,
doi:10.1017/CBO9780511624162.
Jean-Raymond Abrial, Michael Butler & Stefan Hallerstede (2006):
An open extensible tool environment for Event-B.
In: Zhiming Liu & Jifeng He: Proceedings ICFEM'06,
LNCS 4260.
Springer-Verlag,
pp. 588–605,
doi:10.1007/s10009-010-0145-y.
Available at http://eprints.ecs.soton.ac.uk/12711/.
Frédéric Badeau & Marielle Doche-Petit (2012):
Formal Data Validation with Event-B.
CoRR abs/1210.7039.
Available at http://arxiv.org/abs/1210.7039.
Proceedings of DS-Event-B 2012, Kyoto.
CENELEC (2011):
Railway Applications – Communication, signalling and processing systems – Software for railway control and protection systems.
Technical Report EN50128.
European Standard.
ClearSy (2009):
Atelier B, User and Reference Manuals,
Aix-en-Provence, France.
Available at http://www.atelierb.eu/.
C. A. R. Hoare (2003):
The Verifying Compiler: A Grand Challenge for Computing Research.
J.ACM 50(1),
pp. 63–69,
doi:10.1145/602382.602403.
Thierry Lecomte, Lilian Burdy & Michael Leuschel (2012):
Formally Checking Large Data Sets in the Railways.
CoRR abs/1210.6815.
Available at http://arxiv.org/abs/1210.6815.
Proceedings of DS-Event-B 2012, Kyoto.
Michael Leuschel & Michael Butler (2003):
ProB: A Model Checker for B.
In: Keijiro Araki, Stefania Gnesi & Dino Mandrioli: FME 2003: Formal Methods,
LNCS 2805.
Springer-Verlag,
pp. 855–874,
doi:10.1007/978-3-540-45236-2_46.
Michael Leuschel & Michael J. Butler (2008):
ProB: an automated analysis toolset for the B method.
STTT 10(2),
pp. 185–203.
Available at http://dx.doi.org/10.1007/s10009-007-0063-9.
Michael Leuschel, Jérôme Falampin, Fabian Fritz & Daniel Plagge (2009):
Automated Property Verification for Large Scale B Models.
In: A. Cavalcanti & D. Dams: Proceedings FM 2009,
LNCS 5850.
Springer-Verlag,
pp. 708–723,
doi:10.1007/978-3-642-05089-3_45.
Michael Leuschel, Jérôme Falampin, Fabian Fritz & Daniel Plagge (2011):
Automated property verification for large scale B models with ProB.
Formal Asp. Comput. 23(6),
pp. 683–709.
Available at http://dx.doi.org/10.1007/s00165-010-0172-1.
Daniel Plagge & Michael Leuschel (2010):
Seven at a stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more.
STTT 11,
pp. 9–21,
doi:10.1007/s10009-009-0132-3.
Thierry Servat (2007):
BRAMA: A New Graphic Animation Tool for B models.
In: Jacques Julliand & Olga Kouchnarenko: Proceedings B'2007,
LNCS 4355.
Springer-Verlag,
pp. 274–276,
doi:10.1007/11955757_28.
Faqing Yang, Jean-Pierre Jacquot & Jeanine Souquières (2012):
The Case for Using Simulation to Validate Event-B Specifications.
In: Karl R. P. H. Leung & Pornsiri Muenchaisri: APSEC.
IEEE,
pp. 85–90.
Available at http://dx.doi.org/10.1109/APSEC.2012.66.