Abstract
Railway signalling is a complex and safety critical problem that has been extensively studied and standardised over a long period of time. The signalling equipment is typically procured from standard vendors and configured with yard specific application logic for which the route control chart (RCC) is a key input. As the yard size increases, the number of routes also increases and accordingly the difficulty of RCC preparation increases rapidly. RCC preparation for big yards may take months and affects the project deadlines adversely. In this work we report computational procedures to address: <inline-formula> <tex-math notation="LaTeX">a </tex-math></inline-formula>) capturing of signal interlocking plan (SIP) given on paper and storing it using suitable data structures, <inline-formula> <tex-math notation="LaTeX">b </tex-math></inline-formula>) generating the RCC automatically from the captured SIP supported by procedures based on graph theoretic formulation, <inline-formula> <tex-math notation="LaTeX">c </tex-math></inline-formula>) storing the SIP graphically in memory, <inline-formula> <tex-math notation="LaTeX">d </tex-math></inline-formula>) application of formal methods towards validation of yard structure and <inline-formula> <tex-math notation="LaTeX">e </tex-math></inline-formula>) generation of temporal logic properties for formal verification of electronic interlocking (EI) logic. Several important steps towards RCC generation, such as conflict identification and isolation determination and also validation and verification (V&V) covering yard layout and safety property generation based on graph theoretic modelling are the most interesting aspect of this work. The described techniques have been tested successfully on many actual yards.