Research On The Method Of Formal Modeling And Verification Of The Train Control System Requirements Specification

The Train Control System requirements specification is the basic of designing and developing product, and it is crucial for interoperability and efficiency and security. However, the system is a complicated safety-critical system, and the specification dependent on experience inevitably exist some defects or potential safety hazard. In addition, the specification described in natural language may have ambiguity, which would not be beneficial to designing and developing system. So it is necessary to formal modeling and verification for the system requirements specification.Our works take the CTCS-3Train Control System Requirements Specification as the background, to research on the method of modeling and formal verification of the system requirements specification. Firstly, an improved methodology of modeling and formal verification of the train control system requirements specification is proposed. It establishes a bidirectional and integrated track chain for the system requirements specification, model, model checking process and verification results so as to ensure the consistency between the system requirements specifications, models and program code. And then, based on this methodology, focus on how to ensure the consistency and coverage between the model and specification, and research on the model transformation technique between UML and CSP. The main work and innovation are as follows:(1) An improved methodology of modeling and formal verification of the train control system requirements specification is proposed by using a combination of specification management, formal modeling and verification. Different from other methodologies which are only suitable for some scenario or singleness character of the system requirements specification, it could suitable for the whole specification.(2) Safety specification is emphasized in the methodology of formal modeling and verification of the train control system requirements specification. According to the mapping relationship, safety elements are injected into the specification model by formal method. A track and feedback mechanism is established in the methodology. It is beneficial to analysis the consistency and coverage between the specification in natural language and the model, and could implement model transformation and model analysis, and make the verification result could track to the specification document by using the feedback mechanism. (3) A method of modeling the train control system requirements specification based on the extended UML is proposed, and the modeling profile is given. The compulsion safety requirements in the specification are described by stereotype, tag and constraint in the profile. This method could embody system safety properties in the model, and enhanced the reusability, and improve the modeling efficiency. On the other hand, modeling and model checking rules are refined and category guiding principle and mapping relationship are defined. These rules could greatly reduce the subjective factors in the modeling process.(4) A methodology for the model transformation technique between UML and CSP is proposed. The UML metamodel and CSP metamodel are given respectively. By analyzing the features of source and target metamodel languages, a set of model transformation rules are proposed so as to implement atom mappings and pattern mappings. Property preservation of model transformations and the method to prove the correctness of the set of transformation rules are discussed to ensure the reasonable model transformation process.(5) A tool for modeling and verification for the train control system is developed. This tool focuses on model narrowing, transformation, model checking and analysis, and offers an automatic mechanism for formal modeling and verification of the train control system requirements specification. Our practice shows that the tool is effective.