{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T17:00:44Z","timestamp":1783530044318,"version":"3.55.0"},"publisher-location":"Cham","reference-count":23,"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_19","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T21:56:23Z","timestamp":1475618183000},"page":"266-278","source":"Crossref","is-referenced-by-count":18,"title":["On the Use of Static Checking in the Verification of Interlocking Systems"],"prefix":"10.1007","author":[{"given":"Anne E.","family":"Haxthausen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter H.","family":"\u00d8stergaard","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"19_CR1","unstructured":"Banci, M., Fantechi, A., Gnesi, S.: Some Experiences on Formal Specification of Railway Interlocking Systems Using Statecharts (2005)"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Cao, Y., Xu, T., Tang, T., Wang, H., Zhao, L.: Automatic generation and verification of interlocking tables based on domain specific language for computer based interlocking systems (DSL-CBI). In: Proceedings of the IEEE International Conference on Computer Science and Automation Engineering (CSAE 2011), pp. 511\u2013515. IEEE (2011)","DOI":"10.1109\/CSAE.2011.5952519"},{"key":"19_CR3","unstructured":"C. European Committee for Electrotechnical Standardization. EN 50128:2011 - Railway applications - Communications, signalling and processing systems - Software for railway control and protection systems (2011)"},{"key":"19_CR4","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). doi: 10.1007\/978-3-319-05032-4_13"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) FORMS\/FORMAT 2010 \u2013 Formal Methods for Automation and Safety in Railway and Automotive Systems, pp. 107\u2013115. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-14261-1_11"},{"key":"19_CR6","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":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-642-21292-5_10","volume-title":"Foundations of Computer Software. Modeling, Development, and Verification of Adaptive Systems","author":"AE Haxthausen","year":"2011","unstructured":"Haxthausen, A.E.: Towards a framework for modelling and verification of relay interlocking systems. In: Calinescu, R., Jackson, E. (eds.) Monterey Workshop 2010. LNCS, vol. 6662, pp. 176\u2013192. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-21292-5_10"},{"issue":"6","key":"19_CR8","doi-asserted-by":"crossref","first-page":"713","DOI":"10.1007\/s10009-013-0295-9","volume":"16","author":"AE Haxthausen","year":"2014","unstructured":"Haxthausen, A.E.: Automated generation of formal safety conditions from railway interlocking tables. Int. J. Softw. Tools Technol. Transf. (STTT) 16(6), 713\u2013726 (2014). Special Issue on Formal Methods for Railway Control Systems","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"19_CR9","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"},{"issue":"2","key":"19_CR10","doi-asserted-by":"crossref","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":"19_CR11","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 $$||$$ | | 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":"19_CR12","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":"19_CR13","first-page":"103","volume":"4","author":"A Mirabadi","year":"2009","unstructured":"Mirabadi, A., Yazdi, M.B.: Automatic generation and verification of railway interlocking control tables using FSM and NuSMV. Transp. Probl. 4, 103\u2013110 (2009)","journal-title":"Transp. Probl."},{"key":"19_CR14","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.) Proceedings 8th Workshop on Model-Based Testing. Electronic Proceedings in Theoretical Computer Science, vol. 111, pp. 3\u201328. Open Publishing Association, Rome (2013)","DOI":"10.4204\/EPTCS.111.1"},{"key":"19_CR15","unstructured":"George, C., Haff, P., Havelund, K., Haxthausen, A.E., Milne, R., Nielsen, C.b., Prehn, S., Wagner, K.R: The RAISE Language Group: The RAISE Specification Language. The BCS Practitioners Series. Prentice Hall Int. (1992)"},{"key":"19_CR16","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":"19_CR17","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":"19_CR18","unstructured":"Verified Systems International GmbH. RT-Tester Model-Based Test Case and Test Data Generator - RTT-MBT - User Manual (2013). Available on request from http:\/\/www.verified.de"},{"key":"19_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":"19_CR20","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, Institute for Traffic Safety and Automation Engineerin, pp. 200\u2013209. Technische Universit\u00e4t Braunschweig (2014)"},{"key":"19_CR21","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, Heidelberg (2015)"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modeling and verification of interlocking systems featuring sequential release. Sci. Comput. Program. (2016). http:\/\/dx.doi.org\/10.1016\/j.scico.2016.05.010","DOI":"10.1016\/j.scico.2016.05.010"},{"key":"19_CR23","unstructured":"Winter, K., Johnston, W., Robinson, P., Strooper, P., van den Berg, L.: Tool support for checking railway interlocking designs. In: Proceedings of the 10th Australian Workshop on Safety Critical Systems and Software, SCS 2005, vol. 55, pp. 101\u2013107. Australian Computer Society, Inc., Darlinghurst (2006)"}],"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_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T23:09:12Z","timestamp":1749596952000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47169-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471686","9783319471693"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47169-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}