Formal Design and Verification of Zone Controller

iCMTC is an advanced Communication Based Train Control system developed by CASCO Signal Ltd. For China´s mass transit transportation. Some subsystems of iCMTC has been applied in Shanghai Metro Line 10. Zone Controller (ZC) is one of the subsystems of iCMTC. Modeling and verifying ZC is challenging due to the complexity of the block system and the behavior itself. We propose a formal approach to gradually specify the block system and lower complexity of the verification of ZC behavior. In recent years, there are many researches on railway systems. However, these studies use simple track networks, which makes them inadequate in industrial practice. To address this problem, we define specific block layouts (i.e., Double slip connection) as relations on sets. We also define mathematical properties of the relations so that the block system can be precisely described. For the purpose of reducing the complexity of verification, we propose an improved refinement mechanism based on the Event-B notation. Based on this refinement mechanism, we develop a Rodin plug-in to help us refine the system. We use this mechanism in modeling the ZC behavior, and achieve good results in automated proof. Several safety properties are considered and verified to ensure the safety and correctness of ZC.