{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,23]],"date-time":"2025-12-23T05:03:26Z","timestamp":1766466206890,"version":"3.41.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319339504"},{"type":"electronic","value":"9783319339511"}],"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-33951-1_12","type":"book-chapter","created":{"date-parts":[[2016,6,14]],"date-time":"2016-06-14T09:21:26Z","timestamp":1465896086000},"page":"160-177","source":"Crossref","is-referenced-by-count":9,"title":["Comparing Formal Verification Approaches of Interlocking Systems"],"prefix":"10.1007","author":[{"given":"Anne Elisabeth","family":"Haxthausen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hoang Nga","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Roggenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,15]]},"reference":[{"key":"12_CR1","unstructured":"Banci, M., Fantechi, A., Gnesi, S.: Some experiences on formal specification of railway interlocking systems using statecharts. In: TRain Workshop at SEFM (Software Engineering and Formal Methods) (2005)"},{"key":"12_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. In: CSAE, pp. 511\u2013515. IEEE (2011)","DOI":"10.1109\/CSAE.2011.5952519"},{"key":"12_CR3","unstructured":"C. European Committee for Electrotechnical Standardization: EN 50128:2011 \u2013 railway applications \u2013 communications, signalling and processing systems \u2013 software for railway control andprotection systems (2011)"},{"key":"12_CR4","volume-title":"FORMS\/FORMAT","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. Springer, Heidelberg (2010)"},{"key":"12_CR5","unstructured":"Foldager, A.: A graphical domain-specific language for railway interlocking systems. Master\u2019s thesis, Technical University of Denmark, DTU Compute (2015)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/978-3-642-21292-5_10","volume-title":"Foundations of Computer Software","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)"},{"issue":"6","key":"12_CR7","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":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/978-3-642-12566-9_8","volume-title":"Foundations of Computer Software","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)"},{"issue":"2","key":"12_CR9","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). Special issue in Honour of Dines Bj\u00f8rner and Zhou Chaochen on Occasion of their 70th Birthdays","journal-title":"Formal Aspects Comput."},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1007\/978-3-319-08311-7_14","volume-title":"Reliable Software Technologies \u2013 Ada-Europe 2014","author":"A Iliasov","year":"2014","unstructured":"Iliasov, A., Lopatkin, I., Romanovsky, A.: Practical formal methods in railways - the safecap approach. In: George, L., Vardanega, T. (eds.) Ada-Europe 2014. LNCS, vol. 8454, pp. 177\u2013192. Springer, Heidelberg (2014)"},{"key":"12_CR12","volume-title":"Formal Techniques for Safety-Critical Systems","author":"P James","year":"2016","unstructured":"James, P., Lawrence, A., Roggenbach, M., Seisenberger, M.: Towards safety analysis of ERTMS\/ETCS level 2 in real-time maude. In: Artho, C., \u00d6lveczky, P.C. (eds.) Formal Techniques for Safety-Critical Systems. Springer, New York (2016)"},{"issue":"6","key":"12_CR13","doi-asserted-by":"crossref","first-page":"685","DOI":"10.1007\/s10009-014-0304-7","volume":"16","author":"P James","year":"2014","unstructured":"James, P., Moller, F., Nga, N.H., Roggenbach, M., Schneider, S.A., Treharne, H.: Techniques for modelling and verifying railway interlockings. STTT 16(6), 685\u2013711 (2014)","journal-title":"STTT"},{"key":"12_CR14","unstructured":"James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Decomposing scheme plans to manage verification complexity. FORMS\/FORMAT (2014)"},{"key":"12_CR15","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1016\/j.scico.2014.04.005","volume":"96","author":"P James","year":"2014","unstructured":"James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S.A., Treharne, H.: On modelling and verifying railway interlockings: tracking train lengths. Sci. Comput. Program 96, 315\u2013336 (2014)","journal-title":"Sci. Comput. Program"},{"issue":"1","key":"12_CR16","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/s11786-014-0174-0","volume":"8","author":"P James","year":"2014","unstructured":"James, P., Roggenbach, M.: Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans. Math. Comput. Sci. 8(1), 11\u201338 (2014)","journal-title":"Math. Comput. Sci."},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1007\/978-3-642-38088-4_30","volume-title":"NASA Formal Methods","author":"P James","year":"2013","unstructured":"James, P., Trumble, M., Treharne, H., Roggenbach, M., Schneider, S.: Ontrack: an open tooling environment for railway verification. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 435\u2013440. Springer, Heidelberg (2013)"},{"key":"12_CR18","volume-title":"Introduction to Railway Signalling","author":"D Kerr","year":"2001","unstructured":"Kerr, D., Rowbothan, T.: Introduction to Railway Signalling. Institution of Railway Signal Engineers, London (2001)"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge, D.: From Animation to Data Validation: The ProB Constraint Solver 10 Years On, pp. 427\u2013446. Wiley, Hoboken (2014)","DOI":"10.1002\/9781119002727.ch14"},{"issue":"1","key":"12_CR20","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. Prob. 4(1), 103\u2013110 (2009)","journal-title":"Transp. Prob."},{"key":"12_CR21","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, Rome, Italy, Electronic Proceedings in Theoretical Computer Science, vol. 111, pp. 3\u201328. Open Publishing Association (2013)","DOI":"10.4204\/EPTCS.111.1"},{"issue":"4","key":"12_CR22","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/s00165-005-0076-7","volume":"17","author":"S Schneider","year":"2005","unstructured":"Schneider, S., Treharne, H.: CSP theorems for communicating B machines. Formal Aspects Comput. 17(4), 390\u2013422 (2005)","journal-title":"Formal Aspects Comput."},{"key":"12_CR23","unstructured":"Tombs, D., Robinson, N., Nikandros, G.: Signalling control table generation and verification. In: Proceedings of Cost Efficient Railways through Engineering (CORE ), pp. 415\u2013425. Railway Technical Society of Australasia (2002)"},{"key":"12_CR24","unstructured":"Verified Systems International GmbH: RT-Tester Model-Based Test Case and Test Data Generator - RTT-MBT - User Manual (2013)"},{"key":"12_CR25","unstructured":"Vu, L.H.: Formal development and verification of railway control systems - in the context of ERTMS\/ETCS Level 2. Ph.D. thesis (2015)"},{"key":"12_CR26","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. Got best-paper-award, Institute for Traffic Safety and Automation Engineering, Technische Universit\u00e4t Braunschweig (2014)"},{"key":"12_CR27","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.) FTSCS 2014. CCIS, vol. 476, pp. 223\u2013238. Springer, Heidelberg (2015)"},{"key":"12_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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: Steffen, B., Margaria, T. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 246\u2013260. Springer, Heidelberg (2012)"},{"key":"12_CR29","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)"},{"issue":"5","key":"12_CR30","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1016\/j.jss.2005.05.030","volume":"79","author":"YT Yu","year":"2006","unstructured":"Yu, Y.T., Lau, M.F.: A comparison of MC\/DC, MUMCUT and several other coverage criteria for logical decisions. J. Syst. Softw. 79(5), 577\u2013590 (2006). Quality Software","journal-title":"J. Syst. Softw."}],"container-title":["Lecture Notes in Computer Science","Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33951-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T21:40:25Z","timestamp":1748986825000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33951-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319339504","9783319339511"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33951-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}