{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,19]],"date-time":"2026-09-19T15:48:41Z","timestamp":1789832921315,"version":"4.0.1"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319471686","type":"print"},{"value":"9783319471693","type":"electronic"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47169-3_20","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T17:56:23Z","timestamp":1475603783000},"page":"279-293","source":"Crossref","is-referenced-by-count":18,"title":["Compositional Verification of Multi-station Interlocking Systems"],"prefix":"10.1007","author":[{"given":"Hugo D.","family":"Macedo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anne E.","family":"Haxthausen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"20_CR1","unstructured":"CENELEC European Committee for Electrotechnical Standardization: EN 50128:2011 \u2013 Railway applications \u2013 Communications, signalling and processing systems \u2013 Software for railway control and protection systems (2011)"},{"key":"20_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":"20_CR3","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14261-1_11","volume-title":"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, pp. 107\u2013115. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14261-1_11"},{"key":"20_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":"20_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":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/978-3-319-47169-3_19","volume-title":"ISoLA 2016, Part II","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, Part II. LNCS, vol. 9953, pp. 266\u2013278. Springer, Heidelberg (2016)"},{"key":"20_CR7","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, Heidelberg (2014). doi: 10.1007\/978-3-319-05032-4_16"},{"key":"20_CR8","unstructured":"James, P., M\u00f6ller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Decomposing scheme plans to manage verification complexity. In: Schnieder and Tarnai [14], pp. 210\u2013220"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-319-05032-4_15","volume-title":"Software Engineering and Formal Methods","author":"P James","year":"2014","unstructured":"James, P., M\u00f6ller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H., Trumble, M., Williams, D.: Verification of scheme plans using CSP $$||$$ | | B. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 189\u2013204. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-05032-4_15"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-319-05032-4_19","volume-title":"Software Engineering and Formal Methods","author":"P James","year":"2014","unstructured":"James, P., Lawrence, A., M\u00f6ller, F., Roggenbach, M., Seisenberger, M., Setzer, A., Kanso, K., Chadwick, S.: Verification of solid state interlocking programs. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 253\u2013268. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-05032-4_19"},{"key":"20_CR11","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, Heidelberg (2016). doi: 10.1007\/978-3-319-33951-1_10"},{"key":"20_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. Electronic Proceedings in Theoretical Computer Science, Rome, Italy, vol. 111, pp. 3\u201328. Open Publishing Association (2013)","DOI":"10.4204\/EPTCS.111.1"},{"key":"20_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":"20_CR14","unstructured":"Schnieder, E., Tarnai, G. (eds.) FORMS\/FORMAT 2014 - Formal Methods for Automation and Safety in Railway and Automotive Systems. Institute for Traffic Safety and Automation Engineering, Technische Universit\u00e4t Braunschweig (2014)"},{"key":"20_CR15","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, Germany (2009)"},{"key":"20_CR16","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":"20_CR17","unstructured":"Vu, L.H., Haxthausen, A.E., Peleska, J.: A domain-specific language for railway interlocking systems. In: Schnieder and Tarnai [14], pp. 200\u2013209"},{"key":"20_CR18","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-319-17581-2_15","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). doi: 10.1007\/978-3-319-17581-2_15"},{"key":"20_CR19","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":"20_CR20","doi-asserted-by":"crossref","unstructured":"Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modelling and verification of interlocking systems featuring sequential release. Science of Computer Programming (2016)","DOI":"10.1007\/978-3-319-17581-2_15"},{"key":"20_CR21","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"},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-34032-1_24","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies","author":"K Winter","year":"2012","unstructured":"Winter, K.: Optimising ordering strategies for symbolic model checking of railway interlockings. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7610, pp. 246\u2013260. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-34032-1_24"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47169-3_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T04:08:15Z","timestamp":1568434095000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47169-3_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471686","9783319471693"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47169-3_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}