Abstract
Interlocking tables are the functional specification defining the routes, on which the passage of the train is allowed. Associated with the route, the states and actions of all related signalling equipment are also specified. This paper formally models the interlocking tables using Coloured Petri Nets (CPN). The CPN model comprises two parts: Signaling Layout and Interlocking Control. The Signaling Layout part is used to simulate the passage of the train. It stores geographic information of the signalling layout in tokens. The Interlocking Control part models actions of the controller according to the functions specified in the interlocking tables. The arc inscriptions in the model represent the content of the interlocking tables. Following our modelling approach we can reuse the same CPN net structure to model any new or modified interlocking system regardless of its size. Experimental results are presented to provide increased confidence in the model correctness.
Supported by National Research Council of Thailand Grant no. PorKor/2551-153.
Chapter PDF
Similar content being viewed by others
References
Basten, T., Bol, R., Voorhoeve, M.: Simulating and Analyzing Railway Interlockings in ExSpec. IEEE Parallel and Distributed Technology, Systems and Applications 3(3), 50–62 (1995)
Chevilat, C., Carrington, D., Strooper, P., Süß, J.G., Wildman, L.: Model-Based Generation of Interlocking Controller Software from Control Tables. In: Schieferdecker, I., Hartman, A. (eds.) ECMDA-FA 2008. LNCS, vol. 5095, pp. 349–360. Springer, Heidelberg (2008)
Cimatti, A., Clarke, E.E., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Durmus, M.S., Soylemez, M.T.: Railway Signalization and Interlocking Design via Automation Petri Nets. In: Proceedings of the 7th Asian Control Conference, Hong Kong, August 27-29, 2009, pp. 1558–1563 (2009)
Fokkink, W.J., Hollingshead, P.R.: Verification of Interlockings: from Control Tables to Ladder Logic Diagrams. In: Proceedings of the 3rd Workshop on Formal Methods for Industrial Critical Systems (FMICS 1998), Amsterdam, May 1998, pp. 171–185. Stichting Mathematisch Centrum (1998)
Hagalisletto, A.M., Bjørk, J., Yu, I.C., Enger, P.: Constructing and Refining Large-Scale Railway Models Represented by Petri Nets. IEEE Transactions on Systems, Man, and Cybernetics, Part C 37(4), 444–460 (2007)
Hansen, K.M.: Formalizing Railway Interlocking Systems. In: Nordic Seminar on Dependable Computing Systems, Department of Computer Science, Technical University of Denmark, pp. 83–94 (1994)
Janczura, C.W.: Modelling and Analysis of Railway Network Control Logic using Coloured Petri Nets. PhD thesis, School of Mathematics and Institute for Telecommunications Research, University of South Australia, Adelaide, Australia (August 1998)
Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems. International Journal on Software Tools for Technology Transfer 9(3-4), 213–254 (2007)
Svendsen, A., Olsen, G.K., Endresen, J., Moen, T., Carlson, E., Alme, K., Haugen, Ø.: The Future of Train Signaling. In: Czarnecki, K., Ober, I., Bruel, J.-M., Uhl, A., Völter, M. (eds.) MODELS 2008. LNCS, vol. 5301, pp. 128–142. Springer, Heidelberg (2008)
van der Aalst, W.M.P., Odijk, M.A.: Analysis of Railway Stations by Means of Interval Timed Coloured Petri Nets. Real-Time Systems 9(3), 1–23 (1995)
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, Department of Computer Science, University of Aarhus, October 19-21, pp. 139–158 (2009)
Winter, K.: Model Checking Railway Interlocking Systems. In: Oudshoorn, M. (ed.) Proceeding of the 25th Australasian Computer Science Conference (ACSC 2002), Melbourne, Australia, vol. 4, pp. 303–310. Australian Computer Society (2002)
Winter, K., Johnston, W., Robinson, P., Strooper, P., van den Berg, L.: Tool Support for Checking Railway Interlocking Designs. In: Cant, T. (ed.) Proceeding of the 10th Australian Workshop on Safety Related Programmable Systems (SCS 2005), Sydney, Australia, vol. 55, pp. 101–107. Australian Computer Society (2005)
Winter, K., Robinson, N.: Modelling Large Railway Interlockings and Model Checking Small Ones. In: Oudshoorn, M. (ed.) Proceeding of the 26th Australasian Cumputer Science Conference (ACSC 2003), Adelaide, Australia, vol. 16, pp. 309–316. Australian Computer Society (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vanit-Anunchai, S. (2010). Modelling Railway Interlocking Tables Using Coloured Petri Nets. In: Clarke, D., Agha, G. (eds) Coordination Models and Languages. COORDINATION 2010. Lecture Notes in Computer Science, vol 6116. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13414-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-13414-2_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13413-5
Online ISBN: 978-3-642-13414-2
eBook Packages: Computer ScienceComputer Science (R0)