Application of Coloured Petri Nets in Modelling and Simulating a Railway Signalling System
Formal validation of railway signalling systems normally involves three processes: creating models; simulation; and verifying the models’ dynamic behavior against the specified properties. It is well-known that the third process often encounters the problem of state explosion. To achieve fully automated formal validation, researchers usually abstract away details of operating procedures and concentrate on route interlocking that prevents train collision and derailment. Thus we encounter a dilemma between fully automated validation of an incomplete model or partial, semi-automated validation of a complete model. We argue that formally modelling the complete model will be more valuable for the on-going projects of the State Railway of Thailand because they provide insights and can be used to train new signal engineers. This paper focuses on the complete Coloured Petri Net (CPN) model of a typical Thai railway signalling system: a double-line station with one passing loop. The CPN model has included train movements that can be simulated and graphically visualized. In particular we illustrate how the CPN diagrams capture nine properties: Route interlocking, Flank protection, Approach signal release, Aspect sequence, Approach lock, Back lock, Alternative overlap, Sectional route release and Quick route release. Lessons learnt from using CPN Tools to model and validate the railway signalling systems are also discussed.
KeywordsInterlocking tables Route-based interlocking Approach lock Back lock Visualization extension
This work is supported by Research Grant from the National Science and Technology Development Agency and National Research Council of Thailand. The author is thankful to anonymous reviewers and Dr. Guy E. Gallasch. Their constructive feedback has helped the author improve the quality of this paper. The author is also grateful to his colleagues from the State Railway of Thailand, Patama Sridaranop, Anan Phonimdang, Sommart Klinsukol, Ittipon Kansiri, Kittisak Siripen, Surapol eiamsaart and Navaporn Rittisuk.
- 2.CPN Tools. http://cpntools.org
- 3.Clavel, M., et al.: Maude Manual. http://maude.cs.uiuc.edu/
- 6.Fantechi, A., Fokkink, W., Morzenti, A.: Some trends in formal methods applications to railway signaling. In: Formal Methods for Industrial Critical Systems: A Survey of Applications, pp. 61–84 (2012)Google Scholar
- 7.Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) FORMS/FORMAT - Formal Methods for Automation and Safety in Railway and Automotive Systems, pp. 107–115. Springer, Heidelberg (2010)Google Scholar
- 11.Hong, L.V., Haxthausen, A.E., Peleska, J.: Formal modeling and verification of interlocking systems featuring sequential release. In: Artho, C., Olveczky, P.C. (eds.) FTSCS 2014. Communications in Computer and Information Science, vol. 476, pp. 223–238. Springer, Heidelberg (2014)Google Scholar
- 16.Sun, P.: Model based system engineering for safety of railway critical systems. Ph.D. thesis, Université Lille Nord de France, France, July 2015Google Scholar
- 17.Vanit-Anunchai, S.: Verification of railway interlocking tables using coloured Petri nets. In: The Tenth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, DAIMI PB 590, pp. 139–158. Department of Computer Science, University of Aarhus (2009)Google Scholar
- 19.Vanit-Anunchai, S.: Experience using coloured Petri nets to model railway interlocking tables. In: Proceedings 2nd French Singaporean Workshop on Formal Methods and Applications, FSFMA 2014, Singapore, 13 May 2014, pp. 17–28 (2014)Google Scholar