{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T04:05:35Z","timestamp":1746158735215,"version":"3.40.4"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2013,12,22]],"date-time":"2013-12-22T00:00:00Z","timestamp":1387670400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,11]]},"DOI":"10.1007\/s10009-013-0295-9","type":"journal-article","created":{"date-parts":[[2013,12,21]],"date-time":"2013-12-21T06:25:13Z","timestamp":1387607113000},"page":"713-726","source":"Crossref","is-referenced-by-count":19,"title":["Automated generation of formal safety conditions from railway interlocking tables"],"prefix":"10.1007","volume":"16","author":[{"given":"Anne E.","family":"Haxthausen","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,12,22]]},"reference":[{"key":"295_CR1","unstructured":"Aan\u00e6s, M., Thai, H.P.: Modelling and verification of relay interlocking systems. Technical Report IMM-MSC-2012-14, DTU Informatics. Master thesis supervised by Anne Haxthausen, ah@imm.dtu.dk, Technical University of Denmark (2012)"},{"key":"295_CR2","unstructured":"Banci, M., Fantechi, A., Gnesi, S.: Some experiences on formal specification of railway interlocking systems using Statecharts (2005)"},{"key":"295_CR3","unstructured":"Bj\u00f8rner, D.: New results and current trends in formal techniques for the development of software for transportation systems. In: Tanai, G., Schnieder, E. (eds.) Proceedings of the Symposium on Formal Methods for Railway Operation and Control Systems (FORMS\u20192003), Budapest\/Hungary. L\u2019Harmattan Hongrie, 15\u201316 May 2003, pp. 3\u201322"},{"key":"295_CR4","unstructured":"Bliguet, M.L., Kj\u00e6r, A.A.: Modelling interlocking systems for railway stations. Technical Report IMM-M.Sc.-2008-68, DTU Informatics. Master thesis supervised by Anne Haxthausen, ah@imm.dtu.dk, Technical University of Denmark (2008)"},{"key":"295_CR5","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":"295_CR6","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. The MIT Press, Cambridge (1999)"},{"key":"295_CR7","unstructured":"de Moura, L., Owre, S., Shankar, N.: The SAL language manual. Technical Report SRI-CSL-01-02, SRI International, 2003. Available from http:\/\/sal.csl.sri.com"},{"key":"295_CR8","doi-asserted-by":"crossref","unstructured":"Eriksson, L.-H.: Using formal methods in a retrospective safety case. In: Computer safety, reliability, and security\u201423rd International Conference, SAFECOMP 2004, volume 3219 of Lecture Notes in Computer Science. Springer, Berlin, Heidelberg (2004)","DOI":"10.1007\/978-3-540-30138-7_4"},{"key":"295_CR9","unstructured":"European Committee for Electrotechnical Standardization: EN 50128:2011\u2014Railway applications\u2014communications, signalling and processing systems\u2014software for railway control and protection systems. CENELEC, Brussels (2011)"},{"key":"295_CR10","doi-asserted-by":"crossref","unstructured":"Fantechi, A.: The role of formal methods in software development for railway applications. In: Railway safety, reliability and security: technologies and system engineering, pp. 282\u2013297. IGI Global, USA (2012)","DOI":"10.4018\/978-1-4666-1643-1.ch012"},{"key":"295_CR11","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, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-14261-1_11"},{"key":"295_CR12","doi-asserted-by":"crossref","unstructured":"Haxthausen, A.E.: Towards a framework for modelling and verification of relay interlocking systems. In: 16th Monterey Workshop: modelling, development and verification of adaptive systems: the grand challenge for robust software, number 6662 in Lecture Notes in Computer Science. Springer, Berlin, Heidelberg (2011) (Invited paper)","DOI":"10.1007\/978-3-642-21292-5_10"},{"key":"295_CR13","doi-asserted-by":"crossref","unstructured":"Haxthausen, A.E., Bliguet, M.L., Kj\u00e6r, A.A.: Modelling and verification of relay interlocking systems. In: Choppy, C., Sokolsky, O. (eds.) 15th Monterey Workshop: foundations of computer software, pp. 141\u2013153. Future trends and techniques for development, number 6028 in Lecture Notes in Computer Science. Springer, Berlin, Heidelberg (2010) (Invited paper)","DOI":"10.1007\/978-3-642-12566-9_8"},{"key":"295_CR14","doi-asserted-by":"crossref","unstructured":"Haxthausen, A.E., Kj\u00e6r, A.A., Bliguet, M.L.: Formal development of a tool for automated modelling and verification of relay interlocking systems. In: 17th International Symposium on Formal Methods (FM 2011), number 6664 in Lecture Notes in Computer Science, pp. 118\u2013132. Springer, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-21437-0_11"},{"key":"295_CR15","doi-asserted-by":"crossref","unstructured":"Haxthausen, A.E., Peleska, J., Kinder, S.: A formal approach for the construction and verification of railway control systems. Formal aspects of computing, 23(2):191\u2013219, (2011). The article is also available electronically on SpringerLink: http:\/\/www.springerlink.com\/openhbreakurls.asp?genre=article&id=doi:10.1007\/s00165-009-0143-6","DOI":"10.1007\/s00165-009-0143-6"},{"key":"295_CR16","doi-asserted-by":"crossref","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":"295_CR17","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)"},{"key":"295_CR18","doi-asserted-by":"crossref","unstructured":"Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Defining and model checking abstractions of complex railway models using CSP $$\\parallel $$ \u2016 B. In: Hardware and Software: Verification and Testing, 8th International Haifa Verification Conference, number 7857 in Lecture Notes in Computer Science. Springer, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-39611-3_20"},{"key":"295_CR19","doi-asserted-by":"crossref","unstructured":"Schnieder, E., Tarnai, G. (eds.): Proceedings of formal methods for automation and safety in railway and automotive systems (FORMS\/FORMAT 2010). Springer, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-14261-1"},{"key":"295_CR20","unstructured":"Symbolic Analysis Laboratory, SAL, home page: http:\/\/sal.csl.sri.com (2001)"},{"key":"295_CR21","unstructured":"The RAISE Language Group: The RAISE specification language. The BCS Practitioners Series. Prentice Hall Int., UK (1992)"},{"key":"295_CR22","unstructured":"The RAISE Method Group: The RAISE development method. The BCS Practitioners Series. Prentice Hall Int., UK (1995)"},{"key":"295_CR23","doi-asserted-by":"crossref","unstructured":"Winter, K.: Optimising ordering strategies for symbolic model checking of railway interlockings. In: 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA\u20192012), Part II, number 7610 in Lecture Notes in Computer Science, pp. 246\u2013260. Springer, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-34032-1_24"},{"key":"295_CR24","doi-asserted-by":"crossref","unstructured":"Winter, K.: Symbolic model checking for interlocking systems. In: Railway safety, reliability and security: technologies and system engineering, pp. 298\u2013315. IGI Global, USA (2012)","DOI":"10.4018\/978-1-4666-1643-1.ch013"},{"key":"295_CR25","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, vol. 55, SCS \u201905, pp. 101\u2013107. Australian Computer Society Inc., Darlinghurst (2006)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0295-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0295-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0295-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T08:34:58Z","timestamp":1746088498000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0295-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12,22]]},"references-count":25,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2014,11]]}},"alternative-id":["295"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0295-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2013,12,22]]}}}