{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T11:53:15Z","timestamp":1777636395153,"version":"3.51.4"},"publisher-location":"Cham","reference-count":63,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030582975","type":"print"},{"value":"9783030582982","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-58298-2_8","type":"book-chapter","created":{"date-parts":[[2020,8,28]],"date-time":"2020-08-28T18:04:52Z","timestamp":1598637892000},"page":"189-209","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":51,"title":["The First Twenty-Five Years of Industrial Use of the B-Method"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4642-5373","authenticated-orcid":false,"given":"Michael","family":"Butler","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7256-9560","authenticated-orcid":false,"given":"Philipp","family":"K\u00f6rner","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6712-9798","authenticated-orcid":false,"given":"Sebastian","family":"Krings","sequence":"additional","affiliation":[]},{"given":"Thierry","family":"Lecomte","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4595-1518","authenticated-orcid":false,"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]},{"given":"Luis-Fernando","family":"Mejia","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2426-0101","authenticated-orcid":false,"given":"Laurent","family":"Voisin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,8,29]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-319-05032-4_17","volume-title":"Software Engineering and Formal Methods","author":"R Abo","year":"2014","unstructured":"Abo, R., Voisin, L.: Formal implementation of data validation for railway safety-related systems with OVADO. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 221\u2013236. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-05032-4_17"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/3-540-50214-9_8","volume-title":"VDM \u201988 VDM \u2014 The Way Ahead","author":"JR Abrial","year":"1988","unstructured":"Abrial, J.R.: The B tool (abstract). In: Bloomfield, R.E., Marshall, L.S., Jones, R.B. (eds.) VDM 1988. LNCS, vol. 328, pp. 86\u201387. Springer, Heidelberg (1988). https:\/\/doi.org\/10.1007\/3-540-50214-9_8"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Extending B without changing it. In: Proceedings B, pp. 169\u2013190 (1996). ISBN 2-906082-25-2","DOI":"10.1093\/ilj\/25.3.169"},{"key":"8_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)"},{"issue":"5","key":"8_CR5","first-page":"619","volume":"13","author":"J-R Abrial","year":"2007","unstructured":"Abrial, J.-R.: Formal methods: theory becoming practice. J. Univ. Comput. Sci. 13(5), 619\u2013628 (2007)","journal-title":"J. Univ. Comput. Sci."},{"key":"8_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1007\/11901433_32","volume-title":"Formal Methods and Software Engineering","author":"J-R Abrial","year":"2006","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588\u2013605. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11901433_32"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/10930755_1","volume-title":"Theorem Proving in Higher Order Logics","author":"J-R Abrial","year":"2003","unstructured":"Abrial, J.-R., Cansell, D.: Click\u2019n prove: interactive proofs within set theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 1\u201324. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/10930755_1"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BFb0053357","volume-title":"B\u201998: Recent Advances in the Development and Use of the B Method","author":"J-R Abrial","year":"1998","unstructured":"Abrial, J.-R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83\u2013128. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0053357"},{"key":"8_CR10","unstructured":"Abrial, J.-R., Schuman, S., Meyer, B.: Specification language. In: On the Construction of Programs: An Advanced Course. Cambridge University Press (1980)"},{"key":"8_CR11","unstructured":"Ambert, F., et al.: BZ-testing-tools: a tool-set for test generation from Z and B using constraint logic programming. In: Proceedings FATES, pp. 105\u2013120 (2002). Technical report, INRIA"},{"key":"8_CR12","unstructured":"Badeau, F., Doche-Petit, M.: Formal data validation with Event-B. In: Proceedings of DS-Event-B 2012, Kyoto, CoRR, abs\/1210.7039 (2012)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-98938-9_2","volume-title":"Integrated Formal Methods","author":"D Basile","year":"2018","unstructured":"Basile, D., et al.: On the industrial uptake of formal methods in the railway domain. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 20\u201329. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98938-9_2"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Bendisposto, J., Krings, S., Leuschel, M.: Who watches the watchers: validating the ProB validation tool. In: Proceedings F-IDE, EPTCS, vol. 149 (2014)","DOI":"10.4204\/EPTCS.149.3"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11955757_2","volume-title":"B 2007: Formal Specification and Development in B","author":"E Jaffuel","year":"2006","unstructured":"Jaffuel, E.: Using B machines for model-based testing of smartcard software. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 2\u20132. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11955757_2"},{"key":"8_CR16","first-page":"3","volume":"280","author":"M Benveniste","year":"2011","unstructured":"Benveniste, M.: On using B in the design of secure micro-controllers: an experience report. ENTCS 280, 3\u201322 (2011)","journal-title":"ENTCS"},{"key":"8_CR17","unstructured":"Berglehner, R., Cherif, I., Rasheeq, A.: An approach to improve SysML railway specification using UML-B and EVENT-B. Poster presented at RSSRail 2019 (2019)"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"810","DOI":"10.1007\/978-3-642-05089-3_52","volume-title":"FM 2009: Formal Methods","author":"JC Bicarregui","year":"2009","unstructured":"Bicarregui, J.C., Fitzgerald, J.S., Larsen, P.G., Woodcock, J.C.P.: Industrial practice in formal methods: a review. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 810\u2013813. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-05089-3_52"},{"key":"8_CR19","unstructured":"Boite, O.: 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":"8_CR20","first-page":"1099","volume":"21","author":"O Boite","year":"2002","unstructured":"Boite, O.: Automatiser les preuves d\u2019un sous-langage de la m\u00e9thode B. Technique et Science Informatiques 21(8), 1099\u20131120 (2002)","journal-title":"Technique et Science Informatiques"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-46002-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Bouquet","year":"2002","unstructured":"Bouquet, F., Legeard, B., Peureux, F.: CLPS-B\u2014a constraint solver for B. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 188\u2013204. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_14"},{"key":"8_CR22","unstructured":"Burdy, L., Meynadier, J.-M.: Automatic refinement. In: Proceedings BUGM at FM 1999 (1999). https:\/\/www.clearsy.com\/wp-content\/uploads\/sites\/7\/dl\/lilian_burdy\/ug020003.pdf"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-00255-7_2","volume-title":"Integrated Formal Methods","author":"M Butler","year":"2009","unstructured":"Butler, M.: Decomposition structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 20\u201338. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00255-7_2"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Butler, M.J., et al.: Modelling and refinement in CODA. In: Proceedings Refine, EPTCS, vol. 115, pp. 36\u201351 (2013)","DOI":"10.4204\/EPTCS.115.3"},{"key":"8_CR25","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-319-68499-4_5","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"MJ Butler","year":"2017","unstructured":"Butler, M.J., et al.: formal modelling techniques for efficient development of railway control products. In: Fantechi, A., Lecomte, T., Romanovsky, A. (eds.) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. LNCS, vol. 10598, pp. 71\u201386. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68499-4_5"},{"key":"8_CR26","unstructured":"CENELEC: Railway Applications: Communications, Signalling and Processing Systems. Software for Railway Control and Protection Systems. EN50128: 2001 (2001)"},{"key":"8_CR27","unstructured":"ClearSy: Atelier B, User and Reference Manuals. Aix-en-Provence, France (2009). http:\/\/www.atelierb.eu\/"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-68499-4_10","volume-title":"RailReliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"M Comptier","year":"2017","unstructured":"Comptier, M., D\u00e9harbe, D., Perez, J.M., Mussat, L., Thibaut, P., Sabatier, D.: Safety analysis of a CBTC system: a rigorous approach with Event-B. In: Fantechi, A., Lecomte, T., Romanovsky, A. (eds.) RailReliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. LNCS, vol. 10598, pp. 148\u2013159. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68499-4_10"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-030-18744-6_13","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"M Comptier","year":"2019","unstructured":"Comptier, M., Leuschel, M., Mejia, L.-F., Perez, J.M., Mutz, M.: Property-based modelling and validation of a CBTC zone controller in Event-B. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2019. LNCS, vol. 11495, pp. 202\u2013212. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-18744-6_13"},{"issue":"3","key":"8_CR30","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/s10009-019-00548-w","volume":"22","author":"D Dghaym","year":"2020","unstructured":"Dghaym, D., Dalvandi, M., Poppleton, M., Snook, C.F.: Formalising the hybrid ERTMS Level 3 specification in iUML-B and Event-B. Int. J. Softw. Tools Technol. Transf. 22(3), 297\u2013313 (2020)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11955757_21","volume-title":"B 2007: Formal Specification and Development in B","author":"D Essam\u00e9","year":"2006","unstructured":"Essam\u00e9, D., Doll\u00e9, D.: B in large-scale projects: the Canarsie line CBTC experience. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 252\u2013254. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11955757_21"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/11955757_24","volume-title":"B 2007: Formal Specification and Development in B","author":"N Evans","year":"2006","unstructured":"Evans, N., Ifill, W.: Hardware verification and beyond: using B at AWE. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 260\u2013261. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11955757_24"},{"key":"8_CR33","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-642-33170-1_4","volume-title":"Industrial Deployment of System Engineering Methods","author":"J Falampin","year":"2013","unstructured":"Falampin, J., Le-Dang, H., Leuschel, M., Mokrani, M., Plagge, D.: Improving railway data validation with ProB. In: Romanovsky, A., Thomas, M. (eds.) Industrial Deployment of System Engineering Methods, pp. 27\u201343. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-33170-1_4"},{"key":"8_CR34","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-33170-1_10","volume-title":"Industrial Deployment of System Engineering Methods","author":"JS Fitzgerald","year":"2013","unstructured":"Fitzgerald, J.S., Bicarregui, J., Larsen, P.G., Woodcock, J.: Industrial deployment of formal methods: trends and challenges. In: Romanovsky, A., Thomas, M. (eds.) Industrial Deployment of System Engineering Methods, pp. 123\u2013143. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-33170-1_10"},{"key":"8_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-319-91271-4_20","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Hansen","year":"2018","unstructured":"Hansen, D., et al.: Using a formal B model at runtime in a demonstration of the ETCS hybrid level 3 concept with real trains. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 292\u2013306. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91271-4_20"},{"key":"8_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-319-33600-8_10","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Hansen","year":"2016","unstructured":"Hansen, D., Schneider, D., Leuschel, M.: Using B and ProB for data validation projects. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 167\u2013182. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_10"},{"key":"8_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-04570-7_17","volume-title":"Formal Methods for Industrial Critical Systems","author":"L Ladenberger","year":"2009","unstructured":"Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising Event-B models with B-motion studio. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 202\u2013204. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04570-7_17"},{"key":"8_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-319-41591-8_27","volume-title":"Software Engineering and Formal Methods","author":"L Ladenberger","year":"2016","unstructured":"Ladenberger, L., Leuschel, M.: BMotionWeb: a tool for rapid creation of formal prototypes. In: De Nicola, R., K\u00fchn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 403\u2013417. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41591-8_27"},{"key":"8_CR39","unstructured":"Lanet., J.-L.: The use of B for Smart Card. In: Proceedings FDL, vol. 2 (2002)"},{"key":"8_CR40","unstructured":"Lecomte, T.: The CLEARSY Safety Platform. https:\/\/www.clearsy.com\/en\/our-tools\/clearsy-safety-platform\/. Accessed 21 Jan 2020"},{"key":"8_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-04570-7_3","volume-title":"Formal Methods for Industrial Critical Systems","author":"T Lecomte","year":"2009","unstructured":"Lecomte, T.: Applying a formal method in industry: a 15-year trajectory. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 26\u201334. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04570-7_3"},{"key":"8_CR42","unstructured":"Lecomte, T.: Return of experience on automating refinement in B. In: Proceedings SETS (2014)"},{"key":"8_CR43","unstructured":"Lecomte, T.: Developing Safety Critical Applications. CLEARSY Systems Engineering (2019). Accessed 21 Jan 2020"},{"key":"8_CR44","unstructured":"Lecomte, T., Burdy, L., Leuschel, M.: Formally checking large data sets in the railways. In: Proceedings of DS-Event-B, CoRR, abs\/1210.6815 (2012)"},{"key":"8_CR45","unstructured":"Lecomte, T., Servat, T., Pouzancre, G., et al.: Formal methods in safety-critical railway systems. In: Proceedings SBMF, pp. 29\u201331 (2007)"},{"key":"8_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1007\/3-540-54834-3_53","volume-title":"VDM\u201991 Formal Software Development Methods","author":"M Lee","year":"1991","unstructured":"Lee, M., S\u00f8rensen, I.H.: B-tool. In: Prehn, S., Toetenel, W.J. (eds.) VDM 1991. LNCS, vol. 551, pp. 695\u2013696. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-54834-3_53"},{"key":"8_CR47","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge, D.: From animation to data validation: the ProB constraint solver 10 years on. In: Formal Methods Applied to Complex Systems: Implementation of the B Method, ISTE, chapter 14, pp. 427\u2013446. Wiley (2014)","DOI":"10.1002\/9781119002727.ch14"},{"issue":"2","key":"8_CR48","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185\u2013203 (2008)","journal-title":"STTT"},{"key":"8_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"708","DOI":"10.1007\/978-3-642-05089-3_45","volume-title":"FM 2009: Formal Methods","author":"M Leuschel","year":"2009","unstructured":"Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale B models. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 708\u2013723. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-05089-3_45"},{"issue":"6","key":"8_CR50","doi-asserted-by":"publisher","first-page":"683","DOI":"10.1007\/s00165-010-0172-1","volume":"23","author":"M Leuschel","year":"2011","unstructured":"Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale B models with ProB. Formal Asp. Comput. 23(6), 683\u2013709 (2011)","journal-title":"Formal Asp. Comput."},{"key":"8_CR51","doi-asserted-by":"crossref","unstructured":"Maamria , I., Butler, M.:. Rewriting and well-definedness within a proof system. In: Proceedings PAR, vol. 43. EPTCS (2010)","DOI":"10.4204\/EPTCS.43.4"},{"key":"8_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-642-11811-1_40","volume-title":"Abstract State Machines, Alloy, B and Z","author":"I Maamria","year":"2010","unstructured":"Maamria, I., Butler, M., Edmunds, A., Rezazadeh, A.: On an extensible rule-based prover for Event-B. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 407\u2013407. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11811-1_40"},{"issue":"12","key":"8_CR53","doi-asserted-by":"publisher","first-page":"2350","DOI":"10.1002\/spe.2634","volume":"48","author":"A Mashkoor","year":"2018","unstructured":"Mashkoor, A., Kossak, F., Egyed, A.: Evaluating the suitability of state-based formal methods for industrial deployment. Softw. Pract. Exp. 48(12), 2350\u20132379 (2018)","journal-title":"Softw. Pract. Exp."},{"key":"8_CR54","unstructured":"Metayer, C.: AnimB website. http:\/\/www.animb.org\/"},{"key":"8_CR55","unstructured":"Rasheeq, A.: An approach to improve SysML railway specification using UML-B and Event-B. Master\u2019s thesis, Frankfurt University of Applied Sciences (2019)"},{"key":"8_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/BFb0000503","volume-title":"Algebraic Methodology and Software Technology","author":"K Robinson","year":"1997","unstructured":"Robinson, K.: The B method and the B toolkit. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 576\u2013580. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0000503"},{"key":"8_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-33951-1_2","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"D Sabatier","year":"2016","unstructured":"Sabatier, D.: Using formal proof and B method at system level for industrial projects. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 20\u201331. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33951-1_2"},{"key":"8_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/11955757_28","volume-title":"B 2007: Formal Specification and Development in B","author":"T Servat","year":"2006","unstructured":"Servat, T.: BRAMA: a new graphic animation tool for B models. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 274\u2013276. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11955757_28"},{"key":"8_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-662-43652-3_1","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z Proceedings ABZ","author":"L Voisin","year":"2014","unstructured":"Voisin, L., Abrial, J.-R.: The Rodin Platform has turned ten. In: Ait Ameur, Y., Schewe, K.D. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z Proceedings ABZ. LNCS, vol. 8477, pp. 1\u20138. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_1"},{"issue":"2","key":"8_CR60","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/s10617-005-1184-6","volume":"9","author":"NS Voros","year":"2004","unstructured":"Voros, N.S., Snook, C.F., Hallerstede, S., Masselos, K.: Embedded system design using formal model refinement: an approach based on the combined use of UML and the B language. Design Autom. Embed. Syst. 9(2), 67\u201399 (2004)","journal-title":"Design Autom. Embed. Syst."},{"key":"8_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-030-48077-6_21","volume-title":"Rigorous State-Based Methods","author":"M Werth","year":"2020","unstructured":"Werth, M., Leuschel, M.: VisB: a lightweight tool to visualize formal models with SVG graphics. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 260\u2013265. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_21"},{"issue":"4","key":"8_CR62","doi-asserted-by":"publisher","first-page":"19:1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.S.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 19:1\u201319:36 (2009)","journal-title":"ACM Comput. Surv."},{"key":"8_CR63","doi-asserted-by":"crossref","unstructured":"Yang, F., Jacquot, J., Souqui\u00e8res, J.: JeB: safe simulation of Event-B models in JavaScript. In: Proceedings APSEC, vol. 1, pp. 571\u2013576. IEEE (2013)","DOI":"10.1109\/APSEC.2013.83"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-58298-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,12]],"date-time":"2024-08-12T19:58:24Z","timestamp":1723492704000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-58298-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030582975","9783030582982"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-58298-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"29 August 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Methods for Industrial Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vienna","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Austria","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fmics2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fmics20.ait.ac.at\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"42% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}