{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T18:36:46Z","timestamp":1764873406103,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319295091"},{"type":"electronic","value":"9783319295107"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29510-7_6","type":"book-chapter","created":{"date-parts":[[2016,1,29]],"date-time":"2016-01-29T09:39:16Z","timestamp":1454060356000},"page":"103-120","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Towards Safety Analysis of ERTMS\/ETCS Level 2 in Real-Time Maude"],"prefix":"10.1007","author":[{"given":"Phillip","family":"James","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Lawrence","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Roggenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Monika","family":"Seisenberger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,1,30]]},"reference":[{"key":"6_CR1","unstructured":"openETCS (2015). \n                    http:\/\/openetcs.org\n                    \n                  . Accessed 30 August 2015"},{"key":"6_CR2","unstructured":"Alcatel, Alstom, Ansaldo Signal, Bombardier, Invensys Rail and Siemens. System Requirements Specification, Chap. 2, Basic System Description (2006). SUBSET-026-2"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Chiappini, A., Cimatti, A., Macchi, L., Rebollo, O., Roveri, M., Susi, A., Tonetta, S., Vittorini, B.: Formalization and validation of a subset of the european train control system. In: Proceedings of ICSE 2010. ACM Press (2010)","DOI":"10.1145\/1810295.1810312"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-31424-7_29","volume-title":"Computer Aided Verification","author":"T Rizzo","year":"2012","unstructured":"Rizzo, T., Sanseviero, A., Roveri, M., Narasamdya, I., Tchaltsev, A., Lazzaro, A., Corvino, R., Cimatti, A.: Formal verification and validation of ERTMS industrial railway train spacing system. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 378\u2013393. Springer, Heidelberg (2012)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.L. (eds.): All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: WRLA 2002, vol. 71, ENTCS. Elsevier (2002)","DOI":"10.1016\/S1571-0661(05)82534-4"},{"key":"6_CR7","unstructured":"European Railway Industry. ERTMS (2015). \n                    http:\/\/www.era.europa.eu\/Core-Activities\/ERTMS\/Pages\/home.aspx\n                    \n                  . Accessed 30 August 2015"},{"key":"6_CR8","series-title":"NATO ASI Series","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"Verification of Digital and Hybrid Systems","author":"TA Henzinger","year":"2000","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series, vol. 170, pp. 265\u2013292. Springer, Heidelberg (2000)"},{"issue":"6","key":"6_CR9","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. STTT 16(6), 685\u2013711 (2014)","journal-title":"STTT"},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/j.scico.2014.04.005","volume":"96","author":"P James","year":"2014","unstructured":"James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S.A., Treharne, H.: On modelling and verifying railway interlockings: tracking train lengths. Sci. Comput. Program. 96, 315\u2013336 (2014)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"6_CR11","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/s11786-014-0174-0","volume":"8","author":"P James","year":"2014","unstructured":"James, P., Roggenbach, M.: Encapsulating formal methods within domainspecific languages: a solution for verifying railway scheme plans. Math. Comput. Sci. 8(1), 11\u201338 (2014)","journal-title":"Math. Comput. Sci."},{"key":"6_CR12","unstructured":"Lawrence, A., Berger, U., James, P., Roggenbach, M., Seisenberger, M.: Modelling and analysing the european rail traffic management system in Real-Time Maude. In: FTSCS 2014 - Preliminary Proceedings (2014)"},{"issue":"1\u20132","key":"6_CR13","first-page":"161","volume":"20","author":"J Meseguer","year":"2007","unstructured":"Meseguer, J., \u00d6lveczky, P.C.: Semantics and pragmatics of Real-Time Maude. Higher-Order Symbolic Comput. 20(1\u20132), 161\u2013196 (2007)","journal-title":"Higher-Order Symbolic Comput."},{"key":"6_CR14","series-title":"Communications in Computer and Information Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-319-17581-2_7","volume-title":"Formal Techniques for Safety-Critical Systems","author":"R Nardone","year":"2015","unstructured":"Nardone, R., Gentile, U., Peron, A., Benerecetti, M., Vittorini, V., Marrone, S., De Guglielmo, R., Mazzocca, N., Velardi, L.: Dynamic state machines for formalizing railway control system specifications. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2014. CCIS, vol. 476, pp. 93\u2013109. Springer, Heidelberg (2015)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Abstraction and completeness for Real-Time Maude. In: WRLA 2006, vol. 176, ENTCS (2007)","DOI":"10.1016\/j.entcs.2007.06.005"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-78800-3_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Meseguer","year":"2008","unstructured":"Meseguer, J., \u00d6lveczky, P.C.: The Real-Time Maude tool. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 332\u2013336. Springer, Heidelberg (2008)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-72952-5_8","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"S Thorvaldsen","year":"2007","unstructured":"Thorvaldsen, S., \u00d6lveczky, P.C.: Formal modeling and analysis of the OGDC wireless sensor network algorithm in Real-Time Maude. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 122\u2013140. Springer, Heidelberg (2007)"},{"key":"6_CR18","series-title":"Communications in Computer and Information Science","first-page":"223","volume-title":"Formal Techniques for Safety-Critical Systems","author":"LH Vu","year":"2015","unstructured":"Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modeling and verification of interlocking systems featuring sequential release. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2014. CCIS, vol. 476, pp. 223\u2013238. Springer, Heidelberg (2015)"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29510-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T08:18:16Z","timestamp":1559377096000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29510-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319295091","9783319295107"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29510-7_6","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"30 January 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}