A Dedicated Algorithm for Verification of Interlocking Systems
A railway interlocking is the system ensuring a safe train traffic inside a station by monitoring and controlling signalling components. Modern interlockings are controlled by a generic software that uses data, called application data, reflecting the layout of the station under control and defining which actions the interlocking can perform. The safety of the train traffic relies thereby on application data correctness, errors inside them can lead to unexpected events, such as collisions or derailments. Automatising and improving the verification process of application data is an active field of research. Most of this research is based on model checking, which performs an exhaustive verification of the system but which suffers from scalability issues. In this paper, we propose to use our knowledge of the system in order to design a polynomial verification algorithm that can detect all the possible safety issues provided that an assumption of monotonicity hold.
This research is financed by the Walloon Region as part of the Logistics in Wallonia competitiveness pole.
- 1.Cribbens, A.: Solid-state interlocking (ssi): an integrated electronic signalling system for mainline railways. In: IEE Proceedings B (Electric Power Applications), vol. 134, pp. 148–158. IET (1987)Google Scholar
- 2.Theeg, G., Anders, E., Vlasenko, S.: Railway Signalling & Interlocking: International Compendium. Eurailpress, Hamburg (2009)Google Scholar
- 3.Cenelec, E.: 50128. Railway Applications-Communication, Signaling and Processing Systems-Software for Railway Control and Protection Systems (2011)Google Scholar
- 4.Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modeling and verification of interlocking systems featuring sequential release. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2014. CCIS, vol. 476, pp. 223–238. Springer, Heidelberg (2015)Google Scholar
- 5.Winter, K.: Model checking railway interlocking systems. Aust. Comput. Sci. Commun. 24, 303–310 (2002)Google Scholar
- 9.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, pp. 101–107. Australian Computer Society, Inc. (2006)Google Scholar
- 11.Cappart, Q., Limbrée, C., Schaus, P., Legay, A.: Verification by discrete simulation of interlocking systems. In: 29th Annual European Simulation and Modelling Conference 2015, ESM 2015, pp. 402–409 (2015)Google Scholar
- 12.Limbree, C., Cappart, Q., Pecheur, C., Tonetta, S.: Verification of interlocking systems using statistical model checking. arXiv preprint arXiv:1605.06245 (2016)
- 13.Busard, S., Cappart, Q., Limbrée, C., Pecheur, C., Schaus, P.: Verification of railway interlocking systems. In: Proceedings 4th International Workshop on Engineering Safety and Security Systems, ESSS, pp. 19–31 (2015)Google Scholar
- 14.Anunchai, S.: Verification of railway interlocking tables using coloured pertri nets. In: Proceedings of the 10th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools (2009)Google Scholar
- 16.Cappart, Q., Limbrée, C., Schaus, P., Quilbeuf, J., Traonouez, L.M., Legay, A.: Verification of interlocking systems using statistical model checking. arXiv preprint arXiv:1605.02529 (2016)