{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T09:51:09Z","timestamp":1773827469175,"version":"3.50.1"},"publisher-location":"Cham","reference-count":83,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031738869","type":"print"},{"value":"9783031738876","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T00:00:00Z","timestamp":1729641600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T00:00:00Z","timestamp":1729641600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-73887-6_21","type":"book-chapter","created":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T23:02:38Z","timestamp":1729638158000},"page":"327-344","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Formal Methods for\u00a0Industrial Critical Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice H.","family":"ter Beek","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4648-4667","authenticated-orcid":false,"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0139-0421","authenticated-orcid":false,"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,23]]},"reference":[{"issue":"3","key":"21_CR1","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/s10009-019-00525-3","volume":"22","author":"J Abrial","year":"2020","unstructured":"Abrial, J.: The ABZ-2018 case study with Event-B. Int. J. Softw. Tools Technol. Transf. 22(3), 257\u2013264 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00525-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"11","key":"21_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11432-015-5346-2","volume":"58","author":"E Ahmad","year":"2015","unstructured":"Ahmad, E., Dong, Y., Larson, B.R., L\u00fc, J., Tang, T., Zhan, N.: Behavior modeling and verification of movement authority scenario of Chinese train control system using AADL. Sci. China Inf. Sci. 58(11), 1\u201320 (2015). https:\/\/doi.org\/10.1007\/s11432-015-5346-2","journal-title":"Sci. China Inf. Sci."},{"issue":"3","key":"21_CR3","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/s10009-019-00539-x","volume":"22","author":"P Arcaini","year":"2020","unstructured":"Arcaini, P., Kofro\u0148, J., Je\u017eek, P.: Validation of the hybrid ERTMS\/ETCS level 3 using SPIN. Int. J. Softw. Tools Technol. Transf. 22(3), 265\u2013279 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00539-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"4","key":"21_CR4","first-page":"47","volume":"10","author":"AE Arenas","year":"2006","unstructured":"Arenas, A.E., Bicarregui, J., Margaria, T.: The FMICS view on the verified software repository. J. Integr. Des. Process. Sci. 10(4), 47\u201354 (2006)","journal-title":"J. Integr. Des. Process. Sci."},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-030-00244-2_7","volume-title":"Formal Methods for Industrial Critical Systems","author":"M Bartholomeus","year":"2018","unstructured":"Bartholomeus, M., Luttik, B., Willemse, T.: Modelling and analysing ERTMS hybrid level 3 with the mCRL2 toolset. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 98\u2013114. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00244-2_7"},{"key":"21_CR6","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"},{"issue":"3","key":"21_CR7","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/s10009-022-00653-3","volume":"24","author":"D Basile","year":"2022","unstructured":"Basile, D., ter Beek, M.H., Ferrari, A., Legay, A.: Exploring the ERTMS\/ETCS full moving block specification: an experience with formal methods. Int. J. Softw. Tools Technol. Transf. 24(3), 351\u2013370 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00653-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-030-85248-1_11","volume-title":"Formal Methods for Industrial Critical Systems","author":"D Basile","year":"2021","unstructured":"Basile, D., Fantechi, A., Rosadi, I.: Formal analysis of the UNISIG safety application intermediate sub-layer. In: Lluch Lafuente, A., Mavridou, A. (eds.) FMICS 2021. LNCS, vol. 12863, pp. 174\u2013190. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85248-1_11"},{"issue":"6","key":"21_CR9","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1007\/s00165-021-00556-1","volume":"33","author":"D Basile","year":"2021","unstructured":"Basile, D., Fantechi, A., Rucher, L., Mand\u00f2, G.: Analysing an autonomous tramway positioning system with the Uppaal statistical model checker. Form. Asp. Comput. 33(6), 957\u2013987 (2021). https:\/\/doi.org\/10.1007\/s00165-021-00556-1","journal-title":"Form. Asp. Comput."},{"key":"21_CR10","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-031-63790-2_1","volume-title":"ABZ 2024","author":"MH ter Beek","year":"2024","unstructured":"ter Beek, M.H.: Formal methods and tools applied in the railway domain. In: Bonfanti, S., Gargantini, A., Leuschel, M., Riccobene, E., Scandurra, P. (eds.) ABZ 2024. LNCS, vol. 14759, pp. 3\u201321. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63790-2_1"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"762","DOI":"10.1007\/978-3-030-30942-8_46","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"MH ter Beek","year":"2019","unstructured":"ter Beek, M.H., et al.: Adopting formal methods in an industrial setting: the railways case. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 762\u2013772. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_46"},{"issue":"4","key":"21_CR12","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/3702231","volume":"15","author":"M ter Beek","year":"2024","unstructured":"ter Beek, M., Broy, M., Dongol, B.: The role of formal methods in computer science education. ACM InRoads 15(4), 58\u201366 (2024). https:\/\/doi.org\/10.1145\/3702231","journal-title":"ACM InRoads"},{"issue":"1","key":"21_CR13","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/3689374","volume":"37","author":"MH ter Beek","year":"2025","unstructured":"ter Beek, M.H., et al.: Formal methods in industry. Form. Asp. Comput. 37(1), 7:1-7:38 (2025). https:\/\/doi.org\/10.1145\/3689374","journal-title":"Form. Asp. Comput."},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45943-1","volume-title":"Critical Systems: Formal Methods and Automated Verification","year":"2016","unstructured":"ter Beek, M.H., Gnesi, S., Knapp, A. (eds.): FMICS\/AVoCS 2016. LNCS, vol. 9933. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45943-1"},{"issue":"4","key":"21_CR15","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/s10009-018-0494-5","volume":"20","author":"MH ter Beek","year":"2018","unstructured":"ter Beek, M.H., Gnesi, S., Knapp, A.: Formal methods and automated verification of critical systems. Int. J. Softw. Tools Technol. Transf. 20(4), 355\u2013358 (2018). https:\/\/doi.org\/10.1007\/s10009-018-0494-5","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"21_CR16","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s10009-018-0487-4","volume":"20","author":"MH ter Beek","year":"2018","unstructured":"ter Beek, M.H., Gnesi, S., Knapp, A.: Formal methods for transport systems. Int. J. Softw. Tools Technol. Transf. 20(3), 237\u2013241 (2018). https:\/\/doi.org\/10.1007\/s10009-018-0487-4","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58298-2","volume-title":"Formal Methods for Industrial Critical Systems","year":"2020","unstructured":"ter Beek, M.H., Ni\u010dkovi\u0107, D. (eds.): FMICS 2020. LNCS, vol. 12327. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","volume-title":"FM\u201999 \u2014 Formal Methods","author":"P Behm","year":"1999","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: M\u00e9t\u00e9or: a successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369\u2013387. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48119-2_22"},{"key":"21_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-031-43681-9_2","volume-title":"FMICS 2023","author":"D Belli","year":"2023","unstructured":"Belli, D., et al.: The 4SECURail case study on rigorous standard interface specifications. In: Cimatti, A., Titolo, L. (eds.) FMICS 2023. LNCS, vol. 14290, pp. 22\u201339. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43681-9_2"},{"issue":"2","key":"21_CR20","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1023\/A:1008645826258","volume":"12","author":"C Bernardeschi","year":"1998","unstructured":"Bernardeschi, C., Fantechi, A., Gnesi, S., Larosa, S., Mongardi, G., Romano, D.: A formal verification environment for railway signaling system design. Form. Methods Syst. Des. 12(2), 139\u2013161 (1998). https:\/\/doi.org\/10.1023\/A:1008645826258","journal-title":"Form. Methods Syst. Des."},{"key":"21_CR21","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.scico.2016.04.004","volume":"128","author":"A Bonacchi","year":"2016","unstructured":"Bonacchi, A., Fantechi, A., Bacherini, S., Tempestini, M.: Validation process for railway interlocking systems. Sci. Comput. Program. 128, 2\u201321 (2016). https:\/\/doi.org\/10.1016\/j.scico.2016.04.004","journal-title":"Sci. Comput. Program."},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"653","DOI":"10.1007\/978-3-319-95582-7_39","volume-title":"Formal Methods","author":"A Bor\u00e4lv","year":"2018","unstructured":"Bor\u00e4lv, A.: Interlocking design automation using Prover Trident. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 653\u2013656. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_39"},{"key":"21_CR23","doi-asserted-by":"publisher","unstructured":"Broy, M., et al.: Does every computer scientist need to know formal methods? Form. Asp. Comput. (2024). https:\/\/doi.org\/10.1145\/36707","DOI":"10.1145\/36707"},{"issue":"3","key":"21_CR24","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10009-020-00562-3","volume":"22","author":"M Butler","year":"2020","unstructured":"Butler, M., Hoang, T.S., Raschke, A., Reichl, K.: Introduction to special section on the ABZ 2018 case study: hybrid ERTMS\/ETCS Level 3. Int. J. Softw. Tools Technol. Transf. 22(3), 249\u2013255 (2020). https:\/\/doi.org\/10.1007\/s10009-020-00562-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR25","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-030-71374-4_1","volume-title":"Formal Methods \u2013 Fun for Everybody","author":"A Cerone","year":"2021","unstructured":"Cerone, A., et al.: Rooting formal methods within higher education curricula for computer science and software engineering \u2014 a white paper \u2014. In: Cerone, A., Roggenbach, M. (eds.) FMFun 2019. CCIS, vol. 1301, pp. 1\u201326. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71374-4_1"},{"key":"21_CR26","doi-asserted-by":"publisher","unstructured":"Chiappini, A., et al.: Formalization and validation of a subset of the European Train Control System. In: ICSE 2010, pp. 109\u2013118. ACM (2010). https:\/\/doi.org\/10.1145\/1810295.1810312","DOI":"10.1145\/1810295.1810312"},{"issue":"4","key":"21_CR27","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/S001650050022","volume":"10","author":"A Cimatti","year":"1998","unstructured":"Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F., Traverso, P.: Formal verification of a railway interlocking system using model checking. Form. Asp. Comput. 10(4), 361\u2013380 (1998). https:\/\/doi.org\/10.1007\/S001650050022","journal-title":"Form. Asp. Comput."},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03240-0","volume-title":"Formal Methods for Industrial Critical Systems","year":"2009","unstructured":"Cofer, D., Fantechi, A. (eds.): FMICS 2008. LNCS, vol. 5596. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03240-0"},{"key":"21_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":"1","key":"21_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0167-6423(99)00014-3","volume":"36","author":"J Cu\u00e9llar","year":"2000","unstructured":"Cu\u00e9llar, J., Gnesi, S., Latella, D.: FMICS special issue. Sci. Comput. Program. 36(1), 1\u20133 (2000). https:\/\/doi.org\/10.1016\/S0167-6423(99)00014-3","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"21_CR31","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/s10009-019-00540-4","volume":"22","author":"A Cunha","year":"2020","unstructured":"Cunha, A., Macedo, N.: Validating the hybrid ERTMS\/ETCS level 3 concept with Electrum. Int. J. Softw. Tools Technol. Transf. 22(3), 281\u2013296 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00540-4","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR32","unstructured":"DaSilva, C., Dehbonei, B., Mejia, F.: Formal specification in the development of industrial applications: subway speed control system. In: Diaz, M., Groz, R. (eds.) FORTE 1992. IFIP, vol.\u00a0C-10, pp. 199\u2013213. North-Holland (1992)"},{"key":"21_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-642-41010-9_5","volume-title":"Formal Methods for Industrial Critical Systems","author":"JA Davis","year":"2013","unstructured":"Davis, J.A., et al.: Study on the barriers to the industrial adoption of formal methods. In: Pecheur, C., Dierkes, M. (eds.) FMICS 2013. LNCS, vol. 8187, pp. 63\u201377. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41010-9_5"},{"issue":"3","key":"21_CR34","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.: Formalising the hybrid ERTMS level 3 specification in iUML-B and Event-B. Int. J. Softw. Tools Technol. Transf. 22(3), 297\u2013313 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00548-w","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1","key":"21_CR35","doi-asserted-by":"publisher","first-page":"11","DOI":"10.3166\/tsi.22.11-32","volume":"22","author":"D Doll\u00e9","year":"2003","unstructured":"Doll\u00e9, D., Essam\u00e9, D., Falampin, J.: B dans le transport ferroviaire: L\u2019exp\u00e9rience de Siemens transportation systems. Tech. Sci. Inf. 22(1), 11\u201332 (2003). https:\/\/doi.org\/10.3166\/tsi.22.11-32","journal-title":"Tech. Sci. Inf."},{"key":"21_CR36","doi-asserted-by":"publisher","unstructured":"Dongol, B., et al.: On formal methods thinking in computer science education. Form. Asp. Comput. (2024). https:\/\/doi.org\/10.1145\/36704","DOI":"10.1145\/36704"},{"key":"21_CR37","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":"21_CR38","unstructured":"European Committee for Electrotechnical Standardization: CENELEC EN 50128: Railway applications\u00a0\u2013 Communication, signalling and processing systems\u00a0\u2013 Software for railway control and protection systems (2011). https:\/\/standards.globalspec.com\/std\/1678027\/cenelec-en-50128"},{"key":"21_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-319-05032-4_13","volume-title":"Software Engineering and Formal Methods","author":"A Fantechi","year":"2014","unstructured":"Fantechi, A.: Twenty-five years of formal methods and railways: what next? In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 167\u2013183. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-05032-4_13"},{"key":"21_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-47169-3_18","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications","author":"A Fantechi","year":"2016","unstructured":"Fantechi, A., Ferrari, A., Gnesi, S.: Formal methods and safety certification: challenges in the railways domain. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 261\u2013265. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47169-3_18"},{"key":"21_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-34032-1_19","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies","author":"A Fantechi","year":"2012","unstructured":"Fantechi, A., Flammini, F., Gnesi, S.: Formal methods for intelligent transportation systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7610, pp. 187\u2013189. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34032-1_19"},{"issue":"6","key":"21_CR42","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/s10009-014-0342-1","volume":"16","author":"A Fantechi","year":"2014","unstructured":"Fantechi, A., Flammini, F., Gnesi, S.: Formal methods for railway control systems. Int. J. Softw. Tools Technol. Transf. 16(6), 643\u2013646 (2014). https:\/\/doi.org\/10.1007\/s10009-014-0342-1","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-030-61467-6_24","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Applications","author":"A Fantechi","year":"2020","unstructured":"Fantechi, A., Gnesi, S., Haxthausen, A.E.: Formal methods for distributed computing in future railway systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12478, pp. 389\u2013392. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61467-6_24"},{"key":"21_CR44","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-031-19762-8_19","volume-title":"ISoLA 2022","author":"A Fantechi","year":"2022","unstructured":"Fantechi, A., Gnesi, S., Haxthausen, A.E.: Formal methods for distributed control systems of future railways. In: Margaria, T., Steffen, B. (eds.) ISoLA 2022. LNCS, vol. 13704, pp. 243\u2013245. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19762-8_19"},{"key":"21_CR45","volume-title":"ISoLA 2024","author":"A Fantechi","year":"2024","unstructured":"Fantechi, A., Gnesi, S., Haxthausen, A.E.: Formal methods for DIStributed COmputing in future RAILway systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024. Springer, LNCS (2024)"},{"key":"21_CR46","doi-asserted-by":"publisher","unstructured":"Ferrari, A., ter Beek, M.H.: Formal methods in railways: a systematic mapping study. ACM Comput. Surv. 55(4), 69:1\u201369:37 (2023). https:\/\/doi.org\/10.1145\/3520480","DOI":"10.1145\/3520480"},{"key":"21_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-030-18744-6_15","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"A Ferrari","year":"2019","unstructured":"Ferrari, A., et al.: Survey on formal methods and tools in railways: the ASTRail approach. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2019. LNCS, vol. 11495, pp. 226\u2013241. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-18744-6_15"},{"issue":"7","key":"21_CR48","doi-asserted-by":"publisher","first-page":"828","DOI":"10.1016\/j.scico.2012.04.003","volume":"78","author":"A Ferrari","year":"2013","unstructured":"Ferrari, A., Fantechi, A., Magnani, G., Grasso, D., Tempestini, M.: The Metr\u00f4 Rio case study. Sci. Comput. Program. 78(7), 828\u2013842 (2013). https:\/\/doi.org\/10.1016\/j.scico.2012.04.003","journal-title":"Sci. Comput. Program."},{"issue":"11","key":"21_CR49","doi-asserted-by":"publisher","first-page":"4675","DOI":"10.1109\/TSE.2021.3124677","volume":"48","author":"A Ferrari","year":"2022","unstructured":"Ferrari, A., Mazzanti, F., Basile, D., ter Beek, M.H.: Systematic evaluation and usability analysis of formal methods tools for railway signaling system design. IEEE Trans. Softw. Eng. 48(11), 4675\u20134691 (2022). https:\/\/doi.org\/10.1109\/TSE.2021.3124677","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"6","key":"21_CR50","doi-asserted-by":"publisher","first-page":"989","DOI":"10.1007\/S00165-021-00560-5","volume":"33","author":"F Flammini","year":"2021","unstructured":"Flammini, F., Marrone, S., Nardone, R., Vittorini, V.: Compositional modeling of railway virtual coupling with stochastic activity networks. Form. Asp. Comput. 33(6), 989\u20131007 (2021). https:\/\/doi.org\/10.1007\/S00165-021-00560-5","journal-title":"Form. Asp. Comput."},{"key":"21_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-58298-2_1","volume-title":"Formal Methods for Industrial Critical Systems","author":"H Garavel","year":"2020","unstructured":"Garavel, H., ter Beek, M.H., van de Pol, J.: The 2020 expert survey on formal methods. In: ter Beek, M.H., Ni\u010dkovi\u0107, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 3\u201369. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2_1"},{"issue":"3","key":"21_CR52","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1016\/S0167-6423(02)00091-6","volume":"46","author":"H Garavel","year":"2003","unstructured":"Garavel, H., Gnesi, S., Schieferdecker, I.: Special issue on FMICS 2000. Sci. Comput. Program. 46(3), 195\u2013196 (2003). https:\/\/doi.org\/10.1016\/S0167-6423(02)00091-6","journal-title":"Sci. Comput. Program."},{"issue":"10","key":"21_CR53","doi-asserted-by":"publisher","first-page":"2667","DOI":"10.1109\/TITS.2017.2657695","volume":"18","author":"M Ghazel","year":"2017","unstructured":"Ghazel, M.: A control scheme for automatic level crossings under the ERTMS\/ETCS level 2\/3 operation. IEEE Trans. Intell. Transp. Syst. 18(10), 2667\u20132680 (2017). https:\/\/doi.org\/10.1109\/TITS.2017.2657695","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"21_CR54","doi-asserted-by":"publisher","unstructured":"Gnesi, S., Latella, D.: Special issue on FMICS 1996. Form. Methods Syst. Des. 12(2), 123\u2013124 (1998). https:\/\/doi.org\/10.1023\/A:1008669025349","DOI":"10.1023\/A:1008669025349"},{"key":"21_CR55","doi-asserted-by":"publisher","unstructured":"Gnesi, S., Latella, D.: Special issue on FMICS 1997. Form. Asp. Comput. 10(4), 311\u2013312 (1998). https:\/\/doi.org\/10.1007\/s001650050019","DOI":"10.1007\/s001650050019"},{"key":"21_CR56","doi-asserted-by":"publisher","unstructured":"Gnesi, S., Latella, D.: Special issue on FMICS 1999. Form. Methods Syst. Des. 19(2), 119\u2013120 (2001). https:\/\/doi.org\/10.1023\/A:1011279615774","DOI":"10.1023\/A:1011279615774"},{"key":"21_CR57","doi-asserted-by":"publisher","unstructured":"Gnesi, S., Margaria, T.: Formal Methods for Industrial Critical Systems: A Survey of Applications. Wiley, Hoboken (2013). https:\/\/doi.org\/10.1002\/9781118459898","DOI":"10.1002\/9781118459898"},{"key":"21_CR58","doi-asserted-by":"publisher","unstructured":"Groote, J.F., van Vlijmen, S.F.M., Koorn, J.W.C.: The safety guaranteeing system at station Hoorn-Kersenboogerd. In: COMPASS 1995, pp. 57\u201368 (1995). https:\/\/doi.org\/10.1109\/CMPASS.1995.521887","DOI":"10.1109\/CMPASS.1995.521887"},{"key":"21_CR59","doi-asserted-by":"crossref","unstructured":"Guiho, G., Hennebert, C.: SACEM Software validation. In: ICSE 1990, pp. 186\u2013191. IEEE (1990)","DOI":"10.1109\/ICSE.1990.63621"},{"issue":"3","key":"21_CR60","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/s10009-020-00551-6","volume":"22","author":"D Hansen","year":"2020","unstructured":"Hansen, D., et al.: Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model. Int. J. Softw. Tools Technol. Transf. 22(3), 315\u2013332 (2020). https:\/\/doi.org\/10.1007\/s10009-020-00551-6","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR61","doi-asserted-by":"publisher","unstructured":"Haxthausen, A.E., Fantechi, A.: Compositional verification of railway interlocking systems. Form. Asp. Comput. 35(1), 4:1\u20134:46 (2023). https:\/\/doi.org\/10.1145\/3549736","DOI":"10.1145\/3549736"},{"key":"21_CR62","doi-asserted-by":"publisher","unstructured":"Himrane, O., Beugin, J., Ghazel, M.: Toward formal safety and performance evaluation of GNSS-based railway localisation function. IFAC-Pap. 54(2), 159\u2013166 (2021). https:\/\/doi.org\/10.1016\/j.ifacol.2021.06.049. Proceedings CTS 2021","DOI":"10.1016\/j.ifacol.2021.06.049"},{"key":"21_CR63","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1109\/OJITS.2023.3267142","volume":"4","author":"O Himrane","year":"2023","unstructured":"Himrane, O., Beugin, J., Ghazel, M.: Implementation of a model-oriented approach for supporting safe integration of GNSS-based virtual balises in ERTMS\/ETCS Level 3. IEEE Open J. Intell. Transp. Syst. 4, 294\u2013310 (2023). https:\/\/doi.org\/10.1109\/OJITS.2023.3267142","journal-title":"IEEE Open J. Intell. Transp. Syst."},{"key":"21_CR64","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.scico.2016.05.010","volume":"133","author":"LV Hong","year":"2017","unstructured":"Hong, L.V., Haxthausen, A.E., Peleska, J.: Formal modelling and verification of interlocking systems featuring sequential release. Sci. Comput. Program. 133, 91\u2013115 (2017). https:\/\/doi.org\/10.1016\/j.scico.2016.05.010","journal-title":"Sci. Comput. Program."},{"issue":"6","key":"21_CR65","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1007\/S10009-014-0304-7","volume":"16","author":"P James","year":"2014","unstructured":"James, P., Moller, F., Nga, N.H., Roggenbach, M., Schneider, S., Treharne, H.: Techniques for modelling and verifying railway interlockings. Int. J. Softw. Tools Technol. Transf. 16(6), 685\u2013711 (2014). https:\/\/doi.org\/10.1007\/S10009-014-0304-7","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR66","unstructured":"Kubczak, C., Margaria, T., Nagel, R., Steffen, B.: Plug and play with FMICS-jETI: beyond scripting and coding. ERCIM News 73, 41\u201342 (2008). http:\/\/ercim-news.ercim.eu\/plug-and-play-with-fmics-jeti-beyond-scripting-and-coding"},{"key":"21_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-540-68237-0_32","volume-title":"FM 2008: Formal Methods","author":"T Lecomte","year":"2008","unstructured":"Lecomte, T.: Safe and reliable metro platform screen doors control\/command systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 430\u2013434. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68237-0_32"},{"key":"21_CR68","doi-asserted-by":"publisher","unstructured":"Limbr\u00e9e, C., Pecheur, C.: A framework for the formal verification of networks of railway interlockings\u00a0- application to the Belgian railway. Electron. Commun. EASST 76 (2018). https:\/\/doi.org\/10.14279\/TUJ.ECEASST.76.1077","DOI":"10.14279\/TUJ.ECEASST.76.1077"},{"issue":"3","key":"21_CR69","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s10009-019-00543-1","volume":"22","author":"A Mammar","year":"2020","unstructured":"Mammar, A., Frappier, M., Tueno Fotso, S.J., Laleau, R.: A formal refinement-based analysis of the hybrid ERTMS\/ETCS level 3 standard. Int. J. Softw. Tools Technol. Transf. 22(3), 333\u2013347 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00543-1","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"10","key":"21_CR70","doi-asserted-by":"publisher","first-page":"2602","DOI":"10.1109\/TITS.2017.2658179","volume":"18","author":"J Marais","year":"2017","unstructured":"Marais, J., Beugin, J., Berbineau, M.: A survey of GNSS-based research and developments for the European railway signaling. IEEE Trans. Intell. Transp. Syst. 18(10), 2602\u20132618 (2017). https:\/\/doi.org\/10.1109\/TITS.2017.2658179","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"issue":"1","key":"21_CR71","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1109\/MITP.2020.2968715","volume":"22","author":"T Margaria","year":"2020","unstructured":"Margaria, T., Kiniry, J.: Welcome to formal methods in industry. IT Prof. 22(1), 9\u201312 (2020). https:\/\/doi.org\/10.1109\/MITP.2020.2968715","journal-title":"IT Prof."},{"key":"21_CR72","doi-asserted-by":"publisher","unstructured":"Margaria, T., Kubczak, C., Steffen, B., Naujokat, S.: The FMICS-jETI platform: status and perspectives. In: ISoLA 2006, pp. 402\u2013407. IEEE (2006). https:\/\/doi.org\/10.1109\/ISOLA.2006.50","DOI":"10.1109\/ISOLA.2006.50"},{"key":"21_CR73","doi-asserted-by":"publisher","unstructured":"Margaria, T., Massink, M.: FMICS 2005. ACM (2005). https:\/\/doi.org\/10.1145\/1081180","DOI":"10.1145\/1081180"},{"issue":"5","key":"21_CR74","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/S10009-009-0121-6","volume":"11","author":"T Margaria","year":"2009","unstructured":"Margaria, T., Massink, M.: Special section on FMICS 2005. Int. J. Softw. Tools Technol. Transf. 11(5), 355\u2013357 (2009). https:\/\/doi.org\/10.1007\/S10009-009-0121-6","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR75","doi-asserted-by":"publisher","unstructured":"Margaria, T., Raffelt, H., Steffen, B., Leucker, M.: The LearnLib in FMICS-jETI. In: ICECCS 2007, pp. 340\u2013352. IEEE (2007). https:\/\/doi.org\/10.1109\/ICECCS.2007.43","DOI":"10.1109\/ICECCS.2007.43"},{"key":"21_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-319-47169-3_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications","author":"F Mazzanti","year":"2016","unstructured":"Mazzanti, F., Ferrari, A., Spagnolo, G.O.: Experiments in formal modelling of a deadlock avoidance algorithm for a CBTC system. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 297\u2013314. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47169-3_22"},{"key":"21_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-319-10702-8_8","volume-title":"Formal Methods for Industrial Critical Systems","author":"F Mazzanti","year":"2014","unstructured":"Mazzanti, F., Spagnolo, G.O., Della Longa, S., Ferrari, A.: Deadlock avoidance in train scheduling: a model checking approach. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 109\u2013123. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10702-8_8"},{"issue":"6","key":"21_CR78","doi-asserted-by":"publisher","first-page":"2545","DOI":"10.1109\/TITS.2019.2920290","volume":"21","author":"CD Meo","year":"2020","unstructured":"Meo, C.D., Di Vaio, M., Flammini, F., Nardone, R., Santini, S., Vittorini, V.: ERTMS\/ETCS virtual coupling: proof of concept and numerical analysis. IEEE Trans. Intell. Transp. Syst. 21(6), 2545\u20132556 (2020). https:\/\/doi.org\/10.1109\/TITS.2019.2920290","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"21_CR79","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-031-60698-4_24","volume-title":"NFM 2024","author":"S Ramnath","year":"2024","unstructured":"Ramnath, S., Walk, S.: Structuring formal methods into the undergraduate computer science curriculum. In: Benz, N., Gopinath, D., Shi, N. (eds.) NFM 2024. LNCS, vol. 14627, pp. 399\u2013405. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-60698-4_24"},{"key":"21_CR80","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-031-19762-8_20","volume-title":"ISoLA 2022","author":"M Seisenberger","year":"2022","unstructured":"Seisenberger, M., et al.: Safe and secure future AI-driven railway technologies: challenges for formal methods in railway. In: Margaria, T., Steffen, B. (eds.) ISoLA 2022. LNCS, vol. 13704, pp. 246\u2013268. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19762-8_20"},{"issue":"3","key":"21_CR81","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/s10009-019-00542-2","volume":"22","author":"SJ Tueno Fotso","year":"2020","unstructured":"Tueno Fotso, S.J., Frappier, M., Laleau, R., Mammar, A.: Modeling the hybrid ERTMS\/ETCS level 3 standard using a formal requirements engineering approach. Int. J. Softw. Tools Technol. Transf. 22(3), 349\u2013363 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00542-2","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR82","unstructured":"The White House: Back to the Building Blocks: A Path Toward Secure and Measurable Software. Tech. rep., White House Office of the National Cyber Director (ONCD) (2024). https:\/\/www.whitehouse.gov\/wp-content\/uploads\/2024\/02\/Final-ONCD-Technical-Report.pdf"},{"key":"21_CR83","unstructured":"X2Rail-2\u00a0\u2013 Deliverable\u00a0D5.1, Formal Methods (Taxonomy and Survey), Proposed Methods and Applications (2018). https:\/\/projects.shift2rail.org\/download.aspx?id=b4cf6a3d-f1f2-4dd3-ae01-2bada34596b8"}],"updated-by":[{"DOI":"10.1007\/978-3-031-73887-6_24","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T00:00:00Z","timestamp":1729641600000}}],"container-title":["Lecture Notes in Computer Science","The Combined Power of Research, Education, and Dissemination"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-73887-6_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,30]],"date-time":"2025-01-30T11:15:24Z","timestamp":1738235724000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-73887-6_21"}},"subtitle":["30 Years of Railway Applications"],"short-title":[],"issued":{"date-parts":[[2024,10,23]]},"ISBN":["9783031738869","9783031738876"],"references-count":83,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-73887-6_21","relation":{"correction":[{"id-type":"doi","id":"10.1007\/978-3-031-73887-6_24","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,23]]},"assertion":[{"value":"23 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"23 October 2024","order":2,"name":"change_date","label":"Change Date","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Correction","order":3,"name":"change_type","label":"Change Type","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"A correction has been published.","order":4,"name":"change_details","label":"Change Details","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The author(s) has no competing interests to declare that are relevant to the content of this manuscript.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflicts of interest"}}]}}