Abstract
In this paper we describe the successful application of the ProB tool for data validation in several industrial applications. The initial case study centred on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for Atelier B. Atelier B, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense, and they need to be revalidated whenever the rail network infrastructure changes. In this paper we show how we were able to use ProB to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in a few minutes that were manually uncovered in about one man-month. We have repeated this task for three ongoing projects at Siemens, notably the ongoing automatisation of the line 1 of the Paris Métro. Here again, about a man month of effort has been replaced by a few minutes of computation. This achievement required the extension of the ProB kernel for large sets as well as an improved constraint propagation algorithm. We also outline some of the effort and features that were required in moving from a tool capable of dealing with medium-sized examples towards a tool able to deal with actual industrial specifications. We also describe the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Ambert F, Bouquet F, Chemin S, Guenaud S, Legeard B, Peureux F, Utting M, Vacelet N (2002) BZ-testing-tools: a tool-set for test generation from Z and B using constraint logic programming. In Proceedings of FATES’02, 105–120, August 2002. Technical Report, INRIA
Abrial J-R, Butler M, Hallerstede S (2006) An open extensible tool environment for Event-B. In: Liu Z, He J (eds) Proceedings ICFEM’06, LNCS 4260. Springer, Heidelberg, pp 588–605
Abrial J-R (1996) The B-book. Cambridge University Press, London
Aho AV, Lam MS, Sethi R, Ullman JD (2007) Compilers. Principles, techniques, and tools (2nd edn). Addison Wesley, Reading
Abrial J-R, Mussat L (2002) On using conditional definitions in formal theories. In: D. Bert, Bowen JP, Henson MC, Robinson K (eds) Proceedings ZB’2002, LNCS 2272. Springer, Heidelberg, pp 242–269
Appel AW (2002) Modern compiler implementation in Java (2nd edn). Cambridge University Press, London
Badeau F, Amelot A (2005) Using B as a high level programming language in an industrial project: Roissy VAL. In: Treharne H, King S, Henson M, Schneider S (eds) Proceedings ZB’2005, LNCS 3455. Springer, Berlin, pp 334–354
Behm P, Benoit P, Faivre A, Meynadier J-M (1999) Météor: a successful application of B in a large project. In: Wing JM, Woodcock J, Davies J (eds) World Congress on formal methods, LNCS 1708. Springer, Berlin, pp 369–387
Bouquet F, Legeard B, Peureux F (2002) CLPS-B—a constraint solver for B. In: Katoen J-P, Stevens P (eds) Tools and algorithms for the construction and analysis of systems, LNCS 2280. Springer, New York, pp 188–204
Boite O (2000) Méthode B et validation des invariants ferroviaires. Master’s thesis, Université Denis Diderot, 2000. Mémoire de DEA de logique et fondements de l’informatique
Boite O (2002) Automatiser les preuves d’un sous-langage de la méthode B. Technique et Science Informatiques 21(8): 1099–1120
Bofill M, Palahí M, Villaret M (2009) A system for CSP solving through satisfiability modulo theories. In IX Jornadas sobre Programación y Lenguajes (PROLE’09). Donostia, Spain, pp 303–312
Carlsson M, Ottosson G (1997) An open-ended finite domain constraint solver. In: Glaser HG, Hartel PH, Kuchen H (eds) Proc programming languages: implementations, logics, and programs, LNCS 1292. Springer, Berlin, pp 191–206
Dutertre B, de Moura L (2006) A fast linear-arithmetic solver for DPLL(T). In: Ball T, Jones RB (eds) Proceedings CAV’06, LNCS 4144. Springer, Berlin, pp 81–94
Dollé D, Essamé D, Falampin J (2003) B dans le tranport ferroviaire. L’expérience de Siemens Transportation Systems. Technique et Science Informatiques 22(1): 11–32
Derrick J, North S, Simons T (2006) Issues in implementing a model checker for Z. In: Liu Z, He J (eds) Proceedings ICFEM’06, LNCS 4260. Springer, Berlin, pp 678–696
Essamé D, Dollé D (2007) B in large-scale projects: the Canarsie line CBTC experience. In: Julliand J, Kouchnarenko O (eds) Proceedings B’2007, LNCS 4355. Springer, Berlin, pp 252–254
Farahbod R, Gervasi V, Glässer U (2007) CoreASM: an extensible ASM execution engine. Fundam Inform 77(1–2): 71–103
Fritz F (2008) An object oriented parser for B specifications. Bachelor’s thesis, Institut für Informatik, Universität Düsseldorf
Gagnon E (1998) Sable CC, an object-oriented compiler framework. Master’s thesis, McGill University, Montreal, Canada. Available at http://www.sablecc.org
Jackson D (2002) Alloy: a lightweight object modelling notation. ACM Trans Softw Eng Methodol 11: 256–290
Jackson D (2006) Software abstractions: logic, language and analysis. MIT Press, Cambridge
Knuth D (1983) The art of computer programming, vol 3. Addison-Wesley, Reading
Krings S (2010) Code coverage analysis for Prolog. Bachelor’s thesis, Institut für Informatik, Universität Düsseldorf
Lamport L (2002) Specifying systems, the TLA+ language and tools for hardware and software engineers. Addison-Wesley
Leuschel M, Butler M (2003) ProB: a model checker for B. In: Araki K, Gnesi S, Mandrioli D (eds) FME 2003: formal methods, LNCS 2805. Springer, Berlin, pp 855–874
Leuschel M, Butler MJ (2008) ProB: an automated analysis toolset for the B method. STTT 10(2): 185–203
Leuschel M, Butler M, Spermann C, Turner E (2007) Symmetry reduction for B by permutation flooding. In: Julliand J, Kouchnarenko O (eds) Proceedings B’2007, LNCS 4355, Besancon, France, 2007. Springer, Berlin, pp 79–93
Leuschel M, Falampin J, Fritz F, Plagge D (2009) Automated property verification for large scale B models. In: Cavalcanti A, Dams D (eds) Proceedings FM 2009, LNCS 5850. Springer, Berlin, pp 708–723
Leuschel M, Plagge D (2007) Seven at a stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. In: Ameur YA, Boniol F, Wiels V (eds) Proceedings Isola 2007, volume RNTI-SM-1 of Revue des Nouvelles Technologies de l’Information, pages 73–84. Cépaduès-Éditions
Legeard B, Peureux F, Mark Utting (2002) Automated boundary testing from Z and B. In: Eriksson L-H, Lindsay P (eds) Proceedings FME’02, LNCS 2391. Springer, Berlin, pp 21–40
Leuschel M, Samia M, Bendisposto J, Luo L (2008) Easy graphical animation and formula viewing for teaching B. The B method: from research to teaching, pp 17–32
Mariano G (1997) Évaluation de Logiciels Critiques Développés par la Méthode B: Une Approche Quantitive. PhD thesis, Université de Valenciennes et Du Hainaut-Cambrésis, December 1997
Métayer C (2010) AnimB 0.1.1. Available at http://wiki.event-b.org/index.php/AnimB
Milner R (1978) A theory of type polymorphism in programming. J Comput Syst Sci 17: 348–375
Métayer C, Voisin L (2009) The event-B mathematical language. Available at http://wiki.event-b.org/index.php/Event-B_Mathematical_Language
Redmill F (2000) Safety integrity levels—theory and problems. In: Lessons in system safety: proceedings of the eighth Safety-critical systems symposium, Southampton, UK. Available at http://www.csr.ncl.ac.uk/FELIX_Web/new_index.html
Servat T (2007) Brama: a new graphic animation tool for B models. In: Julliand J, Kouchnarenko O (eds) Proceedings B’2007, LNCS 4355. Springer, Berlin, pp 274–276
Siemens (2009) B method—optimum safety guaranteed. Imagine, 10:12–13
Steria F (2009) Aix-en-Provence. Atelier B, user and reference manuals, 2009. Available at http://www.atelierb.eu/
Tatibouet B (2001) The jbtools package. Available at http://lifc.univ-fcomte.fr/PEOPLE/tatibouet/JBTOOLS/BParser_en.html
Torlak E, Jackson D (2007) Kodkod: a relational model finder. In: Grumberg O, Huth M (eds) Proceedings TACAS’07, LNCS 4424. Springer, Berlin, pp 632–647
Turner E, Leuschel M, Spermann C, Butler M (2007) Symmetry reduced model checking for B. In: Proceedings TASE 2007, Shanghai, China, June 2007. IEEE, Washington, DC, pp 25–34
Whaley J, Lam MS (2004) Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In: Pugh W, Chambers C (eds) Proceedings PLDI’04. ACM Press, New York, pp 131–144
Yu Y, Manolios P, Lamport L (1999) Model checking TLA+ specifications. In: Pierre L, Kropf T (eds) Proceedings CHARME’99, LNCS 1703. Springer, Berlin, pp 54–66
Acknowledgments
First, we would like to thank the anonymous referees of FM’2009 and of Formal Aspects of Computing for their extensive and very thorough feedback, which helped us considerably to improve paper. We also would like to thank Jens Bendisposto and Sebastian Krings for assisting us in various ways in writing the paper. We are also grateful to Roozbeh Farahbod and Stefan Hallerstede for encoding the Sieve Algorithm in CoreASM and TLA+ for us. Finally, part of this research has been funded by the EU FP7 project 214158: DEPLOY (Industrial deployment of advanced system engineering methods for high productivity and dependability).
Open Access
This article is distributed under the terms of the Creative Commons Attribution Noncommercial License which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.
Author information
Authors and Affiliations
Corresponding author
Additional information
Ana Cavalcanti, Dennis Dams and Marie-Claude Gaudel
Rights and permissions
Open Access This is an open access article distributed under the terms of the Creative Commons Attribution Noncommercial License (https://creativecommons.org/licenses/by-nc/2.0), which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.
About this article
Cite this article
Leuschel, M., Falampin, J., Fritz, F. et al. Automated property verification for large scale B models with ProB. Form Asp Comp 23, 683–709 (2011). https://doi.org/10.1007/s00165-010-0172-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-010-0172-1