Font Size: a A A

Research Of Analysis Method In RBC Based On Model Checking

Posted on:2015-02-17Degree:MasterType:Thesis
Country:ChinaCandidate:H F SongFull Text:PDF
GTID:2252330425488844Subject:Traffic Information Engineering & Control
Abstract/Summary:PDF Full Text Request
CTCS-3level train control system is based on GSM-R wireless communications system to realize the message dual-direction transmission between the vehicle and ground, radio block center (RBC) generates Movement Authority, balise in charge of locateing the train’s position, train track circuit realizes the occupied examines, and the CTCS-3level train control system involved CTCS-2level train control system function at the same time.Considering the complex and high security requirement of the train control system, it is almost impossible to do test research work in the real operation environment, even if it is available to achieve, which will also bring with a considerable cost. With the assistance of computer, we can simulate the of CTCS-3on-board equipment interconnection and interoperability test platform, with the simulation, we can control both the design of the system and device integration which provide a good test platform for the secondary design, research and development, and validation.The RBC subsystem is a main part of the CTCS-3level on-board equipment interconnection and interoperability test platform, and it plays a decisive role in the entire controlling process, this paper is started with RBC, building the system model, analyzing the system security, realizing automatically test at the same time, as a result, we can get a more viable way to improve the entire test platform in theoretical approaches and practical applications.This paper traces the causes abnormal condition in the process of testing, for example, deeply analyzes the RBC subsystem test analysis method based on model test. Begin from formal modeling method such as the breakthrough point, to find out the ways to reflect the RBC subsystem behavior, this article use UPPAAL modeling tools for RBC subsystem of car flow timed automata model, adopt the method of model test of the accessibility analysis of the proposed model, and finally the whole test platform alignment league test, demonstrate the feasibility of the proposed method has a certain, for the future to further improve and contribute to a certain test platform.
Keywords/Search Tags:Model checking, CTCS-3level train control system, Reachableanalysis, Formal modeling, Radio Block Center sub-system, Test analysis
PDF Full Text Request
Related items