Formal Analysis for Automatic Train Operation System and Research on Diagnosis of Anomalies

摘要

The Chinese Train Control System (CTCS) with Automatic Train Operation (ATO) Function transmits the information through corresponding transmission channel to ensure the safety of the train operation. It is necessary to analyze the consistency of specification and implementation in information exchanges to promote the efficiency of subsequent maintenance. The formal method of communication sequence process (CSP) is selected according to the specification, and the time series of the test data are mapped to IOTS (Input-Output Transition System). The system-level fault diagnosis method is applied to the diagnosis of abnormal conditions in the information interaction. Finally, the state of the equipment is figured out based on test information quantitatively.