Research On Formal Modeling And Verification Of Interlocking System In Communication Based Train Control System

As a complex safety critical system,Computer Based Interlocking,that is the safety critical equipment of the Communication Based Train Control System,has complex structure and function logic,and high integration of hardware and software.How to explore a comprehensive and effective modeling and verification method to ensure the correctness and safety of the interlocking system development becomes an urgent problem of CBTC system.In recent years,the formal method based on rigorous mathematical definition has shown its superiority,which not only accurately and clearly describes the structure and function of the system,but only verifies the characteristics of the system.It has become an important theoretical method for modeling and verification of CBTC interlocking system.According to key issures of formal modeling and verification of CBTC interlocking system,the model reusability and concurrency,model transformation method and the combination of formal method are extensively studied in the paper.The main results and innovations are as follows:Firstly,aiming at model state space complex problem and huge cost problem of repeated component model in the CBTC system,a template for CPN hierarchical model is proposed and implemented.The template is a parameterized model with interlocking system specification and is applicable to all stations,which improves modeling efficiency and universality of the interlocking system.Meanwhile,the template alleviates the state space explosion by hierarchical modeling thought.Secondly,according to synchronous triggering and concurrency problems of HCPN model in the CBTC system,the message driven mechanism is constructed in the underlying model,which solves the problem that the CPN model can not support concurrent behavior and synchronous trigger.On the basis of the existing HCPN framework,the method increases the message driven mechanism,and realizes synchronous trigger of sinal,switch and other control objects of model to make up the shortcomings of traditional HCPN.Thirdly,point at model transformation and code generation problem,a mapping method from hierarchical colored Petri net(HCPN)model to B language is proposed in the paper.The model transformation method optimizes the model transformation mechanism and can be compatible with all kinds of color sets of HCPN model.The method converts the HCPN model to the B abstract machine,and the generated B abstract machine can be verified by model validaton of Atelier B software,which provides guarantee of automatic code generation.Forthly,in view of the shortcomings of a single formal modeling method,a combination modeling method of function based modeling methods and logic based modeling methods is presented in the paper.The modeling method overcomes the problem that the signal HCPN mdoel can not reflect temporal attribute of the CBTC system,so that the model is more likely to find errors,inconsistencies,fuzziness and incompleteness in the CBTC system design.The modeling method of timed automata is applied to the template of CBTC interlocking system,which enhances the versatility of the interlocking template.