{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T02:07:22Z","timestamp":1768356442354,"version":"3.49.0"},"publisher-location":"Cham","reference-count":92,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031637896","type":"print"},{"value":"9783031637902","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-63790-2_1","type":"book-chapter","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T14:03:41Z","timestamp":1718892221000},"page":"3-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Formal Methods and\u00a0Tools Applied in\u00a0the\u00a0Railway Domain"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice H.","family":"ter Beek","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,6,21]]},"reference":[{"key":"1_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":"1_CR2","unstructured":"Abrial, J.: Refinement, decomposition and instantiation of discrete models. In: Proceedings of the 12th International Workshop on Abstract State Machines (ASM 2005), pp. 17\u201340 (2005)"},{"key":"1_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J Abrial","year":"2010","unstructured":"Abrial, J.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010). https:\/\/doi.org\/10.1017\/CBO9781139195881"},{"issue":"3","key":"1_CR4","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."},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018). https:\/\/doi.org\/10.1145\/3158668","DOI":"10.1145\/3158668"},{"issue":"11","key":"1_CR6","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":"1_CR7","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."},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/11415787_20","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"F Badeau","year":"2005","unstructured":"Badeau, F., Amelot, A.: Using B as a high level programming language in an industrial project: Roissy VAL. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 334\u2013354. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11415787_20"},{"key":"1_CR9","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"6","key":"1_CR10","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1080\/10447310802205776","volume":"24","author":"A Bangor","year":"2008","unstructured":"Bangor, A., Kortum, P.T., Miller, J.T.: An empirical evaluation of the system usability scale. Int. J. Hum. Comput. Interact. 24(6), 574\u2013594 (2008). https:\/\/doi.org\/10.1080\/10447310802205776","journal-title":"Int. J. Hum. Comput. Interact."},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Bao, Y., Chen, M., Zhu, Q., Wei, T., Mallet, F., Zhou, T.: Quantitative performance evaluation of uncertainty-aware hybrid AADL designs using statistical model checking. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 36(12), 1989\u20132002 (2017). https:\/\/doi.org\/10.1109\/TCAD.2017.2681076","DOI":"10.1109\/TCAD.2017.2681076"},{"key":"1_CR12","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":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-030-03421-4_24","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"D Basile","year":"2018","unstructured":"Basile, D., ter Beek, M.H., Ciancia, V.: Statistical model checking of a moving block railway signalling scenario with Uppaal SMC. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 372\u2013391. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_24"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Basile, D., ter Beek, M.H., Di Giandomenico, F., Fantechi, A., Gnesi, S., Spagnolo, G.O.: 30 years of simulation-based quantitative analysis tools: a comparison experiment between M\u00f6bius and Uppaal SMC. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles. ISoLA 2020. LNCS, vol. 12476, pp. 368\u2013384. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_21","DOI":"10.1007\/978-3-030-61362-4_21"},{"key":"1_CR15","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":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-030-27008-7_1","volume-title":"Formal Methods for Industrial Critical Systems","author":"D Basile","year":"2019","unstructured":"Basile, D., ter Beek, M.H., Ferrari, A., Legay, A.: Modelling and analysing ERTMS L3 moving block railway signalling with Simulink and Uppaal SMC. In: Larsen, K.G., Willemse, T. (eds.) FMICS 2019. LNCS, vol. 11687, pp. 1\u201321. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-27008-7_1"},{"issue":"3","key":"1_CR17","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":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-50086-3_1","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"D Basile","year":"2020","unstructured":"Basile, D., ter Beek, M.H., Legay, A.: Strategy synthesis for autonomous driving in a moving block railway system with Uppaal Stratego. In: Gotsman, A., Sokolova, A. (eds.) FORTE 2020. LNCS, vol. 12136, pp. 3\u201321. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50086-3_1"},{"issue":"2","key":"1_CR19","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.jrtpm.2016.03.003","volume":"6","author":"D Basile","year":"2016","unstructured":"Basile, D., Chiaradonna, S., Di Giandomenico, F., Gnesi, S.: A stochastic model-based approach to analyse reliable energy-saving rail road switch heating systems. J. Rail Transp. Plan. Manag. 6(2), 163\u2013181 (2016). https:\/\/doi.org\/10.1016\/j.jrtpm.2016.03.003","journal-title":"J. Rail Transp. Plan. Manag."},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Basile, D., Di Giandomenico, F., Gnesi, S.: Statistical model checking of an energy-saving cyber-physical system in the railway domain. In: Proceedings of the 32nd Symposium on Applied Computing (SAC 2017), pp. 1356\u20131363. ACM (2017). https:\/\/doi.org\/10.1145\/3019612.3019824","DOI":"10.1145\/3019612.3019824"},{"issue":"6","key":"1_CR21","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":"1_CR22","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., Bor\u00e4lv, A., Fantechi, A., Ferrari, A., Gnesi, S., L\u00f6fving, C., Mazzanti, F.: 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"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., et al.: Formal methods in industry. Form. Asp. Comput. (2024)","DOI":"10.1145\/3689374"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Ciancia, V., Latella, D., Massink, M., Spagnolo, G.O.: Spatial model checking for smart stations: Research challenges. In: Lluch Lafuente, A., Mavridou, A. (eds.) Formal Methods for Industrial Critical Systems. FMICS 2021. LNCS, vol. 12863, pp. 39\u201347. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85248-1_3","DOI":"10.1007\/978-3-030-85248-1_3"},{"key":"1_CR25","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":"1_CR26","doi-asserted-by":"publisher","unstructured":"Behrmann, G., et al.: UPPAAL\u00a04.0. In: Proceedings of the 3rd International Conference on the Quantitative Evaluation of SysTems (QEST 2006), pp. 125\u2013126. IEEE (2006). https:\/\/doi.org\/10.1109\/QEST.2006.59","DOI":"10.1109\/QEST.2006.59"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-030-17462-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Belmonte","year":"2019","unstructured":"Belmonte, G., Ciancia, V., Latella, D., Massink, M.: VoxLogicA: a spatial model checker for declarative image analysis. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 281\u2013298. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_16"},{"key":"1_CR28","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.scico.2017.10.011","volume":"154","author":"U Berger","year":"2018","unstructured":"Berger, U., James, P., Lawrence, A., Roggenbach, M., Seisenberger, M.: Verification of the European rail traffic management system in real-time Maude. Sci. Comput. Program. 154, 61\u201388 (2018). https:\/\/doi.org\/10.1016\/j.scico.2017.10.011","journal-title":"Sci. Comput. Program."},{"key":"1_CR29","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1016\/j.trc.2017.07.002","volume":"82","author":"M Biagi","year":"2017","unstructured":"Biagi, M., Carnevali, L., Paolieri, M., Vicario, E.: Performability evaluation of the ERTMS\/ETCS - level 3. Transp. Res. C-Emerg. 82, 314\u2013336 (2017). https:\/\/doi.org\/10.1016\/j.trc.2017.07.002","journal-title":"Transp. Res. C-Emerg."},{"key":"1_CR30","doi-asserted-by":"publisher","DOI":"10.1002\/9781119005056","volume-title":"CENELEC 50128 and IEC 62279 Standards","author":"JL Boulanger","year":"2015","unstructured":"Boulanger, J.L.: CENELEC 50128 and IEC 62279 Standards. Wiley, Hoboken (2015)"},{"key":"1_CR31","doi-asserted-by":"publisher","unstructured":"Brooke, J.: SUS: a \u2018quick and dirty\u2019 usability scale. In: Jordan, P.W., Thomas, B., Weerdmeester, B.A., McClelland, I.L. (eds.) Usability Evaluation in Industry, chap.\u00a021, pp. 189\u2013194. CRC press (1996). https:\/\/doi.org\/10.1201\/9781498710411","DOI":"10.1201\/9781498710411"},{"issue":"2","key":"1_CR32","doi-asserted-by":"publisher","first-page":"29","DOI":"10.5555\/2817912.2817913","volume":"8","author":"J Brooke","year":"2013","unstructured":"Brooke, J.: SUS: a retrospective. J. Usability Stud. 8(2), 29\u201340 (2013). https:\/\/doi.org\/10.5555\/2817912.2817913","journal-title":"J. Usability Stud."},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Broy, M., et al.: Does every computer scientist need to know formal methods? Form. Asp. Comput. (2024)","DOI":"10.1145\/3670795"},{"issue":"3","key":"1_CR34","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 the 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."},{"issue":"4","key":"1_CR35","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s40534-016-0119-1","volume":"24","author":"BT Celebi","year":"2016","unstructured":"Celebi, B.T., Kaymakci, O.T.: Verifying the accuracy of interlocking tables for railway signalling systems using abstract state machines. J. Mod. Transp. 24(4), 277\u2013283 (2016). https:\/\/doi.org\/10.1007\/s40534-016-0119-1","journal-title":"J. Mod. Transp."},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Chiappini, A., et al.: Formalization and validation of a subset of the European train control system. In: Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering (ICSE 2010), vol.\u00a02, pp. 109\u2013118. ACM (2010). https:\/\/doi.org\/10.1145\/1810295.1810312","DOI":"10.1145\/1810295.1810312"},{"key":"1_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-030-84629-9_2","volume-title":"Model Checking Software","author":"V Ciancia","year":"2021","unstructured":"Ciancia, V., Belmonte, G., Latella, D., Massink, M.: A hands-on introduction to spatial model checking using VoxLogicA. In: Laarman, A., Sokolova, A. (eds.) SPIN 2021. LNCS, vol. 12864, pp. 22\u201341. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-84629-9_2"},{"key":"1_CR38","doi-asserted-by":"publisher","unstructured":"Clark, G., et al.: The M\u00f6bius modeling tool. In: Proceedings of the 9th International Workshop on Petri Nets and Performance Models (PNPM 2001), pp. 241\u2013250. IEEE (2001). https:\/\/doi.org\/10.1109\/PNPM.2001.953373","DOI":"10.1109\/PNPM.2001.953373"},{"key":"1_CR39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8"},{"key":"1_CR40","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":"Reliability, 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.B. (eds.) RSSRail 2017. LNCS, vol. 10598, pp. 148\u2013159. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68499-4_10"},{"key":"1_CR41","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":"1_CR42","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":"1_CR43","volume-title":"Mastering Simulink","author":"JB Dabney","year":"2003","unstructured":"Dabney, J.B., Harman, T.L.: Mastering Simulink. Pearson, London (2003)"},{"key":"1_CR44","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.) Proceedings of the IFIP TC6\/WG6.1 5th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE 1992). IFIP Transactions, vol.\u00a0C-10, pp. 199\u2013213. North-Holland (1992)"},{"key":"1_CR45","doi-asserted-by":"publisher","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Miku\u010dionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206\u2013211. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16","DOI":"10.1007\/978-3-662-46681-0_16"},{"issue":"4","key":"1_CR46","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397\u2013415 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0361-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"1_CR47","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":"1_CR48","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":"1_CR49","doi-asserted-by":"crossref","unstructured":"Dongol, B., et al.: On formal methods thinking in computer science education. Form. Asp. Comput. (2024)","DOI":"10.1145\/3670419"},{"key":"1_CR50","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":"1_CR51","unstructured":"European Committee for Electrotechnical Standardization: CENELEC EN 50128\u2014Railway applications \u2013 Communication, signalling and processing systems \u2013 Software for railway control and protection systems (2011). https:\/\/standards.globalspec.com\/std\/1678027\/cenelec-en-50128"},{"key":"1_CR52","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":"1_CR53","doi-asserted-by":"publisher","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.) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2019. LNCS, vol. 11495, pp. 226\u2013241. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-18744-6_15","DOI":"10.1007\/978-3-030-18744-6_15"},{"issue":"7","key":"1_CR54","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., Grasso, D., Magnani, G., Fantechi, A., 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":"1_CR55","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."},{"key":"1_CR56","doi-asserted-by":"publisher","unstructured":"Ferrari, A., Mazzanti, F., Basile, D., ter Beek, M.H., Fantechi, A.: Comparing formal tools for system design: a judgment study. In: Proceedings of the 42nd ACM\/IEEE International Conference on Software Engineering (ICSE 2020), pp. 62\u201374. ACM (2020). https:\/\/doi.org\/10.1145\/3377811.3380373","DOI":"10.1145\/3377811.3380373"},{"issue":"9","key":"1_CR57","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S1474-6670(17)38144-2","volume":"33","author":"M Fukuda","year":"2000","unstructured":"Fukuda, M., Hirao, Y., Ogino, T.: VDM specification of an interlocking system and a simulator for its validation. IFAC Proc. 33(9), 187\u2013192 (2000). https:\/\/doi.org\/10.1016\/S1474-6670(17)38144-2. Proceedings of the 9th IFAC Symposium on Control in Transportation Systems (CTS 2000)","journal-title":"IFAC Proc."},{"key":"1_CR58","unstructured":"Furness, N., van Houten, H., Arenas, L., Bartholomeus, M.: ERTMS level\u00a03: the game-changer. IRSE News 232, 2\u20139 (2017). https:\/\/www.irse.nl\/resources\/170314-ERTMS-L3-The-gamechanger-from-IRSE-News-Issue-232.pdf"},{"key":"1_CR59","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/j.scico.2016.04.010","volume":"131","author":"A F\u00fcrst","year":"2016","unstructured":"F\u00fcrst, A., Hoang, T.S., Basin, D.A., Sato, N., Miyazaki, K.: Large-scale system development using abstract data types and refinement. Sci. Comput. Program. 131, 59\u201375 (2016). https:\/\/doi.org\/10.1016\/j.scico.2016.04.010","journal-title":"Sci. Comput. Program."},{"key":"1_CR60","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"},{"key":"1_CR61","doi-asserted-by":"crossref","unstructured":"Guiho, G., Hennebert, C.: SACEM software validation. In: Proceedings of the 12th International Conference on Software Engineering (ICSE 1990), pp. 186\u2013191. IEEE (1990)","DOI":"10.1109\/ICSE.1990.63621"},{"key":"1_CR62","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.jss.2016.09.027","volume":"122","author":"B Hamid","year":"2016","unstructured":"Hamid, B., P\u00e9rez, J.: Supporting pattern-based dependability engineering via model-driven development: approach, tool-support and empirical validation. J. Syst. Softw. 122, 239\u2013273 (2016). https:\/\/doi.org\/10.1016\/j.jss.2016.09.027","journal-title":"J. Syst. Softw."},{"issue":"3","key":"1_CR63","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":"1_CR64","doi-asserted-by":"publisher","unstructured":"Hierons, R.M., et al.: Using formal specifications to support testing. ACM Comput. Surv. 41(2), 9:1\u20139:76 (2009). https:\/\/doi.org\/10.1145\/1459352.1459354","DOI":"10.1145\/1459352.1459354"},{"key":"1_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-030-27008-7_6","volume-title":"Formal Methods for Industrial Critical Systems","author":"A Idani","year":"2019","unstructured":"Idani, A., Ledru, Y., Ait Wakrime, A., Ben\u00a0Ayed, R., Collart-Dutilleul, S.: Incremental development of a safety critical system combining formal methods and DSMLs. In: Larsen, K.G., Willemse, T. (eds.) FMICS 2019. LNCS, vol. 11687, pp. 93\u2013109. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-27008-7_6"},{"key":"1_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-030-31784-3_5","volume-title":"Automated Technology for Verification and Analysis","author":"M Jaeger","year":"2019","unstructured":"Jaeger, M., Jensen, P.G., Larsen, K.G., Legay, A., Sedwards, S., Taankvist, J.H.: Teaching Stratego to play ball: optimal synthesis for continuous space MDPs. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 81\u201397. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_5"},{"issue":"6","key":"1_CR67","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.A., 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":"1_CR68","unstructured":"Jifeng, H.: From CSP to hybrid systems. In: Roscoe, A.W. (ed.) A Classical Mind: Essays in Honour of C. A. R. Hoare. Prentice Hall International Series in Computer Science, pp. 171\u2013189. Prentice Hall (1994)"},{"key":"1_CR69","doi-asserted-by":"publisher","unstructured":"Jin, Y., Xie, G., Chen, P., Hei, X., Ji, W., Zhao, J.: High-speed train emergency brake modeling and online identification of time-varying parameters. Math. Probl. Eng. 2020 (2020). https:\/\/doi.org\/10.1155\/2020\/3872852","DOI":"10.1155\/2020\/3872852"},{"key":"1_CR70","doi-asserted-by":"publisher","unstructured":"Khan, S.A., Zafar, N.A.: Towards the formalization of railway interlocking system using Z-notations. In: Proceedings of the 2nd International Conference on Computer, Control and Communication (IC4 2009), pp.\u00a01\u20136. IEEE (2009). https:\/\/doi.org\/10.1109\/IC4.2009.4909202","DOI":"10.1109\/IC4.2009.4909202"},{"key":"1_CR71","unstructured":"Kitchenham, B.: Procedures for performing systematic reviews. Technical report TR\/SE-0401, Keele University (2004)"},{"issue":"3","key":"1_CR72","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1049\/cce:19970304","volume":"8","author":"B Kitchenham","year":"1997","unstructured":"Kitchenham, B., Linkman, S., Law, D.: DESMET: a methodology for evaluating software engineering methods and tools. Comput. Control. Eng. J. 8(3), 120\u2013126 (1997). https:\/\/doi.org\/10.1049\/cce:19970304","journal-title":"Comput. Control. Eng. J."},{"issue":"4","key":"1_CR73","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/1232743.1232745","volume":"50","author":"J Kramer","year":"2007","unstructured":"Kramer, J.: Is abstraction the key to computing? Commun. ACM 50(4), 36\u201342 (2007). https:\/\/doi.org\/10.1145\/1232743.1232745","journal-title":"Commun. ACM"},{"key":"1_CR74","doi-asserted-by":"publisher","unstructured":"Lano, K.: The B Language and Method: a Guide to Practical Formal Development. FACIT. Springer, London (1996). https:\/\/doi.org\/10.1007\/978-1-4471-1494-9","DOI":"10.1007\/978-1-4471-1494-9"},{"key":"1_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-319-91908-9_23","volume-title":"Computing and Software Science","author":"A Legay","year":"2019","unstructured":"Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical model checking. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 478\u2013504. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_23"},{"issue":"6","key":"1_CR76","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. Form. Asp. Comput. 23(6), 683\u2013709 (2011). https:\/\/doi.org\/10.1007\/s00165-010-0172-1","journal-title":"Form. Asp. Comput."},{"issue":"3","key":"1_CR77","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":"1_CR78","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":"3","key":"1_CR79","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-018-0488-3","volume":"20","author":"F Mazzanti","year":"2018","unstructured":"Mazzanti, F., Ferrari, A., Spagnolo, G.O.: Towards formal methods diversity in railways: an experience report with seven frameworks. Int. J. Softw. Tools Technol. Transf. 20(3), 263\u2013288 (2018). https:\/\/doi.org\/10.1007\/s10009-018-0488-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1_CR80","doi-asserted-by":"publisher","unstructured":"Newborn, M.: Automated Theorem Proving. Springer, Germany (2001). https:\/\/doi.org\/10.1007\/978-1-4613-0089-2","DOI":"10.1007\/978-1-4613-0089-2"},{"key":"1_CR81","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.infsof.2015.03.007","volume":"64","author":"K Petersen","year":"2015","unstructured":"Petersen, K., Vakkalanka, S., Kuzniarz, L.: Guidelines for conducting systematic mapping studies in software engineering: an update. Inf. Softw. Technol. 64, 1\u201318 (2015). https:\/\/doi.org\/10.1016\/j.infsof.2015.03.007","journal-title":"Inf. Softw. Technol."},{"key":"1_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41135-4_1","volume-title":"Tests and Proofs","author":"K Reichl","year":"2016","unstructured":"Reichl, K., Fischer, T., Tummeltshammer, P.: Using formal methods for verification and validation in railway. In: Aichernig, B.K.K., Furia, C.A.A. (eds.) TAP 2016. LNCS, vol. 9762, pp. 3\u201313. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41135-4_1"},{"key":"1_CR83","volume-title":"Handbook of Automated Reasoning","year":"2001","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier, Amsterdam (2001)"},{"key":"1_CR84","doi-asserted-by":"publisher","unstructured":"SAE International: Architecture Analysis & Design Language (AADL) (2022). https:\/\/doi.org\/10.4271\/AS5506D","DOI":"10.4271\/AS5506D"},{"issue":"2","key":"1_CR85","doi-asserted-by":"publisher","first-page":"233","DOI":"10.17730\/humo.56.2.x335923511444655","volume":"56","author":"R Scupin","year":"1997","unstructured":"Scupin, R.: The KJ method: a technique for analyzing data derived from Japanese ethnology. Hum. Organ. 56(2), 233\u2013237 (1997). https:\/\/doi.org\/10.17730\/humo.56.2.x335923511444655","journal-title":"Hum. Organ."},{"key":"1_CR86","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-031-19762-8_20","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Practice","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"},{"key":"1_CR87","doi-asserted-by":"publisher","unstructured":"Snook, C.F., Hoang, T.S., Dghaym, D., Fathabadi, A.S., Butler, M.J.: Domain-specific scenarios for refinement-based methods. J. Syst. Archit. 112 (2021). https:\/\/doi.org\/10.1016\/j.sysarc.2020.101833","DOI":"10.1016\/j.sysarc.2020.101833"},{"issue":"3","key":"1_CR88","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":"1_CR89","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-25423-4_25","volume-title":"Formal Methods and Software Engineering","author":"S Wang","year":"2015","unstructured":"Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 382\u2013399. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25423-4_25"},{"issue":"3","key":"1_CR90","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1109\/MITS.2018.2842230","volume":"10","author":"Y Wang","year":"2018","unstructured":"Wang, Y., Chen, L., Kirkwood, D., Fu, P., Lv, J., Roberts, C.: Hybrid online model-based testing for communication-based train control systems. IEEE Intell. Transp. Syst. Mag. 10(3), 35\u201347 (2018). https:\/\/doi.org\/10.1109\/MITS.2018.2842230","journal-title":"IEEE Intell. Transp. Syst. Mag."},{"issue":"1","key":"1_CR91","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s10270-016-0517-1","volume":"17","author":"D Wu","year":"2018","unstructured":"Wu, D., Schnieder, E.: Scenario-based system design with colored Petri nets: an application to train control systems. Softw. Syst. Model. 17(1), 295\u2013317 (2018). https:\/\/doi.org\/10.1007\/s10270-016-0517-1","journal-title":"Softw. Syst. Model."},{"key":"1_CR92","doi-asserted-by":"publisher","unstructured":"Zhan, B., et al.: Compositional verification of interacting systems using event monads. In: Andronick, J., de\u00a0Moura, L. (eds.) Proceedings of the 13th International Conference on Interactive Theorem Proving (ITP 2022). LIPIcs, vol.\u00a0237, pp. 33:1\u201333:21. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.33","DOI":"10.4230\/LIPIcs.ITP.2022.33"}],"updated-by":[{"DOI":"10.1007\/978-3-031-63790-2_31","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T00:00:00Z","timestamp":1725580800000}}],"container-title":["Lecture Notes in Computer Science","Rigorous State-Based Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63790-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,22]],"date-time":"2024-11-22T08:49:14Z","timestamp":1732265354000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63790-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031637896","9783031637902"],"references-count":92,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63790-2_1","relation":{"correction":[{"id-type":"doi","id":"10.1007\/978-3-031-63790-2_31","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]]},"assertion":[{"value":"21 June 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"6 September 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":"Competing Interests"}},{"value":"ABZ","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Rigorous State-Based Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bergamo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"abz2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/abz-conf.org\/site\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}