Abstract
Notwithstanding the large amount of attempts to formally verify them, railway interlocking systems still represent a challenging problem for automatic verification. Interlocking systems controlling sufficiently large stations, due to their inherent complexity related to the high number of variables involved, are not readily amenable to automatic verification, typically incurring in state space explosion problems. The study described in this paper aims at evaluating and experimenting the industrial application of verification by model checking for this class of systems. The choices made at the beginning of the study, also on the basis of specific requirements from the industrial partner, are presented, together with the advancement status of the project and the plans for its completion.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
European Committee for Electrotechnical Standardization, CENELEC EN50128, Railway applications-Communication signalling and processing system software for railway control and protection systems
Simulink\(^{\textregistered }\): Design Verifier R2012b. MathWorks (2012)
Simulink\(^{\textregistered }\): User Guide R2012b. MathWorks (2012)
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–161 (1998)
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–207. Springer, Heidelberg (1999)
Bonacchi, A.: Formal safety proof: a real case study in a railway interlocking system. In: ISSTA, pp. 378–381. ACM (2013)
Borälv, A.: Case study: formal verification of a computerized railway interlocking. Formal Asp. Comput. 10, 338–360 (1998)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)
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–364. Springer, Heidelberg (2002)
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–169. Springer, Heidelberg (2000)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: FORMS/FORMAT, pp. 98–107 (2010)
Fokkink, W., Hollingshead, P.: Verification of interlockings: from control tables to ladder logic diagrams. In: FMICS’98, pp. 171–185 (1998)
Fringuelli, B., Lamma, E., Mello, P., Santocchia, G.: Knowledge-based technology for controlling railway stations. IEEE Expert: Intell. Syst. Appl. 7, 45–52 (1992)
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)
Hansen, K.M.: Formalising railway interlocking systems. In: Proceedings of the 2nd FMERail, Workshop (1998)
Haxthausen, A.E.: Developing a domain model for relay circuits. Int. J. Softw. Inf. 3(2–3), 241–272 (2009)
Haxthausen, A.E., Le Bliguet, M., Kjær, A.A.: Modelling and verification of relay interlocking systems. In: Choppy, C., Sokolsky, O. (eds.) Monterey Workshop 2008. LNCS, vol. 6028, pp. 141–153. Springer, Heidelberg (2010)
Holzmann, G.: Spin Model Checker, The Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)
James, P., Roggenbach, M.: Automatically verifying railway interlockings using SAT-based model checking. In: AVOCS, pp. 141–153 (2010)
Kanso, K., Moller, F., Setzer, A.: Automated verification of signalling principles in railway interlocking systems. Electron. Notes Theor. Comput. Sci. 250(2), 19–31 (2009)
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–225 (2003)
Mirabadi, A., Yazdi, M.: Automatic generation and verification of railway interlocking control tables using FSM and NuSMV. Transport Prob.: Int. Sci. J. 4, 103–110 (2009)
Vanit-Anunchai, S.: Modelling railway interlocking tables using coloured petri nets. In: Clarke, D., Agha, G. (eds.) COORDINATION 2010. LNCS, vol. 6116, pp. 137–151. Springer, Heidelberg (2010)
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–107 (2006)
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–316 (2003)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Bonacchi, A., Fantechi, A., Bacherini, S., Tempestini, M., Cipriani, L. (2014). Validation of Railway Interlocking Systems by Formal Verification, A Case Study. In: Counsell, S., Núñez, M. (eds) Software Engineering and Formal Methods. SEFM 2013. Lecture Notes in Computer Science(), vol 8368. Springer, Cham. https://doi.org/10.1007/978-3-319-05032-4_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-05032-4_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-05031-7
Online ISBN: 978-3-319-05032-4
eBook Packages: Computer ScienceComputer Science (R0)