IIT KGP develops safer tool for railway interlocking

Railway Interlocking is a critical signalling system that prevents trains from conflicting movements through only allowing trains to receive authority to proceed, when routes have been set, lock and detected in safe combinations. Indian railways is moving towards Electronic interlocking which has much higher availability, reliability and safety. However, the configuration of an electronic interlocking (EI) equipment is a highly safety critical task. The executive software of the electronic interlocking equipment interprets the yard specific application logic while asserting the signal aspects. The application logic for a yard is typically developed by third-party vendors and rigorously tested, however errors in the application logic have been detected in commissioned electronic interlocking equipment – some leading to near catastrophic consequences. Formal verification methods, which can mathematically prove the conformance of the application logic with respect to yard specific safety properties, is being studied by railways around the world, under the larger mandate of using formal methods in the EN50128 railway safety standards.
Researchers in the Computer Science & Engineering Department have leveraged analytical tools used for verification of VLSI circuits to develop formal verification logic for railway interlocking systems. The goal of this project is to develop a tool flow for formally proving the safety of the application logic for a given yard. “Since errors in the application logic of interlocking systems may have catastrophic consequences, this development has significant potential for improving railway safety. In the proposed approach the yard layout is used as a reference for automatically generating a list of safety properties, which are then proven on the application logic using back end model checking tools. The generation of the formal properties is specifically tailored to the combination of relays used in that yard. It has already been successfully tested in several Railway Yards” said Prof. Pallab Dasgupta, lead researcher of the project. 
The tool suite is developed at IIT Kharagpur in collaboration with Research, Designs & Standards Organization (RDSO) and Service Improvement Group (SIG) Indian Railway. The tool flow has been tested on several railway yards. This project has the potential to be further extended to study and develop optimum traffic operation plans, alternative plans for emergencies.
Indian Railways operates one of the largest railway networks in the world. Given current forecasts about the rate of growth of the Indian economy, freight and passenger traffic is expected to grow at the rate of 10% per year. The Railways has long term vision plan, to make major improvements in the quality of the services it provides its customers, implement improved safety standards, reduce operating costs and ensure efficient utilization of available assets and infrastructure. To achieve these objectives, the Indian Railways, through RDSO has awarded 12 research projects to IIT Kharagpur’s Centre for Railway Research in the area of analysis and design of rolling stock, infrastructure, operations and maintenance. Several of the products and technologies are being field tested at various facilities of Indian Railways apart from lab testing at IIT Kharagpur. The next step would be to further develop the products and technologies with an industrial partner for production.