{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T00:32:52Z","timestamp":1770337972832,"version":"3.49.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319175805","type":"print"},{"value":"9783319175812","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17581-2_15","type":"book-chapter","created":{"date-parts":[[2015,4,15]],"date-time":"2015-04-15T12:22:36Z","timestamp":1429100556000},"page":"223-238","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release"],"prefix":"10.1007","author":[{"given":"Linh H.","family":"Vu","sequence":"first","affiliation":[]},{"given":"Anne E.","family":"Haxthausen","sequence":"additional","affiliation":[]},{"given":"Jan","family":"Peleska","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,16]]},"reference":[{"key":"15_CR1","unstructured":"Aan\u00e6s, M., Thai, H.P.: Modelling and verification of relay interlocking systems. Master\u2019s thesis, Technical University of Denmark, DTU Informatics (2012). Series: IMM-MSC-2012-14"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Behnia, S., Mammar, A., Mota, J.-M., Breton, N., Caspi, P., Raymond, P.: Industrialising a proof-based verification approach of computerised interlocking systems. In: Allan, J., Arias, E., Brebbia, C.A., Goodman, C., Rumsey, A.F., Sciutto, G., Tomii, N. (eds.) Eleventh International Conference on Computer System Design and Operation in the Railway and Other Transit Systems (COMPRAIL 2008). WIT Press (2008)","DOI":"10.2495\/CR080151"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-540-45069-6_2","volume-title":"Computer Aided Verification","author":"L de Moura","year":"2003","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Bounded model checking and induction: from refutation to verification. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 14\u201326. Springer, Heidelberg (2003)"},{"key":"15_CR4","unstructured":"ERTMS: Annex A for ETCS Baseline 3 and GSM-R Baseline 0, April 2012"},{"key":"15_CR5","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_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-34032-1_26","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"A Fantechi","year":"2012","unstructured":"Fantechi, A.: Distributing the challenge of model checking interlocking control tables. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 276\u2013289. Springer, Heidelberg (2012)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-319-05032-4_13","volume-title":"Software Engineering and Formal Methods","author":"A Fantechi","year":"2014","unstructured":"Fantechi, A.: Twenty-five years of formal methods and railways: what next? In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 167\u2013183. Springer, Heidelberg (2014)"},{"key":"15_CR8","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":"15_CR9","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., van de Pol, J., dos Santos, O.M.: Automated verification of executable UML models. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 6957, pp. 225\u2013250. Springer, Heidelberg (2011)"},{"key":"15_CR10","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., Le 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)"},{"key":"15_CR11","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1109\/32.879808","volume":"26","author":"AE Haxthausen","year":"2000","unstructured":"Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control systems. IEEE Trans. Softw. Eng. 26, 687\u2013701 (2000)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"15_CR12","first-page":"127","volume-title":"Railways: Types, Design and Safety Issues","author":"AE Haxthausen","year":"2013","unstructured":"Haxthausen, A.E., Peleska, J.: Efficient development and verification of safe railway control software. In: Reinhardt, C., Shroeder, K. (eds.) Railways: Types, Design and Safety Issues, pp. 127\u2013148. Nova Science Publishers Inc, New York (2013)"},{"key":"15_CR13","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, 191\u2013219 (2011). Springer","journal-title":"Formal Aspects Comput."},{"key":"15_CR14","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)"},{"key":"15_CR15","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., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H., Trumble, M., Williams, D.: Verification of scheme plans using CSP\u2014\u2014B. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 189\u2013204. Springer, Heidelberg (2014)"},{"key":"15_CR16","unstructured":"James, P., Roggenbach, M.: Automatically verifying railway interlockings using sat-based model checking. In: Proceedings of the Electronic Communications of the EASST, vol. 35, EASST (2011)"},{"key":"15_CR17","first-page":"3","volume-title":"Proceedings of the 8th Workshop on Model-Based Testing, Electronic Proceedings in Theoretical Computer Science","author":"J 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.) Proceedings of the 8th Workshop on Model-Based Testing, Electronic Proceedings in Theoretical Computer Science, vol. 111, pp. 3\u201328. Open Publishing Association, Rome, Italy (2013)"},{"key":"15_CR18","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)"},{"key":"15_CR19","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_CR20","unstructured":"Tombs, D., Robinson, N., Nikandros, G.: Signalling control table generation and verification. In: CORE 2002: Cost Efficient Railways through Engineering, p. 415. Railway Technical Society of Australasia\/Rail Track Association of Australia (2002)"},{"key":"15_CR21","unstructured":"Verified Systems International GmbH: RT-Tester Model-Based Test Case and Test Data Generator - RTT-MBT - User Manual (2013)"},{"key":"15_CR22","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_CR23","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","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, Part II. LNCS, vol. 7610, pp. 246\u2013260. Springer, Heidelberg (2012)"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17581-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,20]],"date-time":"2023-02-20T23:46:03Z","timestamp":1676936763000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17581-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175805","9783319175812"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17581-2_15","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"value":"1865-0929","type":"print"},{"value":"1865-0937","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}