Research On The Method Of Formal Development Of The ATP System

Automatic Train Protection System is a subsystem of Communication Based TrainControl System which manage for the security of train running. The function of the ATPsystem with speed measurement, distance measure, overspeed protection, speed curve and soon. Therefore, the ATP system software development is very important. This is the guaranteeof the safe operation of the train. The current domestic research results of ATP system is notvery mature. However, systematic and network of ATP system is very high, and very largeand complex, so we need to use formal methods to establish the corresponding equipmentsystem model, then we can have better understanding and analysis to maximize the automatictrain protection system, and can eliminate the ambiguity of the software development,reducing the cost of software development. To ensure that the logic correctness andcompleteness of the ATP system.UML is an object-oriented development method which commonly used, the B method isa kind of formal development method. Combines B method and UML language can make upfor the inadequacy of UML language. The combining method also has more precise semanticand unambiguous. And B methods like traditional software development methods, can getinvolved in the system requirements analysis, design, in the end the whole process of thesystem function realization.The research object based on the ATP system, the main research is on the systemmodeling and validation. Select the UML static model class diagram and state diagram infigure, by adopting the method of B formal specification on UML class diagram and statediagram formalization. Using the abstract machine of B language to the class diagram andstate diagram, established a relationship of class diagram and state diagram to abstractmachine. Finally adopting the formal specification on UML class diagram and state diagramformalization to the ATP system of train interval control, door control, overspeed protectionfunctions. Use the proB as model validation tool, verifying the accuracy of ATP systemfunction model.This paper studies the formal modeling and its validation method, improved the ATPsystem modeling and validation method. Different with traditional modeling and verificationmethods can only simple to ATP system of a certain function, This method can be used to thewhole ATP system.According to the characteristics of the ATP system, Through the UML class diagram andstate diagram to formal B method code mapping relationship, formal method was applied tothe ATP system modeling and validation process, strengthen the security of ATP system modeling and validation. And proB don’t have to guess the correctness of the operationparameters, let the model validation results more accurate.