Modeling And Verification Of Movement Authority Module Of RBC System Based On Safe State Machine

At present, Chinese Railway has entered a period of great development. With the rapid development the computer technology, the Ministry of Railways proposed Chinese Train Control System (CTCS) which consists of five application levels, from level 0 to level 4 and is very suit for our national conditions. Currently the CTCS-3 system based on GSM-R wireless communications is under research, which can greatly enhance the safety of train operation and efficiency of railway transportation. The Radio Block Center (in short RBC) is the core ground equipment of the CTCS-3 system, which makes the on board equipment control the train safely by calculating and sending Movement Authority (in short MA) to the on board. So it is very important for the researchers to design reasonable arithmetic of MA.This master thesis focuses on the algorithm, the functional requirements and the realization of MA. The algorithm of MA is divided into many modules for easier modeling and understanding. This thesis also analyzes and designs MA model based on Safe State Machine (S.S.M.) and verifies the MA model by using UPPAAL tool. The main work accomplished in this thesis is listed as follows:Firstly, this master thesis begins with the study of functions and interfaces of RBC, then analyzes and designs the basic meaning, the functional requirements and the algorithm of MA. The thesis completes the delineation of functional modules based on the functional requirements of MA including calculating MA in the Full Supervision, in the scene of Level Conversion, in the scene of handover of adjacent RBC and the scene of containing the temporary speed information mode, it also analyzes and designs the realization of all functional modules.Secondly, MA is divided into five modules based on the algorithm of MA, including Compute Train Path module, Train Location module, Updating Path module, MA Calculation module, and MA Sending module, and the five functional modules mentioned above are realized in the MA Calculation module and describe the process of MA Calculation in detail. This thesis designs MA model based on Safe State Machine for the five modules, and it realizes the logic function of the modules with the Preemption structure, the Hierarchy structure and the Concurrency structure, which are the three key characters of the S.S.M., and combining the state abstracting and the control of the condition transfer. Finally, this thesis simulates the Safe State Machine model, designs MA model and Verifies the MA model by using UPPAAL, which provides the theoretical basis for MA Application Software Design.The innovation of this thesis lies in proposing the algorithm of MA and the modeling, analyzing and verification of Movement Authority module of RBC system with Safe State Machine and providing design proposals for MA. The model has friendly interface and is feasible. So it may be meaningful for us to develop a way modeling and verification for the whole RBC system, which would provide the powerful basis for the design of system.