Movement authority security modeling and verification based on fault statechart

2019 2nd International Conference on Advanced Materials, Intelligent Manufacturing and Automation

Yu, Fan^1 ; Tang, Minan^1 ; Hao, Binbin^1 ; Wang, Qianqian^1

School of Automation and Electrical Engineering, Lanzhou Jiaotong University, Lanzhou, Gansu

730070, China^1

关键词: Analysis and verifications;    Communication-based train control systems;    Development trends;    Movement authorities;    Normal operations;    Safety critical systems;    Security modeling and verification;    Train control systems;   

Others  :  https://iopscience.iop.org/article/10.1088/1757-899X/569/4/042056/pdf
DOI  :  10.1088/1757-899X/569/4/042056

来源: IOP

【 摘 要 】

Communication Based Train Control System (CBTC) has become the development trend of train control system, and generating safe and reasonable movement authority is the key to ensure the normal operation of the whole system. Combined with the security of the system, a security analysis method based on fault tree information to construct fault Statechart is proposed. The fault tree that generates the abnormality of the movement authority is analyzed, and it is represented as a form that the Statechart can describe, thereby establishing a fault statechart of the movement authority generating abnormality. Finally, the formal modeling of the fault statechart is carried out by using the time automaton theory, and the fault state unreachable is taken as the attribute of the specification for inspection. The results show that the method of combining fault Statechart and time automata proposed in the paper is feasible and suitable for the analysis and verification of safety critical systems.