{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T09:51:13Z","timestamp":1773827473637,"version":"3.50.1"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,11,6]],"date-time":"2019-11-06T00:00:00Z","timestamp":1572998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,11,6]],"date-time":"2019-11-06T00:00:00Z","timestamp":1572998400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2020,6]]},"DOI":"10.1007\/s10009-019-00539-x","type":"journal-article","created":{"date-parts":[[2019,11,6]],"date-time":"2019-11-06T13:03:30Z","timestamp":1573045410000},"page":"265-279","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Validation of the Hybrid ERTMS\/ETCS Level 3 using Spin"],"prefix":"10.1007","volume":"22","author":[{"given":"Paolo","family":"Arcaini","sequence":"first","affiliation":[]},{"given":"Jan","family":"Kofro\u0148","sequence":"additional","affiliation":[]},{"given":"Pavel","family":"Je\u017eek","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,6]]},"reference":[{"key":"539_CR1","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-91271-4_17","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"TS Hoang","year":"2018","unstructured":"Hoang, T.S., Butler, M., Reichl, K.: The Hybrid ERTMS\/ETCS Level 3 Case Study. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 251\u2013261. Springer, Cham (2018)"},{"key":"539_CR2","unstructured":"Hybrid ERTMS\/ETCS Level 3, version 1A. Technical report, EEIG ERTMS Users Group, 07 (2017)"},{"key":"539_CR3","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-540-87603-8_2","volume-title":"Abstract State Machines, B and Z: First International Conference, ABZ 2008, London, UK, September 16\u201318, 2008. Proceedings","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M.: The high road to formal validation. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) Abstract State Machines, B and Z: First International Conference, ABZ 2008, London, UK, September 16\u201318, 2008. Proceedings, pp. 4\u201323. Springer, Berlin (2008)"},{"key":"539_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-56641-1","volume-title":"Modeling Companion for Software Practitioners","author":"E B\u00f6rger","year":"2018","unstructured":"B\u00f6rger, E., Raschke, A.: Modeling Companion for Software Practitioners. Springer, Berlin (2018)"},{"key":"539_CR5","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":"539_CR6","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: AsmetaSMV: a way to link high-level ASM models to low-level NuSMV specifications. In: Proceedings of the 2nd International Conference on Abstract State Machines, Alloy, B and Z (ABZ 2010). LNCS, vol. 5977, pp. 61\u201374. Springer (2010)","DOI":"10.1007\/978-3-642-11811-1_6"},{"issue":"2","key":"539_CR7","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.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"539_CR8","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-540-24732-6_17","volume-title":"Model Checking Software","author":"J Chen","year":"2004","unstructured":"Chen, J., Cui, H.: Translation from adapted UML to Promela for CORBA-based applications. In: Graf, S., Mounier, L. (eds.) Model Checking Software, pp. 234\u2013251. Springer, Berlin (2004)"},{"key":"539_CR9","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/3-540-46017-9_8","volume-title":"Mod. Check. Softw.","author":"A Prigent","year":"2002","unstructured":"Prigent, A., Cassez, F., Dhaussy, P., Roux, O.: Extending the translation from SDL to Promela. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) Mod. Check. Softw., pp. 79\u201394. Springer, Berlin (2002)"},{"key":"539_CR10","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1007\/11901433_33","volume-title":"Formal Methods and Software Engineering","author":"B Meenakshi","year":"2006","unstructured":"Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating Simulink models into input language of a model checker. In: Liu, Z., He, J. (eds.) Formal Methods and Software Engineering, pp. 606\u2013620. Springer, Berlin (2006)"},{"key":"539_CR11","volume-title":"The SPIN Model Checker-Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker-Primer and Reference Manual. Addison-Wesley, Boston (2004)"},{"key":"539_CR12","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV version 2: an opensource tool for symbolic model checking. In: Proceedings International Conference on Computer-Aided Verification (CAV 2002). LNCS, vol. 2404. Springer (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"539_CR13","unstructured":"Git. \nhttps:\/\/git-scm.com\/\n\n. Accessed 30 May 2019"},{"key":"539_CR14","unstructured":"The Spin model checker website. \nhttp:\/\/spinroot.com\/\n\n. Accessed 30 May 2019"},{"key":"539_CR15","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"P Arcaini","year":"2018","unstructured":"Arcaini, P., Je\u017eek, P., Kofro\u0148, J.: Modelling the Hybrid ERTMS\/ETCS Level 3 Case Study in Spin. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z. Springer, Cham (2018)"},{"key":"539_CR16","unstructured":"Dr\u00e1\u017en\u00ed inspekce (The Rail Safety Inspection of the Czech Republic): Investigation Report of Railway Accident: Collision of a locomotive running solo as train No. 72461 with passenger train No. 5011 in Moravany station (2008). \nhttp:\/\/www.dicr.cz\/uploads\/Zpravy\/MU\/MU_Moravany.pdf\n\n. Accessed 30 May 2019"},{"key":"539_CR17","unstructured":"Das Eisenbahn-Bundesamt (EBA): The German Federal Railway Authority. Erweiterte Regelung zur Bedienung der Sandstreueinrichtung (2013). \nhttps:\/\/www.eba.bund.de\/SharedDocs\/Downloads\/DE\/GesetzeundRegelwerk\/Allgemeinverf\/34_allgvfg_sandstreu1.pdf?__blob=publicationFile&v=3\n\n. Accessed 30 May 2019"},{"key":"539_CR18","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-04570-7_17","volume-title":"Formal Methods for Industrial Critical Systems: 14th International Workshop, FMICS 2009, Eindhoven, The Netherlands, November 2\u20133, 2009.","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.) Formal Methods for Industrial Critical Systems: 14th International Workshop, FMICS 2009, Eindhoven, The Netherlands, November 2\u20133, 2009., pp. 202\u2013204. Springer, Berlin (2009)"},{"issue":"3","key":"539_CR19","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1002\/stvr.402","volume":"19","author":"G Fraser","year":"2009","unstructured":"Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey. Softw. Test. Verif. Reliab. 19(3), 215\u2013261 (2009)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"539_CR20","first-page":"7","volume-title":"Proceedings Tenth Workshop on Model Based Testing, London, UK, 18th April 2015, Volume 180 of Electronic Proceedings in Theoretical Computer Science","author":"AR Espada","year":"2015","unstructured":"Espada, A.R., del Mar Gallardo, M., Salmer\u00f3n, A., Merino, P.: Using model checking to generate test cases for android applications. In: Pakulin, N., Petrenko, A.K., Schlingloff, B.-H. (eds.) Proceedings Tenth Workshop on Model Based Testing, London, UK, 18th April 2015, Volume 180 of Electronic Proceedings in Theoretical Computer Science, pp. 7\u201321. Open Publishing Association, London (2015)"},{"key":"539_CR21","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1016\/j.scico.2016.09.002","volume":"133","author":"M Benerecetti","year":"2017","unstructured":"Benerecetti, M., De Guglielmo, R., Gentile, U., Marrone, S., Mazzocca, N., Nardone, R., Peron, A., Velardi, L., Vittorini, V.: Dynamic state machines for modelling railway control systems. Sci. Comput. Program. 133, 116\u2013153 (2017). Formal Techniques for Safety-Critical Systems (FTSCS 2014)","journal-title":"Sci. Comput. Program."},{"key":"539_CR22","unstructured":"Glossary of terms and abbreviations. Technical report, ERA * UNISIG * EEIG ERTMS USERS GROUP, 5 (2016)"},{"key":"539_CR23","unstructured":"Hybrid ERTMS\/ETCS Level 3, version 1C. Technical report, EEIG ERTMS Users Group, 07 (2018)"},{"key":"539_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-61073-3","volume-title":"Requirements Engineering","author":"J Dick","year":"2017","unstructured":"Dick, J., Hull, E., Jackson, K.: Requirements Engineering, 4th edn. Springer, Berlin (2017)","edition":"4"},{"key":"539_CR25","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-91271-4_21","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"A Cunha","year":"2018","unstructured":"Cunha, A., Macedo, N.: Validating the Hybrid ERTMS\/ETCS Level 3 concept with electrum. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 307\u2013321. Springer, Cham (2018)"},{"key":"539_CR26","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-319-91271-4_22","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"J-R Abrial","year":"2018","unstructured":"Abrial, J.-R.: The ABZ-2018 case study with Event-B. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 322\u2013337. Springer, Cham (2018)"},{"key":"539_CR27","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-319-91271-4_24","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"A Mammar","year":"2018","unstructured":"Mammar, A., Frappier, M., Fotso, S.J.T., Laleau, R.: An Event-B model of the hybrid ERTMS\/ETCS Level 3 standard. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 353\u2013366. Springer, Cham (2018)"},{"key":"539_CR28","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-319-91271-4_23","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Dghaym","year":"2018","unstructured":"Dghaym, D., Poppleton, M., Snook, C.: Diagram-led formal modelling using iUML-B for Hybrid ERTMS Level 3. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 338\u2013352. Springer, Cham (2018)"},{"key":"539_CR29","unstructured":"Leue, S., Holzmann, G.J.: v-Promela: a visual, object-oriented language for SPIN. In: Proceedings 2nd IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC\u201999) (Cat. No.99-61702), pp. 14\u201323 (1999)"},{"key":"539_CR30","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., Leuschel, M., Schneider, D., Krings, S., K\u00f6rner, P., Naulin, T., Nayeri, N., Skowron, F.: 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.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 292\u2013306. Springer, Cham (2018)"},{"key":"539_CR31","volume-title":"Models@run.time\u2014Foundations, Applications, and Roadmaps [Dagstuhl Seminar 11481, November 27\u2013December 2, 2011]. Lecture Notes in Computer Science","year":"2014","unstructured":"Bencomo, N., France, R.B., Cheng, B.H.C., A\u00dfmann, U. (eds.): Models@run.time\u2014Foundations, Applications, and Roadmaps [Dagstuhl Seminar 11481, November 27\u2013December 2, 2011]. Lecture Notes in Computer Science, vol. 8378. Springer, Cham (2014)"},{"key":"539_CR32","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-319-91271-4_18","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"SJT Fotso","year":"2018","unstructured":"Fotso, S.J.T., Frappier, M., Laleau, R., Mammar, A.: Modeling the hybrid ERTMS\/ETCS Level 3 standard using a formal requirements engineering approach. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 262\u2013276. Springer, Cham (2018)"},{"issue":"2","key":"539_CR33","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/s00766-004-0191-7","volume":"9","author":"A Fuxman","year":"2004","unstructured":"Fuxman, A., Liu, L., Mylopoulos, J., Pistore, M., Roveri, M., Traverso, P.: Specifying and analyzing early requirements in Tropos. Requir. Eng. 9(2), 132\u2013150 (2004)","journal-title":"Requir. Eng."},{"issue":"4","key":"539_CR34","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)","journal-title":"Form. Asp. Comput."},{"key":"539_CR35","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1007\/3-540-46419-0_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Gnesi","year":"2000","unstructured":"Gnesi, S., Latella, D., Lenzini, G., Abbaneo, C., Amendola, A.M., Marmo, P.: A formal specification and validation of a critical system in presence of byzantine errors. In: Graf, S., Schwartzbach, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 535\u2013549. Springer, Berlin (2000)"},{"key":"539_CR36","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L Lamport","year":"1982","unstructured":"Lamport, L., Shostak, R., Pease, M.: The byzantine generals problem. ACM Trans. Program. Lang. Syst. 4, 382\u2013401 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"539_CR37","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)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"539_CR38","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-540-68237-0_2","volume-title":"FM 2008: Formal Methods: 15th International Symposium on Formal Methods, Turku, Finland, May 26\u201330, 2008 Proceedings","author":"ND Arvind","year":"2008","unstructured":"Arvind, N.D., Katelman, M.: Getting formal verification into design flow. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008: Formal Methods: 15th International Symposium on Formal Methods, Turku, Finland, May 26\u201330, 2008 Proceedings, pp. 12\u201332. Springer, Berlin (2008)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00539-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00539-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00539-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,5]],"date-time":"2020-11-05T00:34:47Z","timestamp":1604536487000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00539-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,6]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["539"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00539-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11,6]]},"assertion":[{"value":"6 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}