{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T21:14:21Z","timestamp":1770412461369,"version":"3.49.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319050317","type":"print"},{"value":"9783319050324","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-319-05032-4_16","type":"book-chapter","created":{"date-parts":[[2014,3,7]],"date-time":"2014-03-07T09:36:26Z","timestamp":1394184986000},"page":"205-220","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["Applied Bounded Model Checking for Interlocking System Designs"],"prefix":"10.1007","author":[{"given":"Anne E.","family":"Haxthausen","sequence":"first","affiliation":[]},{"given":"Jan","family":"Peleska","sequence":"additional","affiliation":[]},{"given":"Ralf","family":"Pinger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,3,8]]},"reference":[{"key":"16_CR1","unstructured":"Guide to the software engineering body of knowledge. Technical report, IEEE Computer Society (2004). http:\/\/www.computer.org\/portal\/web\/swebok\/htmlformat"},{"key":"16_CR2","series-title":"LNCS","first-page":"369","volume-title":"FM 1999","author":"P Behm","year":"1999","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: M\u00e9t\u00e9or: a successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369\u2013387. Springer, Heidelberg (1999)"},{"key":"16_CR3","series-title":"LNCS","first-page":"193","volume-title":"TACAS 1999","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"issue":"5","key":"16_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-2(5:5)2006","volume":"2","author":"A Biere","year":"2006","unstructured":"Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Meth. Comput. Sci. 2(5), 1\u201364 (2006)","journal-title":"Log. Meth. Comput. Sci."},{"key":"16_CR5","unstructured":"Bj\u00f8rner, D.: New results and current trends in formal techniques for the development of software for transportation systems. In: Proceedings of the Symposium on Formal Methods for Railway Operation and Control Systems (FORMS\u20192003). L\u2019Harmattan Hongrie, Budapest, 15\u201316 May 2003"},{"key":"16_CR6","unstructured":"Clabaut, M., Metayer, C., Morand, E.: 4B\u20132 formal data validation - formal techniques applied to verification of data properties. In: Embedded Real Time Software and Systems ERTS (2010)"},{"key":"16_CR7","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"issue":"3","key":"16_CR8","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1049\/ip-cdt:20045073","volume":"152","author":"R Drechsler","year":"2005","unstructured":"Drechsler, R., Gro\u00dfe, D.: System level validation using formal techniques. IEE Proc. - Comput. Digit. Tech. 152(3), 393\u2013406 (2005)","journal-title":"IEE Proc. - Comput. Digit. Tech."},{"key":"16_CR9","volume-title":"EN 50128:2011 - Railway Applications - Communications, Signalling and Processing Systems - Software for Railway Control and Protection Systems","author":"European Committee for Electrotechnical Standardization","year":"2011","unstructured":"European Committee for Electrotechnical Standardization: EN 50128:2011 - Railway Applications - Communications, Signalling and Processing Systems - Software for Railway Control and Protection Systems. CENELEC, Brussels (2011)"},{"key":"16_CR10","series-title":"LNCS","first-page":"276","volume-title":"ISoLA 2012, Part II","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":"16_CR11","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1002\/9781118459898.ch4","volume-title":"In: Formal Methods for Industrial Critical Systems","author":"A Fantechi","year":"2012","unstructured":"Fantechi, A., Fokkink, W.J., Morzenti, A.: Some trends in formal methods applications to railway signaling. In: Formal Methods for Industrial Critical Systems, pp. 61\u201384. Wiley, Hoboken (2012)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS\/FORMAT 2010). Springer, Braunschweig (2011)","DOI":"10.1007\/978-3-642-14261-1_11"},{"issue":"8","key":"16_CR13","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 system. IEEE Trans. Softw. Eng. 26(8), 687\u2013701 (2000)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"16_CR14","series-title":"LNCS","first-page":"176","volume-title":"Monterey Workshop 2010","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)"},{"key":"16_CR15","series-title":"LNCS","first-page":"261","volume-title":"ISoLA 2012, Part II","author":"AE Haxthausen","year":"2012","unstructured":"Haxthausen, A.E.: Automated generation of safety requirements from railway interlocking tables. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 261\u2013275. Springer, Heidelberg (2012)"},{"key":"16_CR16","first-page":"127","volume-title":"In: 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: Railways: Types, Design and Safety Issues, pp. 127\u2013148. Nova Science Publishers Inc, New York (2013)"},{"issue":"2","key":"16_CR17","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":"16_CR18","unstructured":"Lecomte, T., Burdy, L., Leuschel, M.: Formally checking large data sets in the railways. CoRR, abs\/1210.6815 (2012)"},{"key":"16_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992)"},{"key":"16_CR20","series-title":"LNCS","first-page":"193","volume-title":"HVC","author":"F Moller","year":"2013","unstructured":"Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Defining and model checking abstractions of complex railway models using CSP$$||$$B. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, pp. 193\u2013208. Springer, Heidelberg (2013)"},{"key":"16_CR21","volume-title":"Railway Operation and Control","author":"J Pachl","year":"2002","unstructured":"Pachl, J.: Railway Operation and Control. VTD Rail Publishing, Mountlake Terrace (2002)"},{"key":"16_CR22","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 Eighth Workshop on Model-Based Testing, Rome, 17 March 2013. Electronic Proceedings in Theoretical Computer Science, vol. 111, pp. 3\u201328. Open Publishing Association (2013)","DOI":"10.4204\/EPTCS.111.1"},{"key":"16_CR23","series-title":"LNCS","first-page":"298","volume-title":"NFM 2011","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)"},{"issue":"5","key":"16_CR24","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"AP Sistla","year":"1994","unstructured":"Sistla, A.P.: Liveness and fairness in temporal logic. Form. Aspects Comput. 6(5), 495\u2013512 (1994)","journal-title":"Form. Aspects Comput."},{"key":"16_CR25","series-title":"LNCS","first-page":"246","volume-title":"ISoLA 2012, Part II","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":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-05032-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,14]],"date-time":"2023-02-14T12:12:43Z","timestamp":1676376763000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05032-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319050317","9783319050324"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05032-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"8 March 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}