Movement authority security modeling and verification based on fault statechart

Abstract

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.