{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T18:38:07Z","timestamp":1764873487040,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319572871"},{"type":"electronic","value":"9783319572888"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-57288-8_11","type":"book-chapter","created":{"date-parts":[[2017,4,8]],"date-time":"2017-04-08T06:45:05Z","timestamp":1491633905000},"page":"146-162","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations"],"prefix":"10.1007","author":[{"given":"Hugo Daniel","family":"Macedo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anne E.","family":"Haxthausen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,9]]},"reference":[{"key":"11_CR1","unstructured":"CENELEC European Committee for Electrotechnical Standardization. EN 50128:2011 - Railway applications - Communications, signalling and processing systems - Software for railway control and protection systems (2011)"},{"key":"11_CR2","unstructured":"European Railway Agency. ERTMS - System Requirements Specification - UNISIG SUBSET-026, April 2014. http:\/\/www.era.europa.eu\/Document-Register\/Pages\/Set-2-System-Requirements-Specification.aspx"},{"key":"11_CR3","first-page":"107","volume-title":"FORMS\/FORMAT 2010 - Formal Methods for Automation and Safety in Railway and Automotive Systems","author":"A Ferrari","year":"2010","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) FORMS\/FORMAT 2010 - Formal Methods for Automation and Safety in Railway and Automotive Systems, pp. 107\u2013115. Springer, Heidelberg (2010)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-25271-6_12","volume-title":"Formal Methods for Components and Objects","author":"H Hvid Hansen","year":"2011","unstructured":"Hvid Hansen, H., Ketema, J., Luttik, B., Mousavi, M.R., Pol, J., Santos, O.M.: Automated verification of executable UML models. In: Aichernig, B.K., Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 225\u2013250. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-25271-6_12"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-12566-9_8","volume-title":"Foundations of Computer Software. Future Trends and Techniques for Development","author":"AE Haxthausen","year":"2010","unstructured":"Haxthausen, A.E., Bliguet, M., Kj\u00e6r, A.A.: Modelling and verification of relay interlocking systems. In: Choppy, C., Sokolsky, O. (eds.) Monterey Workshop 2008. LNCS, vol. 6028, pp. 141\u2013153. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-12566-9_8"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-319-47169-3_19","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications","author":"AE Haxthausen","year":"2016","unstructured":"Haxthausen, A.E., \u00d8stergaard, P.H.: On the use of static checking in the verification of interlocking systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 266\u2013278. Springer, Cham (2016). doi: 10.1007\/978-3-319-47169-3_19"},{"issue":"2","key":"11_CR7","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s00165-009-0143-6","volume":"23","author":"AE Haxthausen","year":"2011","unstructured":"Haxthausen, A.E., Peleska, J., Kinder, S.: A formal approach for the construction and verification of railway control systems. Form. Asp. Comput. 23(2), 191\u2013219 (2011)","journal-title":"Form. Asp. Comput."},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-319-05032-4_16","volume-title":"Software Engineering and Formal Methods","author":"AE Haxthausen","year":"2014","unstructured":"Haxthausen, A.E., Peleska, J., Pinger, R.: Applied bounded model checking for interlocking system designs. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 205\u2013220. Springer, Cham (2014). doi: 10.1007\/978-3-319-05032-4_16"},{"issue":"6","key":"11_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., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Techniques for modelling and verifying railway interlockings. Int. J. Softw. Tools Technol. Transf. 16(6), 685\u2013711 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-319-33951-1_10","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"C Limbr\u00e9e","year":"2016","unstructured":"Limbr\u00e9e, C., Cappart, Q., Pecheur, C., Tonetta, S.: Verification of railway interlocking - compositional approach with OCRA. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 134\u2013149. Springer, Cham (2016). doi: 10.1007\/978-3-319-33951-1_10"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-319-47169-3_20","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications","author":"HD Macedo","year":"2016","unstructured":"Macedo, H.D., Fantechi, A., Haxthausen, A.E.: Compositional verification of multi-station interlocking systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 279\u2013293. Springer, Cham (2016). doi: 10.1007\/978-3-319-47169-3_20"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Peleska, J.: Industrial-strength model-based testing - state of the art and current challenges. In: Petrenko, A.K., Schlingloff, H. (eds.) 8th Workshop on Model-Based Testing, Rome, Italy, vol. 111, Electronic Proceedings in Theoretical Computer Science, pp. 3\u201328. Open Publishing Association (2013)","DOI":"10.4204\/EPTCS.111.1"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-20398-5_22","volume-title":"NASA Formal Methods","author":"J Peleska","year":"2011","unstructured":"Peleska, J., Vorobev, E., Lapschies, F.: Automated test case generation with SMT-solving and abstract interpretation. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 298\u2013312. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-20398-5_22"},{"key":"11_CR14","volume-title":"Railway Signalling & Interlocking: International Compendium","author":"G Theeg","year":"2009","unstructured":"Theeg, G., Vlasenko, S.V., Anders, E.: Railway Signalling & Interlocking: International Compendium. Eurailpress, Hamburg (2009)"},{"key":"11_CR15","unstructured":"Verified Systems International GmbH. RT-Tester Model-Based Test Case and Test Data Generator - RTT-MBT - User Manual (2013). http:\/\/www.verified.de"},{"key":"11_CR16","unstructured":"Vu, L.H., Haxthausen, A.E., Peleska, J.: A domain-specific language for railway interlocking systems. In: Schnieder, E., Tarnai, G. (eds.) FORMS\/FORMAT 2014\u201310th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems, pp. 200\u2013209. Institute for Traffic Safety and Automation Engineering, Technische Universit\u00e4t Braunschweig (2014)"},{"key":"11_CR17","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.) Formal Techniques for Safety-Critical Systems. Communications in Computer and Information Science, vol. 476, pp. 223\u2013238. Springer International Publishing, Cham (2015)"},{"key":"11_CR18","unstructured":"Vu, L.H.: Formal development and verification of railway control systems. In the context of ERTMS\/ETCS Level 2. Ph.D. thesis, Technical University of Denmark, DTU Compute (2015)"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.scico.2016.05.010","volume":"133","author":"V Linh Hong","year":"2017","unstructured":"Linh Hong, V., Haxthausen, A.E., Peleska, J.: Formal modelling and verification of interlocking systems featuring sequential release. Sci. Comput. Program. 133, 91\u2013115 (2017)","journal-title":"Sci. Comput. Program."},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Winter, K.: Symbolic model checking for interlocking systems. In: Flammini, F. (ed.) Railway Safety, Reliability, and Security: Technologies and Systems Engineering. IGI Global (2012)","DOI":"10.4018\/978-1-4666-1643-1.ch013"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57288-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,5]],"date-time":"2020-10-05T05:32:57Z","timestamp":1601875977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57288-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319572871","9783319572888"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57288-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"9 April 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Moffett Field","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 May 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ti.arc.nasa.gov\/events\/nfm-2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}