Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Automated Verification of Critical Systems

International Workshop on Formal Methods for Industrial Critical Systems

AVoCS 2016, FMICS 2016: Critical Systems: Formal Methods and Automated Verification pp 214–230Cite as

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

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,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.

This work is supported by the National Science and Technology Development Agency and National Research Council of Thailand.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    No conflicted route can be used at the same time by multiple trains.

  2. 2.

    Visualization Extension v.0.9 Developed By M. Westergaard and M. Assiri.

  3. 3.

    The track circuit in front of the (approaching) home or starter signal.

References

  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)

    Article  Google Scholar 

  2. CPN Tools. http://cpntools.org

  3. Clavel, M., et al.: Maude Manual. http://maude.cs.uiuc.edu/

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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 

  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)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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

    Chapter  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 

  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)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  15. Jensen, K., Kristensen, L.M.: Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer, Heidelberg (2009)

    Book  MATH  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 2015

    Google 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 

  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)

    Chapter  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 

  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)

    Chapter  Google Scholar 

Download references

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.

Author information

Authors and Affiliations

  1. School of Telecommunication Engineering, Institute of Engineering, Suranaree University of Technology, Muang, Nakhon Ratchasima, Thailand

    Somsak Vanit-Anunchai

Authors
  1. Somsak Vanit-Anunchai
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Somsak Vanit-Anunchai .

Editor information

Editors and Affiliations

  1. ISTI-CNR , Pisa, Italy

    Maurice H. ter Beek

  2. ISTI-CNR , Pisa, Italy

    Stefania Gnesi

  3. Universität Augsburg, Augsburg, Germany

    Alexander Knapp

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Vanit-Anunchai, S. (2016). Application of Coloured Petri Nets in Modelling and Simulating a Railway Signalling System. In: ter Beek, M., Gnesi, S., Knapp, A. (eds) Critical Systems: Formal Methods and Automated Verification. AVoCS FMICS 2016 2016. Lecture Notes in Computer Science(), vol 9933. Springer, Cham. https://doi.org/10.1007/978-3-319-45943-1_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-45943-1_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-45942-4

  • Online ISBN: 978-3-319-45943-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation