{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T04:30:21Z","timestamp":1770352221592,"version":"3.49.0"},"publisher-location":"Cham","reference-count":26,"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_18","type":"book-chapter","created":{"date-parts":[[2014,3,7]],"date-time":"2014-03-07T09:36:26Z","timestamp":1394184986000},"page":"237-252","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Validation of Railway Interlocking Systems by Formal Verification, A Case Study"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Bonacchi","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[]},{"given":"Stefano","family":"Bacherini","sequence":"additional","affiliation":[]},{"given":"Matteo","family":"Tempestini","sequence":"additional","affiliation":[]},{"given":"Leonardo","family":"Cipriani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,3,8]]},"reference":[{"key":"18_CR1","unstructured":"European Committee for Electrotechnical Standardization, CENELEC EN50128, Railway applications-Communication signalling and processing system software for railway control and protection systems"},{"key":"18_CR2","unstructured":"Simulink$$^{\\textregistered }$$: Design Verifier R2012b. MathWorks (2012)"},{"key":"18_CR3","unstructured":"Simulink$$^{\\textregistered }$$: User Guide R2012b. MathWorks (2012)"},{"key":"18_CR4","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1023\/A:1008645826258","volume":"12","author":"C Bernardeschi","year":"1998","unstructured":"Bernardeschi, C., Fantechi, A., Gnesi, S., Larosa, S., Mongardi, G., Romano, D.: A formal verification environment for railway signaling system design. Formal Methods Syst. Des. 12, 139\u2013161 (1998)","journal-title":"Formal Methods Syst. Des."},{"key":"18_CR5","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)"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Bonacchi, A.: Formal safety proof: a real case study in a railway interlocking system. In: ISSTA, pp. 378\u2013381. ACM (2013)","DOI":"10.1145\/2483760.2492398"},{"key":"18_CR7","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/s001650050021","volume":"10","author":"A Bor\u00e4lv","year":"1998","unstructured":"Bor\u00e4lv, A.: Case study: formal verification of a computerized railway interlocking. Formal Asp. Comput. 10, 338\u2013360 (1998)","journal-title":"Formal Asp. Comput."},{"issue":"8","key":"18_CR8","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"18_CR9","series-title":"LNCS","first-page":"359","volume-title":"CAV 2002","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an OpenSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"18_CR10","series-title":"LNCS","first-page":"154","volume-title":"CAV 2000","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"18_CR11","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: FORMS\/FORMAT, pp. 98\u2013107 (2010)","DOI":"10.1007\/978-3-642-14261-1_11"},{"key":"18_CR13","unstructured":"Fokkink, W., Hollingshead, P.: Verification of interlockings: from control tables to ladder logic diagrams. In: FMICS\u201998, pp. 171\u2013185 (1998)"},{"key":"18_CR14","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1109\/64.180408","volume":"7","author":"B Fringuelli","year":"1992","unstructured":"Fringuelli, B., Lamma, E., Mello, P., Santocchia, G.: Knowledge-based technology for controlling railway stations. IEEE Expert: Intell. Syst. Appl. 7, 45\u201352 (1992)","journal-title":"IEEE Expert: Intell. Syst. Appl."},{"key":"18_CR15","unstructured":"Groote, J.F., van Vlijmen, S., Koorn, J.: The Safety Guaranteeing System at Station Hoorn-Kersenboogerd. In: Logic Group Preprint Series 121. Utrecht University (1995)"},{"key":"18_CR16","unstructured":"Hansen, K.M.: Formalising railway interlocking systems. In: Proceedings of the 2nd FMERail, Workshop (1998)"},{"issue":"2\u20133","key":"18_CR17","first-page":"241","volume":"3","author":"AE Haxthausen","year":"2009","unstructured":"Haxthausen, A.E.: Developing a domain model for relay circuits. Int. J. Softw. Inf. 3(2\u20133), 241\u2013272 (2009)","journal-title":"Int. J. Softw. Inf."},{"key":"18_CR18","series-title":"LNCS","first-page":"141","volume-title":"Monterey Workshop 2008","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":"18_CR19","unstructured":"Holzmann, G.: Spin Model Checker, The Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)"},{"key":"18_CR20","unstructured":"James, P., Roggenbach, M.: Automatically verifying railway interlockings using SAT-based model checking. In: AVOCS, pp. 141\u2013153 (2010)"},{"issue":"2","key":"18_CR21","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.entcs.2009.08.015","volume":"250","author":"K Kanso","year":"2009","unstructured":"Kanso, K., Moller, F., Setzer, A.: Automated verification of signalling principles in railway interlocking systems. Electron. Notes Theor. Comput. Sci. 250(2), 19\u201331 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"2","key":"18_CR22","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1016\/S1571-0661(04)81050-8","volume":"89","author":"KJ Kristoffersen","year":"2003","unstructured":"Kristoffersen, K.J., Pedersen, C., Andersen, H.R.: Runtime verification of timed LTL using disjunctive normalized equation systems. Electr. Notes Theor. Comput. Sci. 89(2), 210\u2013225 (2003)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"18_CR23","first-page":"103","volume":"4","author":"A Mirabadi","year":"2009","unstructured":"Mirabadi, A., Yazdi, M.: Automatic generation and verification of railway interlocking control tables using FSM and NuSMV. Transport Prob.: Int. Sci. J. 4, 103\u2013110 (2009)","journal-title":"Transport Prob.: Int. Sci. J."},{"key":"18_CR24","series-title":"LNCS","first-page":"137","volume-title":"COORDINATION 2010","author":"S Vanit-Anunchai","year":"2010","unstructured":"Vanit-Anunchai, S.: Modelling railway interlocking tables using coloured petri nets. In: Clarke, D., Agha, G. (eds.) COORDINATION 2010. LNCS, vol. 6116, pp. 137\u2013151. Springer, Heidelberg (2010)"},{"key":"18_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, pp. 101\u2013107 (2006)"},{"key":"18_CR26","unstructured":"Winter, K., Robinson, N.J.: Modelling large railway interlockings and model checking small ones. In: Twenty-Sixth Australasian Computer Science Conference (ACSC2003), Adelaide, South Australia, pp. 309\u2013316 (2003)"}],"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_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,7]],"date-time":"2023-02-07T22:14:05Z","timestamp":1675808045000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05032-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319050317","9783319050324"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05032-4_18","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"}}]}}