Research on Method of Modeling and Formal Verification of the CTCS-3 Train Control System Specification
Lin Zhao · Journal of the China Railway Society · 2011
The specifications of the CTCS-3 train control system is the basis of design and development of the CTCS-3 train control system,and it is crucial for realization of good interoperability and high efficiency and security of the system.However,specifications compiled by experience or intuitive thought inevitably bring about defects or hidden dangers.So it is necessary to carry out modeling and formal verification of the system specifications.The paper proposes the method of modeling and formal verification of the CTCS-3 train control system specifications.The method establishes a track chain of the system specifications,model,model checking tools and verification results so as to ensure the consistency of the system specifications,models and program codes.Our practice has proved that this method is feasible and efficient.