Verification Method Of ZC Subsystem Safety Based On Hybrid Automata

In recent years, with the acceleration of urbanization process, urban rail transportation has become the preferred scheme of city traffic, In order to ease traffic congestion phenomenon. Communication based train control system (CBTC) is our urban rail traffic control system, combined with communication technology, computer technology and automatic control technology. As a safety critical system and complex system, verify the nature of the system meets the design requirements, and search for potential safety hazard is an important work, At this stage for system safety analysis verify the main use of classic security fault tree analysis method, and based on the formal model system security verification. This article from the perspective of CBTC system hybrid feature, use linear hybrid automata model to modeling the system function, verify the system meets the design requirements and driving safety.Starting from the analysis of CBTC system structure and features, summed up the real-time feature, security feature, hybrid feature and concurrent feature. For real-time and concurrent feature have used in the study of communicating sequential process and timed automata formalism method system model to established and verified. Study for CBTC system hybrid feature modeling and validation is less, hybrid features related to system control train operation safety. This paper puts forward using linear hybrid automata formal method for ZC subsystem modeling analysis and properties test and verify.The article select the Unified Modeling Language (UML) for system description, because of its powerful ability to extension., Use stereotypes, tagged values and constraints extension method to extend UML sequence diagram for add time and variables factors. This extension can reflect real-time feature, hybrid feature and concurrent feature. According to the theory of model transformation, converts the extended UML sequence diagram to linear hybrid automata. By the transformation of the strict rules, ensure model consistency problem in the process of model transformation. Linear hybrid automata as a branch of automata, can describe the continuous variables changing process between discrete states.Finally, this paper selected the ZC subsystem trains across the border from ZC handoff control function, combined with the Move Authority generation process modeling, and use BACH hybrid automaton software to verify this model properties and safety analysis. Proved the feasibility and correctness of verification method for ZC subsystem safety in this paper.