References

1. Jean-Raymond Abrial (1996): The B-Book. Cambridge University Press, doi:10.1017/CBO9780511624162.
2. 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/.
3. 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.
4. CENELEC (2011): Railway Applications – Communication, signalling and processing systems – Software for railway control and protection systems. Technical Report EN50128. European Standard.
5. ClearSy (2009): Atelier B, User and Reference Manuals, Aix-en-Provence, France. Available at http://www.atelierb.eu/.
6. 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.
7. 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.
8. 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.
9. 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.
10. 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.
11. 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.
12. 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.
13. 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.
14. Jean-Baptiste Tristan & Xavier Leroy (2008): Formal verification of translation validators: A case study on instruction scheduling optimizations. In: 35th symposium Principles of Programming Languages. ACM Press, pp. 17–27, doi:10.1007/s10817-008-9099-0. Available at http://gallium.inria.fr/~xleroy/publi/validation-scheduling.pdf.
15. 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.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org