A Dedicated Algorithm for Verification of Interlocking Systems

  • Quentin CappartEmail author
  • Pierre Schaus
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9922)


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. 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. 2.
    Theeg, G., Anders, E., Vlasenko, S.: Railway Signalling & Interlocking: International Compendium. Eurailpress, Hamburg (2009)Google Scholar
  3. 3.
    Cenelec, E.: 50128. Railway Applications-Communication, Signaling and Processing Systems-Software for Railway Control and Protection Systems (2011)Google Scholar
  4. 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. 5.
    Winter, K.: Model checking railway interlocking systems. Aust. Comput. Sci. Commun. 24, 303–310 (2002)Google Scholar
  6. 6.
    Eisner, C.: Using symbolic model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 99–109. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  7. 7.
    Huber, M., King, S.: Towards an integrated model checker for railway signalling data. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 204–223. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    Clarke, E.M., Klieber, W., Nováček, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1–30. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  9. 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
  10. 10.
    Winter, K.: Optimising ordering strategies for symbolic model checking of railway interlockings. In: Steffen, B., Margaria, T. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 246–260. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  11. 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. 12.
    Limbree, C., Cappart, Q., Pecheur, C., Tonetta, S.: Verification of interlocking systems using statistical model checking. arXiv preprint arXiv:1605.06245 (2016)
  13. 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. 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
  15. 15.
    Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Defining and model checking abstractions of complex railway models using CSP\(||\)B. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, vol. 7857, pp. 193–208. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  16. 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)

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Université catholique de LouvainLouvain-La-NeuveBelgium

Personalised recommendations