Abstract
Formal verification of safety of interlocking systems and of their configuration on a specific track layout is conceptually an easy task for model checking. Systems that control large railway networks, however, are challenging due to state space explosion problems. A possible way out is to adopt a compositional approach that allows safety of a large system to be deduced from the formal verification of parts in which the system has been properly decomposed. Two different approaches have been proposed in this regard, differing for the decomposition assumptions and for the adopted compositional verification techniques. In this paper we compare the two approaches, discussing the differences, but also showing how the different concepts behind them are essentially equivalent, hence producing comparable benefits.
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
Similar content being viewed by others
Notes
- 1.
The automatization of cut placements for RobustRailS tool is currently an undergoing activity.
- 2.
- 3.
The formal equivalence of the two presented methods is out of scope of this paper.
- 4.
The models are available at https://github.com/gorigloria/compositionalverificationmodels.
References
Bonacchi, A., Fantechi, A., Bacherini, S., Tempestini, M.: Validation process for railway interlocking systems. Sci. Comput. Program. 128, 2–21 (2016)
Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_7
Busard, S., Cappart, Q., Limbrée, C., Pecheur, C., Schaus, P.: Verification of railway interlocking systems. In: Proceedings of the ESSS 2015, Oslo, Norway, 22 June 2015. EPTCS, vol. 184, pp. 19–31. Open Publishing Association (2015)
Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: 28th IEEE/ACM International Conference on Automated Software Engineering, Silicon Valley, CA, USA, 11–15 November 2013, pp. 702–705. IEEE (2013)
Cimatti, A., Tonetta, S.: A property-based proof system for contract-based design. In: 38th Euromicro Conference on Software Engineering and Advanced Applications, pp. 21–28. IEEE (2012)
Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97, 333–348 (2015)
Claessen, K., Sörensson, N.: A liveness checking algorithm that counts. In: Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, 22–25 October 2012, pp. 52–59. IEEE (2012)
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., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) FORMS/FORMAT 2010, pp. 107–115. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14261-1_11
Haxthausen, A.E., Fantechi, A.: Compositional verification of railway interlocking systems. Submitted for publication (2021)
Haxthausen, A.E., Nguyen, H.N., Roggenbach, M.: Comparing formal verification approaches of interlocking systems. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 160–177. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33951-1_12
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
James, P., Möller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Decomposing scheme plans to manage verification complexity. In: FORMS/FORMAT 2014, 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. Electron. Commun. Eur. Assoc. Softw. 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
Peleska, J.: Industrial-strength model-based testing - state of the art and current challenges. In: 8th Workshop on Model-Based Testing, Rome, Italy, vol. 111, pp. 3–28. Open Publishing Association (2013)
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: FORMS/FORMAT 2014. 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.) RSSRail 2017. LNCS, 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. Program. 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
Acknowledgement
The authors wish to thank Jan Peleska and Linh H. Vu with whom Anne Haxthausen developed the RobustRailS verification method and tools, and Hugo D. Macedo, who collaborated in the initial work of Anne Haxthausen and Alessandro Fantechi on the RobustRailS compositional approach.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this paper
Cite this paper
Fantechi, A., Gori, G., Haxthausen, A.E., Limbrée, C. (2022). Compositional Verification of Railway Interlockings: Comparison of Two Methods. In: Collart-Dutilleul, S., Haxthausen, A.E., Lecomte, T. (eds) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2022. Lecture Notes in Computer Science, vol 13294. Springer, Cham. https://doi.org/10.1007/978-3-031-05814-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-031-05814-1_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-05813-4
Online ISBN: 978-3-031-05814-1
eBook Packages: Computer ScienceComputer Science (R0)