Automatic Conversion Method of the Requirements Specification Verification for CTCS Level 3
Yu Ping Zhou, Lin Feng Zhao, Jin Tao Liu · Applied Mechanics and Materials · 2014
Chinese Train Control System Level 3(CTCS-3) is a typical complex cyber-physical system which connects the control center, the station and the train. In order to ensure the friendly communication between the different manufacturers equipment, the high reliability is required by the CTCS-3 system. The reliability of a system can be tested with the formal verification method and a lot of formal tools have been developed, such as SPIN, VIS and NuSMV. In this paper, we describe the modeling techniques and abstractions of the control process. The required assembly unit has been specified as extended class. The required behavior has been specified as extended state machine diagrams and translated to temporal logic properties. Then, we propose a method to simplify the steps which transfer a UML model into a formal model. Moreover, the transition can be implemented with development language, where its result-the formal model-can be run by the formal tool and return an analysis result. At last, we take the Radio Block Center (RBC) Handover of CTCS-3 as an example, and the experimental results show the validity and feasibility of this method.