{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T03:04:58Z","timestamp":1770347098372,"version":"3.49.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2011,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            In this paper we describe the successful application of the\n            <jats:sc>ProB<\/jats:sc>\n            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\n            <jats:sc>ProB<\/jats:sc>\n            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\u00e9tro. Here again, about a man month of effort has been replaced by a few minutes of computation. This achievement required the extension of the\n            <jats:sc>ProB<\/jats:sc>\n            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\n            <jats:sc>ProB<\/jats:sc>\n            , so that it can be integrated into the SIL4 development chain at Siemens.\n          <\/jats:p>","DOI":"10.1007\/s00165-010-0172-1","type":"journal-article","created":{"date-parts":[[2011,1,13]],"date-time":"2011-01-13T14:48:43Z","timestamp":1294930123000},"page":"683-709","source":"Crossref","is-referenced-by-count":46,"title":["Automated property verification for large scale B models with ProB"],"prefix":"10.1145","volume":"23","author":[{"given":"Michael","family":"Leuschel","sequence":"first","affiliation":[{"name":"Lehrstuhl Softwaretechnik und Programmiersprachen, Universit\u00e4t D\u00fcsseldorf, Universit\u00e4tsstr. 1, 40225, D\u00fcsseldorf, Germany"}]},{"given":"J\u00e9r\u00f4me","family":"Falampin","sequence":"additional","affiliation":[{"name":"Siemens Transportation Systems, BP 101, 150, avenue de la R\u00e9publique, 92323, Ch\u00e2tillon Cedex, France"}]},{"given":"Fabian","family":"Fritz","sequence":"additional","affiliation":[{"name":"Lehrstuhl Softwaretechnik und Programmiersprachen, Universit\u00e4t D\u00fcsseldorf, Universit\u00e4tsstr. 1, 40225, D\u00fcsseldorf, Germany"}]},{"given":"Daniel","family":"Plagge","sequence":"additional","affiliation":[{"name":"Lehrstuhl Softwaretechnik und Programmiersprachen, Universit\u00e4t D\u00fcsseldorf, Universit\u00e4tsstr. 1, 40225, D\u00fcsseldorf, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"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\u201902 105\u2013120 August 2002. Technical Report INRIA"},{"key":"e_1_2_1_2_2_2","first-page":"588","volume-title":"Proceedings ICFEM\u201906, LNCS 4260","author":"Abrial J-R","year":"2006"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/236705"},{"key":"e_1_2_1_2_4_2","volume-title":"Compilers. Principles, techniques, and tools","author":"Aho AV","year":"2007","edition":"2"},{"key":"e_1_2_1_2_5_2","first-page":"242","volume-title":"Proceedings ZB\u20192002, LNCS 2272","author":"Abrial J-R","year":"2002"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.5555\/599718"},{"key":"e_1_2_1_2_7_2","first-page":"334","volume-title":"Proceedings ZB\u20192005, LNCS 3455","author":"Badeau F","year":"2005"},{"key":"e_1_2_1_2_8_2","first-page":"369","volume-title":"World Congress on formal methods, LNCS 1708","author":"Behm P","year":"1999"},{"key":"e_1_2_1_2_9_2","first-page":"188","volume-title":"Tools and algorithms for the construction and analysis of systems, LNCS 2280","author":"Bouquet F","year":"2002"},{"key":"e_1_2_1_2_10_2","unstructured":"Boite O (2000) M\u00e9thode B et validation des invariants ferroviaires. Master\u2019s thesis Universit\u00e9 Denis Diderot 2000. M\u00e9moire de DEA de logique et fondements de l\u2019informatique"},{"issue":"8","key":"e_1_2_1_2_11_2","first-page":"1099","article-title":"Automatiser les preuves d\u2019un sous-langage de la m\u00e9thode B","volume":"21","author":"Boite O","year":"2002","journal-title":"Technique et Science Informatiques"},{"key":"e_1_2_1_2_12_2","unstructured":"Bofill M Palah\u00ed M Villaret M (2009) A system for CSP solving through satisfiability modulo theories. In IX Jornadas sobre Programaci\u00f3n y Lenguajes (PROLE\u201909). Donostia Spain pp 303\u2013312"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BFb0033845","volume-title":"Proc programming languages: implementations, logics, and programs, LNCS 1292","author":"Carlsson M","year":"1997"},{"key":"e_1_2_1_2_14_2","first-page":"81","volume-title":"Proceedings CAV\u201906, LNCS 4144","author":"Dutertre B","year":"2006"},{"issue":"1","key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","first-page":"11","DOI":"10.3166\/tsi.22.11-32","article-title":"B dans le tranport ferroviaire. L\u2019exp\u00e9rience de Siemens Transportation Systems","volume":"22","author":"Doll\u00e9 D","year":"2003","journal-title":"Technique et Science Informatiques"},{"key":"e_1_2_1_2_16_2","first-page":"678","volume-title":"Proceedings ICFEM\u201906, LNCS 4260","author":"Derrick J","year":"2006"},{"key":"e_1_2_1_2_17_2","first-page":"252","volume-title":"Proceedings B\u20192007, LNCS 4355","author":"Essam\u00e9 D","year":"2007"},{"issue":"1","key":"e_1_2_1_2_18_2","first-page":"71","article-title":"CoreASM: an extensible ASM execution engine","volume":"77","author":"Farahbod R","year":"2007","journal-title":"Fundam Inform"},{"key":"e_1_2_1_2_19_2","unstructured":"Fritz F (2008) An object oriented parser for B specifications. Bachelor\u2019s thesis Institut f\u00fcr Informatik Universit\u00e4t D\u00fcsseldorf"},{"key":"e_1_2_1_2_20_2","unstructured":"Gagnon E (1998) Sable CC an object-oriented compiler framework. Master\u2019s thesis McGill University Montreal Canada. Available at http:\/\/www.sablecc.org"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_2_1_2_22_2","volume-title":"Software abstractions: logic, language and analysis","author":"Jackson D","year":"2006"},{"key":"e_1_2_1_2_23_2","volume-title":"The art of computer programming, vol 3","author":"Knuth D","year":"1983"},{"key":"e_1_2_1_2_24_2","unstructured":"Krings S (2010) Code coverage analysis for Prolog. Bachelor\u2019s thesis Institut f\u00fcr Informatik Universit\u00e4t D\u00fcsseldorf"},{"key":"e_1_2_1_2_25_2","unstructured":"Lamport L (2002) Specifying systems the TLA+ language and tools for hardware and software engineers. Addison-Wesley"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: formal methods, LNCS 2805","author":"Leuschel M","year":"2003"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0063-9"},{"key":"e_1_2_1_2_28_2","first-page":"79","volume-title":"Proceedings B\u20192007, LNCS 4355, Besancon, France, 2007","author":"Leuschel M","year":"2007"},{"key":"e_1_2_1_2_29_2","first-page":"708","volume-title":"Proceedings FM 2009, LNCS 5850","author":"Leuschel M","year":"2009"},{"key":"e_1_2_1_2_30_2","unstructured":"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\u2019Information pages 73\u201384. C\u00e9padu\u00e8s-\u00c9ditions"},{"key":"e_1_2_1_2_31_2","first-page":"21","volume-title":"Proceedings FME\u201902, LNCS 2391","author":"Legeard B","year":"2002"},{"key":"e_1_2_1_2_32_2","unstructured":"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\u201332"},{"key":"e_1_2_1_2_33_2","unstructured":"Mariano G (1997) \u00c9valuation de Logiciels Critiques D\u00e9velopp\u00e9s par la M\u00e9thode B: Une Approche Quantitive. PhD thesis Universit\u00e9 de Valenciennes et Du Hainaut-Cambr\u00e9sis December 1997"},{"key":"e_1_2_1_2_34_2","unstructured":"M\u00e9tayer C (2010) AnimB 0.1.1. Available at http:\/\/wiki.event-b.org\/index.php\/AnimB"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_1_2_36_2","unstructured":"M\u00e9tayer C Voisin L (2009) The event-B mathematical language. Available at http:\/\/wiki.event-b.org\/index.php\/Event-B_Mathematical_Language"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Redmill F (2000) Safety integrity levels\u2014theory 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","DOI":"10.1007\/978-1-4471-0883-2_1"},{"key":"e_1_2_1_2_38_2","first-page":"274","volume-title":"Proceedings B\u20192007, LNCS 4355","author":"Servat T","year":"2007"},{"key":"e_1_2_1_2_39_2","unstructured":"Siemens (2009) B method\u2014optimum safety guaranteed. Imagine 10:12\u201313"},{"key":"e_1_2_1_2_40_2","unstructured":"Steria F (2009) Aix-en-Provence. Atelier B user and reference manuals 2009. Available at http:\/\/www.atelierb.eu\/"},{"key":"e_1_2_1_2_41_2","unstructured":"Tatibouet B (2001) The jbtools package. Available at http:\/\/lifc.univ-fcomte.fr\/PEOPLE\/tatibouet\/JBTOOLS\/BParser_en.html"},{"key":"e_1_2_1_2_42_2","first-page":"632","volume-title":"Proceedings TACAS\u201907, LNCS 4424","author":"Torlak E","year":"2007"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"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\u201334","DOI":"10.1109\/TASE.2007.50"},{"key":"e_1_2_1_2_44_2","first-page":"131","volume-title":"Proceedings PLDI\u201904","author":"Whaley J","year":"2004"},{"key":"e_1_2_1_2_45_2","first-page":"54","volume-title":"Proceedings CHARME\u201999, LNCS 1703","author":"Yu Y","year":"1999"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-010-0172-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:59:22Z","timestamp":1641484762000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-010-0172-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11]]},"references-count":45,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2011,11]]}},"alternative-id":["10.1007\/s00165-010-0172-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-010-0172-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,11]]}}}