Executive Summary : | The fixed block signaling infrastructure in Indian railways (IR) is a significant performance bottleneck in terms of line capacity and safety. However, the communication-based train control (CBTC) system with Moving block signaling enhances these capabilities. The IR vision 2020 report suggests that CBTC systems are needed to improve operational performance and meet public requirements. Implementing CBTC in heterogeneous scenarios, such as mixed traffic, is challenging. A CBTC system is safety critical, and systematically assessing its functional components is necessary to identify risks and hazards. The health of a CBTC system depends on the proper functioning of its software components and cooperative communication among them. The EN50128 signaling safety standards recommend the use of formal methods for this purpose. A CBTC system with Moving block signaling consists of three systems: automatic train protection (ATP), automatic train operation (ATO), and automatic train supervision (ATS). ATP functions provide guaranteed protection against train collisions, overspeed, grade crossing accidents, and other hazardous conditions. This proposal focuses on the development of a Moving block signaling-based ATP system for IR. The structural design will be detailed using a standard system design methodology, with functional safety assessed to ensure compliance with CENELEC EN50126 safety requirements. The structural design will be modeled using a formal modeling technique to check design correctness and verify errors and anomalous properties. The formal model will be validated through simulation in various run-time scenarios to ensure it meets the expected behavior of the ATP system. |