| ABSTRACT:The train control system requirements engineering is the starting point and foundation of the train control system development. The modeling analysis of the requirements specification is an effective means to improve the quality of its specifications and reduce the risk and cost of system development. The research of CTCS-3train control system uses the international general method of "standard", the first system of standards specification, so that the follow-up research and development of guidance system. The requirements specification formulation is mostly rely on the experience of experts in the field, and inevitably exists some loopholes or expression is not clear because of natural language and human factor, which bring the adverse effect of the system for the design and development. So the train control system requirements specification for formal modeling and verification is very necessary.The main research object of this thesis is CTCS-3train control system requirement specification and studies the modeling and formal verification analysis method. Mainly including the following points:1. This thesis focuses on an effective modeling analysis method of the train control system specification. By the proposed modeling method based on SysML Profile, its extended SysML model was set up and describes from the system requirements, the static structure and dynamic behavior aspects, and extends the modeling language to enhance the modeling ability.2. The thesis puts forward two formal analysis methods of the requirements specification from quality and quantity aspects. The requirement analysis method based on property is a qualitative analysis method, and the consistency, realizability and design intent of the requirement specification can be analyzed by this method. The analysis method based on MITLFG quantitatively is used to describe time constraints of system requirements. These two approaches are complementary.3. The thesis has developed a software for modeling and formal analysis of the train control system specification:ReqTool. The software is a set of tools based on the Eclipse platform, integrating modeling tool (Topcased) and verification tools (RATSY) successfully. It implements three main functions including model extraction, model building and model analysis, and greatly improves the efficiency of the modeling and verification. |