Modeling And Verification Of Functional Compatibility Scheme For On-board System Of CTCS-1

The research of functional compatibility aims to solve the problem of train cross-line operation,one is to enable the on-board system to support train's safe operation under low-level line conditions through reasonable system design,and the second is to make sure that the train control mode can transit between different levels safely and efficiently through the reasonable scenario design.In the overall technical scheme of CTCS-1,the idea of integrating CO function inside the C1 on-board system is put forward,and the preliminary work of the project focuses on the core function,which fails to give a definite scheme for the on-board functional compatibility of C1/C0.In this thesis,problems in the current functional compatibility scheme of C1 are summarized,and the scheme is improved and designed.A modeling and verification framework for functional compatibility scheme is proposed,the basic model of functional compatibility scheme is established,and by using NuSMV symbol model testing technology and TCPN modeling and simulation method,the improved functional compatibility scheme is verified,from the perspective of system function design and train operation scenario.The main work of this thesis is as follows:(1)Analysis of functional compatibility requirement and optimization design of functional compatibility scheme.The functional compatibility items in the relevant system specification C1 are sorted out,the interaction design of the core control unit is compared,and one of them is chosen as the basis for scheme optimization.Through the system function analysis,the Cl/CO function compatibility requirement is extracted.Then the design of functional compatibility of C1 on-broad system is optimized from the aspects of system structure and function unit interaction.(2)The proposal of the research framework of the scheme verification and the establishment of the base model library.A model-based scheme verification framework is proposed.The abstraction principle from scheme to model is given from three dimensions:class,interaction and behavior.Combined with the optimized functional compatibility scheme and CO core business logic,the base model is established,which implements the standardization and visualization of the functional compatibility scheme.(3)Verification of functional compatibility scheme.A UML-based model symbolic checking method is proposed.By defining the conversion rules from UML to NuSMV,the NuSMV model is establised.The attributes to be verified are extracted and processed into the corresponding CTL expression.The state and variables that do not meet the attribute requirements are traced back according to the results of the model execution,then the cause of the error can be found,and the scheme or model to be modified accordingly,and the correct and perfected scheme is obtained.(4)Verification and perfomance analysis of scenario of level transition.The scenario of C1/C0 level transition is designed from the aspects of line design,communication interaction between on-broad system and grand system,etc.Taking the the main time constraints of each sub-link in the scenario process into consideration,the TCPN modeling of the scenario is established.The dynamic performance of the model is analyzed,which proves the rationality of the scenario design.The real-time performance of the scene is discussed,and the line design suggestion is given.Through the research of this thesis,a relatively complete functional compatibility scheme of C1 on-broad system is finally obtained,and the verification results show that the scheme meets the functional compatibility requirements and conforms to the C1 system specification.The related results can provide theoretical support for the subsequent C1 technology research,and the established base model can also be reused for future multi-dimensional verification and analysis of the system.