Advertisement

Application of Coloured Petri Nets in Modelling and Simulating a Railway Signalling System

  • Somsak Vanit-AnunchaiEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9933)

Abstract

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.

Keywords

Interlocking tables Route-based interlocking Approach lock Back lock Visualization extension 

Notes

Acknowledgments

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.

References

  1. 1.
    Basten, T., Bol, R., Voorhoeve, M.: Simulating and analyzing railway interlockings in ExSpec. IEEE Parallel Distrib. Technol. Syst. Appl. 3(3), 50–62 (1995)CrossRefGoogle Scholar
  2. 2.
  3. 3.
    Clavel, M., et al.: Maude Manual. http://maude.cs.uiuc.edu/
  4. 4.
    Fantechi, A.: Distributing the challenge of model checking interlocking control tables. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 276–289. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  5. 5.
    Fantechi, A.: Twenty-five years of formal methods and railways: what next? In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 167–183. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  6. 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. 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
  8. 8.
    Hagalisletto, A.M., Bjørk, J., Yu, I.C., Enger, P.: Constructing and refining large-scale railway models represented by Petri nets. IEEE Trans. Syst. Man Cybern. Part C 37(4), 444–460 (2007)CrossRefGoogle Scholar
  9. 9.
    Haxthausen, A.E., Peleska, J., Pinger, R.: Applied bounded model checking for interlocking system designs. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 205–220. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  10. 10.
    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, Heidelberg (2016). doi: 10.1007/978-3-319-33951-1_12 CrossRefGoogle Scholar
  11. 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
  12. 12.
    James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S.A., Treharne, H.: On modelling and verifying railway interlockings: tracking train lengths. Sci. Comput. Program. 96, 315–336 (2014)CrossRefGoogle Scholar
  13. 13.
    James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S.A., Treharne, H.: Techniques for modelling and verifying railway interlockings. STTT 16(6), 685–711 (2014)CrossRefGoogle Scholar
  14. 14.
    Jensen, K., Kristensen, L.M.: Colored Petri nets: a graphical language for formal modeling and validation of concurrent systems. Commun. ACM 58(6), 61–70 (2015)CrossRefGoogle Scholar
  15. 15.
    Jensen, K., Kristensen, L.M.: Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer, Heidelberg (2009)CrossRefzbMATHGoogle Scholar
  16. 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. 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
  18. 18.
    Vanit-Anunchai, S.: Modelling railway interlocking tables using coloured Petri nets. In: Clarke, D., Agha, G. (eds.) COORDINATION 2010. LNCS, vol. 6116, pp. 137–151. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  19. 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
  20. 20.
    Winter, K.: Optimising ordering strategies for symbolic model checking of railway interlockings. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 246–260. Springer, Heidelberg (2012)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  1. 1.School of Telecommunication Engineering, Institute of EngineeringSuranaree University of TechnologyNakhon RatchasimaThailand

Personalised recommendations