Formal Modeling and Verification of CTCS-2 Train Control System
Dong Yu, Shui Jing, Lei Li · Jisuanji gongcheng · 2013
(Abstract)For the designing complexity of CTCS-2 system, this paper proposes the method combining Unified Modeling Language(UML) and Symbolic Model Checking(SMC) for modeling and formal verification. It analyzes the mode conversion scene of CTCS-2 on-board equipment. The mode conversion scene of CTCS-2 on-board equipment is modeled by using the UML, and UML class diagrams and UML state diagrams are gotten as well, through formulating some exchanging rules to extend and abstract UML model and exchanging it to the NuSMV model. The property of to be verified system and system Symbolic Model Verifier(SMV) model are inputted to symbolic model verifier to check. The verified results are true, and it shows that mode conversion scene of CTCS-2 on-board equipment has activity, accessibility and security. (Key words ) )) )train control system; Symbolic Model Checking(SMC); formal method; on-board equipment; mode conversion