•  
  •  
 

Journal of System Simulation

Abstract

Abstract: The C3+ATO system is in the experimental stage in our country and has the characteristics of high automation degree and high safety requirement at present. In order to confirm whether the specific function of the high-speed railway C3+ATO system meets the corresponding technical specification under the specific scene, a formal modeling and verification method based on the timed automata is proposed. The station automatic departure scene is selected as the modeling object. The functional requirements of C3+ATO system specification are extracted and the timed automata model of the scene is established. The message sequence chart of the corresponding process is generated, and the functional attributes of the system are verified and the model is simulated at the C3+ATO train control simulation platform. The simulation results show that the model meets the security function attributes and restricted activity attributes of the system technical specification, and can provide theoretical reference for the system design, practical application and improvement of related specifications.

First Page

951

Revised Date

2020-05-29

Last Page

961

CLC

TP391.9

Recommended Citation

Zhang Zhenhai, Yao Jie. Modeling and Verification of Scene of C3+ATO System Based on Timed Automata[J]. Journal of System Simulation, 2021, 33(4): 951-961.

DOI

10.16182/j.issn1004731x.joss.19-0662

Download

Share

COinS