Refinement And Verification Of Trackside Systems

Communication based train control (CBTC) is the newest railway system. CBTC has the advantages of short railway interval, high rail capacity, and smooth operation, largely enhancing transportation capacity of city. To face up with more and more serious traffic problems in metropolitans, the construction of CBTC based railway systems has speeded up in China. One of subsystems of CBTC is the Trackside System, which should be assured of the highest safety requirement. Once the trackside system fails, it may cause serious consequences, such as train collision or derailing. Compared to traditional railway systems, CBTC based trackside system is designed with more complicated physical environment and system behavior. As a result, verifying large systems such as trackside systems can easily incur state explosion problem. It is obvious that traditional modeling process is unable to model and verify large systems since it cannot provide a solution to lower the complexity of the model. Therefore, we must consider how to decrease the complexity of the model, how to divide state transitions, and how to reduce state space, before we can go ahead to model and verify trackside system. Meanwhile, we should also ensure that the reduced model should be consistent with the original one. Besides, we should also define certain laws and prove some theorems to make sure that the reduced model can be further verified in the deduction system of formal methods.In the domain of railway signal systems, the Event-B method and Safety-critical application development environment (SCADE) are the main stream formal methods. Both methods have bright futures in industries. The modeling of a large system containing many state transitions is not possible to be done in one shot. Through refinement of Event-B, we may gradually introduce the state variables and strengthen the guards of events so as to make the mathematical model closed to the real system behaviors. Meanwhile, the correctness of the mathematical models of different refinement levels are assured of data consistency by proof obligations. Event-B offers modeling of a large system at a system level while ensure that the model satisfies safety requirements. While SCADE provides a thorough software development process including modeling, simulation, verification and code auto-generation. The SCADE driven development process ensure the system safety and maintainability of software.In this paper, we propose the partition paradigm modeling based on the Event-B refinement. Using this method, we can lower the complexity of the mathematical model so that the model can be proved with simplified state space. Firstly, we define the semantics, graphical representation and deduction laws of the paradigm. Then, we validate the proof obligations of the reduced model so as to ensure its consistency with the original model. Upon this modeling method, we propose a modeling process, from refinement, partition, to decomposition, towards a large system. Also, based on Rodin, the Event-B modeling platform, we realized this method as a Rodin plug-in.To divide the state space of the SCADE model, we also propose slicing criteria tailored for the SCADE models. We first define the semantics of criteria using LUSTRE language, the dataflow based on clock and the mathematical equations. In this work, the slicing criteria that the SCADE process must conduct in order to simplify the complexity of SCADE models are stated.Finally, we propose a modeling and verification process for CBTC based Trackside System. Through the splitting modeling method and its Rodin based implementation, we are able to split the Event-B models into sub models with low cohesion. As a result, we succeed in verifying all the safety properties stated in the trackside systems. While in the software development process of the trackside system, we choose SCADE driven software development. Using SCADE operators, we formalize the physical environment and the movement authority calculation. To avoid state explosion problem, we apply the slicing criteria to divide the state space of the model. Consequently, we complete the automatic proof of SCADE models.