{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T18:38:12Z","timestamp":1764873492364,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661964"},{"type":"electronic","value":"9783319661971"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66197-1_15","type":"book-chapter","created":{"date-parts":[[2017,8,11]],"date-time":"2017-08-11T21:02:30Z","timestamp":1502485350000},"page":"236-252","source":"Crossref","is-referenced-by-count":13,"title":["Compositional Verification of Interlocking Systems for Large Stations"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Fantechi","sequence":"first","affiliation":[]},{"given":"Anne E.","family":"Haxthausen","sequence":"additional","affiliation":[]},{"given":"Hugo D.","family":"Macedo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,13]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.scico.2016.04.004","volume":"128","author":"A Bonacchi","year":"2016","unstructured":"Bonacchi, A., Fantechi, A., Bacherini, S., Tempestini, M.: Validation process for railway interlocking systems. Sci. Comput. Program. 128, 2\u201321 (2016)","journal-title":"Sci. Comput. Program."},{"key":"15_CR2","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":"15_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:\n10.1007\/978-3-642-14261-1_11"},{"key":"15_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:\n10.1007\/978-3-642-25271-6_12"},{"key":"15_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:\n10.1007\/978-3-642-12566-9_8"},{"issue":"2","key":"15_CR6","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. Formal Aspects Comput. 23(2), 191\u2013219 (2011)","journal-title":"Formal Aspects Comput."},{"key":"15_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, Cham (2014). doi:\n10.1007\/978-3-319-05032-4_16"},{"key":"15_CR8","unstructured":"James, P., M\u00f6ller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Decomposing scheme plans to manage verification complexity. In: FORMS\/FORMAT 2014\u201310th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems, pp. 210\u2013220. Institute for Traffic Safety and Automation Engineering, Technische Universit\u00e4t Braunschweig (2014)"},{"key":"15_CR9","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., Moller, 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, Cham (2014). doi:\n10.1007\/978-3-319-05032-4_19"},{"issue":"6","key":"15_CR10","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":"15_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, Cham (2016). doi:\n10.1007\/978-3-319-33951-1_10"},{"key":"15_CR12","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:\n10.1007\/978-3-319-47169-3_20"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-57288-8_11","volume-title":"NASA Formal Methods","author":"HD Macedo","year":"2017","unstructured":"Macedo, H.D., Fantechi, A., Haxthausen, A.E.: Compositional model checking of interlocking systems for lines with multiple stations. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 146\u2013162. Springer, Cham (2017). doi:\n10.1007\/978-3-319-57288-8_11"},{"key":"15_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.4204\/EPTCS.111.1","volume":"111","author":"Jan Peleska","year":"2013","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, pp. 3\u201328. Electronic Proceedings in Theoretical Computer Science, Open Publishing Association (2013)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"15_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":"15_CR16","unstructured":"Verified Systems International GmbH. RT-Tester Model-Based Test Case and Test Data Generator - RTT-MBT - User Manual (2013). \nhttp:\/\/www.verified.de"},{"key":"15_CR17","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":"15_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, Cham (2015). doi:\n10.1007\/978-3-319-17581-2_15"},{"key":"15_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)"},{"issue":"Part 2","key":"15_CR20","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.scico.2016.05.010","volume":"133","author":"LH Vu","year":"2017","unstructured":"Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modelling and verification of interlocking systems featuring sequential release. Sci. Comput. Program. 133(Part 2), 91\u2013115 (2017). doi:\n10.1016\/j.scico.2016.05.010","journal-title":"Sci. Comput. Program."},{"key":"15_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":"15_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:\n10.1007\/978-3-642-34032-1_24"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66197-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,24]],"date-time":"2018-07-24T23:51:56Z","timestamp":1532476316000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66197-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661964","9783319661971"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66197-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}