Generation And Formal Verification Of Radio Block Center Data Streams Based On STATEMATE

China Train Control System level 3(CTCS-3) is a Communication-Based Train Control system.It is an important component of China Train Control System(CTCS).It is on behalf of the advanced level in the existing train control technology.Radio Block Center(RBC) is the key equipment of the trackside sub-system in CTCS-3.RBC Database is an important part of RBC.It is responsible for the management of data,which is received from external equipments in the whole process of train control.The purpose of generating RBC Data streams is sorting out the data stored in RBC database into whatever format RBC application layer(the other application modules of RBC) needs,provide the necessary data support for RBC to compute Movement Authority(MA).By this token,the generation of RBC data streams plays a very crucial role in ensuring that the trains which are within the jurisdiction of the RBC can run safely.Therefore,the study of the generation of RBC data streams has great practical significance.Firstly,according to the specified function which RBC should realize in the main railway operation scenes of CTCS-3,the thesis makes a concrete analysis of functional requirement of RBC Database in every operation scene.This paper begins to design RBC Database with the functional requirement of RBC Database,and normalizes the design to improve the performance of RBC Database,on the premise of achieving functional.The formal methods have the advantage of reducing design errors and improving system reliability.In view of these characteristics,this paper choses modeling based on formal methods as research method.Statemate enables engineers to rapidly design and validate complex reactive systems through a unique combination of graphic modeling, simulation,code generation,documentation generation,and test plan definition.As a result,the thesis choses Statemate as research platform to design the applications of RBC Database and models the design for ensuring that the design of RBC data streams match with the functional requirement.State chart is one of the core modeling languages in Statemate.So this paper each establishes state transition models of the applications of RBC data streams with state chart,in three railway operation scenes which are "login and starting","RBC handing over" and "computing MA".These models show the process that RBC application layer calls RBC data streams to realize the functional of train control.The paper uses the simulation tool and check model tool within Statemate to make accurate simulation and rigorous validation for these models of RBC data streams.In this way,the thesis effectively eliminates the existing contradictions and the ambiguity in the system original design,ensures that the design of RBC Database meets funcational requirements and security requirement also.These conclusions provid the theoretical basis for the design of RBC data streams.