{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,16]],"date-time":"2026-10-16T20:23:15Z","timestamp":1792182195489,"version":"4.4.0"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031197611","type":"print"},{"value":"9783031197628","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-19762-8_21","type":"book-chapter","created":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T08:03:09Z","timestamp":1666166589000},"page":"269-285","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Future Train Control Systems: Challenges for\u00a0Dependability Assessment"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4648-4667","authenticated-orcid":false,"given":"Alessandro","family":"Fantechi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0139-0421","authenticated-orcid":false,"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8482-2612","authenticated-orcid":false,"given":"Gloria","family":"Gori","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,10,17]]},"reference":[{"key":"21_CR1","doi-asserted-by":"publisher","unstructured":"Amendola, A., et al.: Formal design and validation of an automatic train operation control system. In: Dutilleul, S.C., Haxthausen, A.E., Lecomte, T. (eds.) Proceedings of RSSRail 2022. LNCS, vol. 13294, pp. 169\u2013178 (2022). https:\/\/doi.org\/10.1007\/978-3-031-05814-1_12","DOI":"10.1007\/978-3-031-05814-1_12"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Aslansefat, K., Kabir, S., Gheraibia, Y., Papadopoulos, Y.: Dynamic fault tree analysis: state-of-the-art in modelling, analysis and tools, pp. 73\u2013112, June 2020","DOI":"10.1201\/9780429268922-4"},{"key":"21_CR3","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. Transfer 24, 351\u2013370 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-030-61362-4_21","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"D Basile","year":"2020","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.) ISoLA 2020. LNCS, vol. 12476, pp. 368\u2013384. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_21"},{"issue":"6","key":"21_CR5","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. Formal Aspect. Comput. 33(6), 957\u2013987 (2021)","journal-title":"Formal Aspect. Comput."},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Bause, F., Kritzinger, P.S.: Stochastic Petri Nets - An Introduction to the Theory, 2nd edn. (2002)","DOI":"10.1007\/978-3-322-86501-4"},{"key":"21_CR7","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. Part C 82, 314\u2013336 (2017)","journal-title":"Transp. Res. Part C"},{"issue":"5","key":"21_CR8","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/s10009-010-0156-8","volume":"12","author":"G Bucci","year":"2010","unstructured":"Bucci, G., Carnevali, L., Ridi, L., Vicario, E.: Oris: a tool for modeling, verification and evaluation of real-time systems. Int. J. Softw. Tools Technol. Transfer 12(5), 391\u2013403 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Bulychev, P., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B.: Rewrite-based statistical model checking of WMTL. In: Qadeer, S., Tasiran, S. (eds.) Runtime Verification, pp. 260\u2013275 (2013)","DOI":"10.1007\/978-3-642-35632-2_25"},{"issue":"1","key":"21_CR10","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/S0951-8320(01)00121-1","volume":"75","author":"M Cepin","year":"2002","unstructured":"Cepin, M., Mavko, B.: A dynamic fault tree. Reliab. Eng. Syst. Saf. 75(1), 83\u201391 (2002). https:\/\/doi.org\/10.1016\/S0951-8320(01)00121-1","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Clark, G., et al.: The M\u00f6bius modeling tool. In: Proceedings of 9th International Workshop on Petri Nets and Performance Models, pp. 241\u2013250 (2001)","DOI":"10.1109\/PNPM.2001.953373"},{"issue":"5","key":"21_CR12","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1109\/52.84218","volume":"8","author":"J Couvillion","year":"1991","unstructured":"Couvillion, J., et al.: Performability modeling with UltraSAN. IEEE Softw. 8(5), 69\u201380 (1991)","journal-title":"IEEE Softw."},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u0103ionis, M., Poulsen, D.B.: UPPAAL SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397\u2013415 (2015)","DOI":"10.1007\/s10009-014-0361-y"},{"issue":"6","key":"21_CR14","first-page":"2545","volume":"21","author":"C Di Meo","year":"2020","unstructured":"Di Meo, C., Di Vaio, M., Flammini, F., Nardone, R., Santini, S., Vittorini, V.: ERTMS\/ETCS virtual coupling: proof of concept and numerical analysis. IEEE Trans. ITS 21(6), 2545\u20132556 (2020)","journal-title":"IEEE Trans. ITS"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-18744-6_1","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"A Fantechi","year":"2019","unstructured":"Fantechi, A.: Connected or autonomous trains? In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2019. LNCS, vol. 11495, pp. 3\u201319. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-18744-6_1"},{"key":"21_CR16","doi-asserted-by":"publisher","unstructured":"Flammini, F., Donato, L.D., Fantechi, A., Vittorini, V.: A vision of intelligent train control. In: Dutilleul, S.C., Haxthausen, A.E., Lecomte, T. (eds.) Proceedings of RSSRail 2022. LNCS, vol. 13294, pp. 192\u2013208. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-05814-1_14","DOI":"10.1007\/978-3-031-05814-1_14"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Flammini, F., Marrone, S., Nardone, R., Petrillo, A., Santini, S., Vittorini, V.: Towards railway virtual coupling. In: International Transportation Electrification Conference (ITEC) (2018)","DOI":"10.1109\/ESARS-ITEC.2018.8607523"},{"issue":"6","key":"21_CR18","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. Formal Aspects Comput. 33(6), 989\u20131007 (2021). https:\/\/doi.org\/10.1007\/s00165-021-00560-5","journal-title":"Formal Aspects Comput."},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Gehlot, V., Nigro, C.: Colored petri net model of the session initiation protocol (SIP). In: IECON 2010\u201336th Annual Conference on IEEE Industrial Electronics Society, pp. 2150\u20132155 (2010)","DOI":"10.1109\/IECON.2010.5675312"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Genrich, H.J.: Predicate\/transition nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Petri Nets: Central Models and Their Properties, pp. 207\u2013247 (1987)","DOI":"10.1007\/978-3-540-47919-2_9"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Hendriks, M., et al.: UPPAAL 4.0. In: QEST 2006, pp. 125\u2013126 (2006)","DOI":"10.1109\/QEST.2006.59"},{"issue":"2","key":"21_CR22","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/j.ifacol.2021.06.049","volume":"54","author":"O Himrane","year":"2021","unstructured":"Himrane, O., Beugin, J., Ghazel, M.: Toward formal safety and performance evaluation of GNSS-based railway localisation function. IFAC-PapersOnLine 54(2), 159\u2013166 (2021)","journal-title":"IFAC-PapersOnLine"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Huang, J., Lv, J., Feng, Y., Luo, Z., Liu, H., Chai, M.: A novel method on probability evaluation of ZC handover scenario based on SMC. In: Qian, J., Liu, H., Cao, J., Zhou, D. (eds.) Robotics and Rehabilitation Intelligence, pp. 319\u2013333 (2020)","DOI":"10.1007\/978-981-33-4929-2_22"},{"key":"21_CR24","unstructured":"IEEE: Vehicular technology society, 1474.1 - standard for communications - based train control (CBTC) - performance and functional requirements (2004)"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Jensen, K.: Coloured petri nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Petri Nets: Central Models and Their Properties, pp. 248\u2013299 (1987)","DOI":"10.1007\/978-3-540-47919-2_10"},{"issue":"3","key":"21_CR26","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10009-007-0038-x","volume":"9","author":"K Jensen","year":"2007","unstructured":"Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transfer 9(3), 213\u2013254 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"21_CR27","doi-asserted-by":"publisher","unstructured":"Katoen, J.: The probabilistic model checking landscape. In: Grohe, M., Koskinen, E., Shankar, N. (eds.) Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2016, New York, NY, USA, 5\u20138 July 2016, pp. 31\u201345 (2016). https:\/\/doi.org\/10.1145\/2933575.2934574","DOI":"10.1145\/2933575.2934574"},{"issue":"11","key":"21_CR28","first-page":"4693","volume":"21","author":"J Liu","year":"2020","unstructured":"Liu, J., Zhang, Y., Han, J., He, J., Sun, J., Zhou, T.: Intelligent hazard-risk prediction model for train control systems. IEEE Trans. ITS 21(11), 4693\u20134704 (2020)","journal-title":"IEEE Trans. ITS"},{"issue":"6","key":"21_CR29","doi-asserted-by":"publisher","first-page":"1211","DOI":"10.1109\/TSE.2019.2917202","volume":"47","author":"M Paolieri","year":"2021","unstructured":"Paolieri, M., Biagi, M., Carnevali, L., Vicario, E.: The ORIS tool: quantitative evaluation of Non-Markovian systems. IEEE Trans. Softw. Eng. 47(6), 1211\u20131225 (2021)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"21_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(91)90203-E","volume":"80","author":"W Reisig","year":"1991","unstructured":"Reisig, W.: Petri nets and algebraic specifications. Theor. Comput. Sci. 80(1), 1\u201334 (1991). https:\/\/doi.org\/10.1016\/0304-3975(91)90203-E","journal-title":"Theor. Comput. Sci."},{"key":"21_CR31","doi-asserted-by":"crossref","unstructured":"Sanders, W., Obal, W., Qureshi, M., Widjanarko, F.: The UltraSAN modeling environment. Perform. Eval. 24(1), 89\u2013115 (1995). Performance Modeling Tools","DOI":"10.1016\/0166-5316(95)00012-M"},{"key":"21_CR32","unstructured":"Sanders, W., Meyer, J.: METASAN: a performability evaluation tool based on Stochastic Activity Networks, pp. 807\u2013816, December 1986"},{"key":"21_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-15651-9_1","volume-title":"Computer Safety, Reliability, and Security","author":"O Schulz","year":"2010","unstructured":"Schulz, O., Peleska, J.: Reliability analysis of safety-related communication architectures. In: Schoitsch, E. (ed.) SAFECOMP 2010. LNCS, vol. 6351, pp. 1\u201314. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15651-9_1"},{"key":"21_CR34","unstructured":"Shift2Rail Joint Undertaking: Multi-annual action plan, November 2015. http:\/\/ec.europa.eu\/research\/participants\/data\/ref\/h2020\/other\/wp\/jtis\/h2020-maap-shift2rail_en.pdf"},{"issue":"1","key":"21_CR35","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1186\/s13173-021-00105-x","volume":"27","author":"LD da Silva","year":"2021","unstructured":"da Silva, L.D., Lollini, P., Mongelli, D., Bondavalli, A., Mand\u00f2, G.: A stochastic modeling approach for traffic analysis of a tramway system with virtual tags and local positioning. J. Braz. Comput. Soc. 27(1), 2 (2021)","journal-title":"J. Braz. Comput. Soc."},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Song, H.: Development and analysis of a train-centric distance measurement system by means of Colored Petri Nets. Ph.D. thesis (2018)","DOI":"10.1016\/j.ress.2017.03.001"},{"key":"21_CR37","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1016\/j.ress.2017.03.001","volume":"164","author":"H Song","year":"2017","unstructured":"Song, H., Liu, J., Schnieder, E.: Validation, verification and evaluation of a train to train distance measurement system by means of Colored Petri Nets. Reliab. Eng. Syst. Saf. 164, 10\u201323 (2017)","journal-title":"Reliab. Eng. Syst. Saf."},{"issue":"2","key":"21_CR38","doi-asserted-by":"publisher","first-page":"236","DOI":"10.17531\/ein.2018.2.08","volume":"20","author":"H Song","year":"2018","unstructured":"Song, H., Schnieder, E.: Modeling of railway system maintenance and availability by means of colored Petri nets. EiN 20(2), 236\u2013243 (2018)","journal-title":"EiN"},{"key":"21_CR39","doi-asserted-by":"crossref","unstructured":"Song, H., Schnieder, E.: Availability and performance analysis of train-to-train data communication system. IEEE Trans. ITS 20(7), 2786\u20132795 (2019)","DOI":"10.1109\/TITS.2019.2914701"},{"key":"21_CR40","unstructured":"UIC: Virtually coupled trains. http:\/\/www.railway-energy.org\/static\/Virtually_coupled_trains_86.php. Accessed 24 Feb 2019"},{"issue":"2","key":"21_CR41","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/j.ifacol.2021.06.045","volume":"54","author":"S Verma","year":"2021","unstructured":"Verma, S., Ghazel, M., Berbineau, M.: Model-based dependability evaluation of a wireless communication system in a virtually coupled train set. IFAC-PapersOnLine 54(2), 179\u2013186 (2021)","journal-title":"IFAC-PapersOnLine"},{"key":"21_CR42","doi-asserted-by":"crossref","unstructured":"Wang, J.: Stochastic Timed Petri Nets and Stochastic Petri Nets, pp. 125\u2013153 (1998)","DOI":"10.1007\/978-1-4615-5537-7_5"},{"key":"21_CR43","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/s10009-022-00652-4","volume":"24","author":"N Weik","year":"2022","unstructured":"Weik, N., Volk, M., Katoen, J.P., Nie\u00dfen, N.: DFT modeling approach for operational risk assessment of railway infrastructure. Int. J. Softw. Tools Technol. Transfer 24, 331\u2013350 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"21_CR44","doi-asserted-by":"crossref","unstructured":"Yong, Z., Sirui, Z.: Typical train virtual coupling scenario modeling and analysis of train control system based on vehicle-vehicle communication. In: 2020 IEEE 6th ICCSSE, pp. 143\u2013148, July 2020","DOI":"10.1109\/ICCSSE50399.2020.9171984"},{"issue":"1","key":"21_CR45","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.jss.2003.12.039","volume":"77","author":"A Zimmermann","year":"2005","unstructured":"Zimmermann, A., Hommel, G.: Towards modeling and evaluation of ETCS real-time communication and operation. J. Syst. Softw. 77(1), 47\u201354 (2005)","journal-title":"J. Syst. Softw."},{"key":"21_CR46","unstructured":"Zimmermann, A., Knoke, M., Huck, A., Hommel, G.: Towards version 4.0 of TimeNET, pp. 1\u20134, April 2006"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Practice"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-19762-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,6]],"date-time":"2024-10-06T02:43:22Z","timestamp":1728182602000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-19762-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031197611","9783031197628"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-19762-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"17 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}