Abstract

A “control table” is a functional specification of the signaling system of a railway section. It specifies the routes on which trains are allowed to pass. Control table for interlocking system in Indian Railways is done by a vendor. This control table is verified for correctness by another vendor. The process followed to generate this control table remains a black box, i.e., unknown. Through this paper, a working system has been proposed to explore this unknown process and come up with correct control table entries for a given layout of railway section.

References

• Dines Bjørner. Train: The railway domain - A ”grand challenge” for computing science & transportation engineering. In Building the Information Society, IFIP 18th World Computer Congress, Topical Sessions, 22-27 August 2004, Toulouse, France, pages 607–611, 2004.
• Egon Börger and Robert F. Stärk. Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, 2003.
• Stephen D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. J. ACM, 31(3):560–599, 1984.
• Giuseppe Del Castillo and Kirsten Winter. Model checking support for the ASM high-level language. In Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings, pages 331–346, 2000.
• E. Allen Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pages 995–1072. 1990.
• Thomas Gibson-Robinson, Philip J. Armstrong, Alexandre Boulgakov, and A. W. Roscoe. FDR3 - A modern refinement checker for CSP. In Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, pages 187–201, 2014.
• Tomas Hlavaty, Libor Preucil, and Petr Stepan. Case study: Formal specification and verification of railway interlocking system. In 27th EUROMICRO Conference 2001: A Net Odyssey, 4-6 September 2001, Warsaw, Poland, pages 258–263, 2001.
• Karim Kanso, Faron Moller, and Anton Setzer. Automated verification of signalling principles in railway interlocking systems. Electr. Notes Theor. Comput. Sci., 250(2):19–31, 2009.
• Ahmad Mirabadi and Mohammad Bemani Yazdi. Automatic generation and verification of railway interlocking control tables using fsm and nusmv. In Engineering Modelling 21 (2008) 1-4, pages 57–63, 2008.
• Mehmet T. Sylemez, Mustafa S. Durmu, Uur Yldrm, Serhat Trk, and Arcan Sonat. The application of automation theory to railway signalization systems: The case of turkish national railway signalization project. In 18th IFAC World Congress, 2011, Italy, pages 10752–10757, 2011.
• Somsak Vanit-Anunchai. Experience using coloured petri nets to model railway interlocking tables. In Proceedings 2nd French Singaporean Workshop on Formal Methods and Applications, FSFMA 2014, Singapore, 13th May 2014., pages 17–28, 2014.
• K. Winter. Model checking railway interlocking systems. In Computer Science 2002, Twenty-Fifth Australasian Computer Science Conference (ACSC2002), Monash University, Melbourne, Victoria, January/February 2002, pages 303–310, 2002.
• KirstenWinter and Neil J. Robinson. Modelling large railway interlockings and model checking small ones. In Computer Science 2003, Twenty-Sixth Australasian Computer Science Conference (ACSC2003), Adelaide, South Australia, February 2003, pages 309–316, 2003.