KEYWORDS: Transponders, Systems modeling, Telecommunications, Control systems, Visual process modeling, Data communications, Logic, General packet radio service, Computer programming, Safety
Formal methods are used to improve the credibility and correctness of scenarios in Chinese Train Control Systems (CTCS). At present, there are few formal studies on the high-speed Automatic Train Operation system that developed from CTCS-3 level high-speed railway technology. In this paper, we adopt a new formal method, Alvis, which combines the advantages of high-level programming language and graphical modeling and select the interzone TSRS handover scene in high-speed railway ATO system as the research object. The messaging behaviors of the scene are analyzed using UML sequence diagrams, and an Alvis model of the system is built, which is converted into an smv model supporting the formal validation of the model checking tool nuXmv. The real-time performance of the extracted messaging was verified on demand, inconsistency between technical specifications and actual operational scenarios was identified and solution was provided. The results of this method can provide some reference for the technical promotion of ATO train control system in China.
Access to the requested content is limited to institutions that have purchased or subscribe to SPIE eBooks.
You are receiving this notice because your organization may not have SPIE eBooks access.*
*Shibboleth/Open Athens users─please
sign in
to access your institution's subscriptions.
To obtain this item, you may purchase the complete book in print or electronic format on
SPIE.org.
INSTITUTIONAL Select your institution to access the SPIE Digital Library.
PERSONAL Sign in with your SPIE account to access your personal subscriptions or to use specific features such as save to my library, sign up for alerts, save searches, etc.