Abstract
This paper considers model checking the safety for members of a product line of railway interlocking systems, where an actual interlocking system is modelled as an instance of a generic model configured over the network under its control. For models over large networks it is a well-known problem that model checking may fail due to state space explosion. The RobustRailS tools that combine inductive reasoning with SMT solving using Jan Peleska’s powerful RT-Tester tool suite have pushed considerably the limits of the size of networks that can be handled. To further push these limits, we have proposed a compositional method that can be combined with RobustRailS to reduce the size of networks to be model checked: the idea is to divide the network of the system to be verified into two sub-networks and then model check the model instances for these sub-networks instead of that for the full network. In this paper we propose a strategy for applying such network divisions repeatedly to achieve a fine granularity decomposition of a given network into a number of small sub-networks. Under certain conditions, these sub-networks all belong to a library of pre-verified elementary networks, so model checking of the sub-networks is no longer needed.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
- 3.
- 4.
We are considering modern ERTMS level 2 based interlocking systems for which there are no physical signals. They are replaced by markerboards, and in the control system there are virtual signals associated with the markerboards. Throughout the paper we use the term signal as a synonym for markerboard.
- 5.
A network is loop-free, if there are no physically possible path through the network containing the same section more than once.
- 6.
In the end of Sect. 4.3 the notion of flank protection is explained.
- 7.
By connected we mean that by navigating the graph of the not yet visited part of the network starting from the two sides we eventually reach a common point.
- 8.
Note that when coming from the stem, we do not have such a problem, as a route cannot pass through a point via its two branches.
References
Fantechi, A., Gori, G., Haxthausen, A.E., Limbrée, C.: Compositional verification of railway interlockings: comparison of two methods. In: Dutilleul, S.C., Haxthausen, A.E., Lecomte, T. (eds.) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification: Fifth International Conference, RSSRail 2022, Paris, France, June 1–2, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13294, pp. 3–19. Springer Nature Switzerland AG (2022). https://doi.org/10.1007/978-3-031-05814-1_1
Fantechi, A., Haxthausen, A.E., Macedo, H.D.: Compositional verification of interlocking systems for large stations. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 236–252. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66197-1_15
Ferrari, A., Ter Beek, M.H.: Formal methods in railways: a systematic mapping study. ACM Comput. Surv. 55(4), 1–37 (2022)
Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: FORMS/FORMAT 2010 - Formal Methods for Automation and Safety in Railway and Automotive Systems. pp. 107–115. Springer (2010). https://doi.org/10.1007/978-3-642-14261-1_11
Ferrari, A., Mazzanti, F., Basile, D., ter Beek, M.H.: Systematic evaluation and usability analysis of formal methods tools for railway signaling system design. IEEE Trans. Softw. Eng. 48(11), 4675–4691 (2022)
Ferrari, A., Mazzanti, F., Basile, D., Ter Beek, M.H., Fantechi, A.: Comparing formal tools for system design: a judgment study. In: Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, pp. 62–74. ICSE 2020, Association for Computing Machinery, New York, NY, USA (2020)
Haxthausen, A.E., Østergaard, P.H.: On the use of static checking in the verification of interlocking systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 266–278. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_19
Haxthausen, A.E., Fantechi, A.: Compositional verification of railway interlocking systems. Form. Asp. Comput. 35(1) (2023). https://doi.org/10.1145/3549736
Huang, W., Peleska, J.: Complete model-based equivalence class testing. Int. J. Softw. Tools Technol. Transfer 18(3), 265–383 (2016)
James, P., Möller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Decomposing scheme plans to manage verification complexity. In: Schnieder, E., Tarnai, G. (eds.) FORMS/FORMAT 2014–10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems, pp. 210–220. Institute for Traffic Safety and Automation Engineering Technische Univ., Braunschweig (2014)
James, P., et al.: Verification of solid state interlocking programs. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 253–268. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05032-4_19
Limbrée, C., Cappart, Q., Pecheur, C., Tonetta, S.: Verification of Railway Interlocking - Compositional Approach with OCRA. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 134–149. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33951-1_10
Limbrée, C., Pecheur, C.: A framework for the formal verification of networks of railway interlockings - application to the Belgian railway. Electr. Commun. Eur. Assoc. Study Sci. Technol. 76 (2018)
Limbrée, C.: Formal verification of railway interlocking systems. Ph.D. thesis, UCL Louvain (2019)
Macedo, H.D., Fantechi, A., Haxthausen, A.E.: Compositional verification of multi-station interlocking systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 279–293. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_20
Macedo, H.D., Fantechi, A., Haxthausen, A.E.: Compositional model checking of interlocking systems for lines with multiple stations. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 146–162. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_11
Nguyen, A.N.A., Eilgaard, O.B.: Development and use of a tool supporting compositional verification of railway interlocking systems. Master’s thesis, Technical University of Denmark, DTU Compute (2020)
Peleska, J.: Industrial-strength model-based testing - state of the art and current challenges. In: Petrenko, A.K., Schlingloff, H. (eds.) 8th Workshop on Model-Based Testing, Rome, Italy. vol. 111, pp. 3–28. Open Publishing Association (2013)
Peleska, J., et al.: A real-world benchmark model for testing concurrent real-time systems in the automotive domain. In: Wolff, B., Zaïdi, F. (eds.) ICTSS 2011. LNCS, vol. 7019, pp. 146–161. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24580-0_11
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–312. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_22
Verified systems international GmbH: RT-Tester model-based test case and test data generator - RTT-MBT - User Manual (2013). http://www.verified.de
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–10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems, pp. 200–209. Institute for Traffic Safety and Automation Engineering Technische Universität, Braunschweig (2014)
Vu, L.H., Haxthausen, A.E., Peleska, J.: A domain-specific language for generic interlocking models and their properties. In: Fantechi, A., Lecomte, T., Romanovsky, A. (eds.) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification: Second International Conference, RSSRail 2017, Pistoia, Italy, November 14–16, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10598, pp. 99–115. Springer Cham (2017). https://doi.org/10.1007/978-3-319-68499-4_7
Vu, L.H.: Formal development and verification of railway control systems - In the context of ERTMS/ETCS Level 2. Ph.D. thesis, Technical University of Denmark, DTU Compute (2015)
Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modelling and verification of interlocking systems featuring sequential release. Sci. Comput. Programm. 133, Part 2, 91–115 (2017)
Winter, K.: Optimising ordering strategies for symbolic model checking of railway interlockings. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7610, pp. 246–260. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34032-1_24
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this chapter
Cite this chapter
Haxthausen, A.E., Fantechi, A., Gori, G. (2023). Decomposing the Verification of Interlocking Systems. In: Haxthausen, A.E., Huang, Wl., Roggenbach, M. (eds) Applicable Formal Methods for Safe Industrial Products. Lecture Notes in Computer Science, vol 14165. Springer, Cham. https://doi.org/10.1007/978-3-031-40132-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-031-40132-9_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-40131-2
Online ISBN: 978-3-031-40132-9
eBook Packages: Computer ScienceComputer Science (R0)