CBTC联锁系统的形式化建模与验证方法研究

发布时间：2018-04-27 06:02

本文选题：联锁系统 + 形式化方法　；参考：《中国铁道科学研究院》2017年博士论文

【摘要】：作为基于通信的列车控制(Communication Based Train Control,CBTC)系统的安全关键设备,联锁系统的结构、功能逻辑复杂,软硬件集成度较高,是典型的复杂安全苛求系统。如何保证联锁系统开发的正确性和安全性,寻求一套全面、有效的建模与验证方法已经成为CBTC系统中亟需解决的问题。近年来,基于严格数学定义的形式化方法越来越显示出它的优越性,不仅能够准确、清晰地描述系统的结构与功能,而且能够对系统特性进行验证,已经成为CBTC联锁系统建模与验证的一种重要理论方法。基于此,针对CBTC联锁系统形式化建模与验证的关键问题,本文从模型可重用性、并发性、模型转换方法,以及组合形式化方法四个方面展开了深入研究。本论文的主要成果和创新点如下:(1)针对CBTC联锁系统模型状态空间复杂、重复构件模型成本巨大的问题,本文提出并实现了一种基于分层有色Petri网(HCPN)的CBTC联锁系统模型模板。该模板属于分层的参数化模型,可重用性较强,适用于不同的CBTC车站,提高了联锁系统的建模效率与普适性,并且该模板通过分层建模思想解决模型的状态空间爆炸问题。(2)针对CBTC联锁系统的HCPN模型的同步触发和并发性问题,本文引入了模型的消息驱动机制,解决了HCPN模型无法支持各网络层之间并发行为以及同步触发的问题。该方法在现有HCPN框架的基础上,增加消息驱动机制,能够实现模型中信号机、道岔等控制对象的同步触发,弥补传统HCPN的不足。(3)针对模型转换以及代码生成问题,本文给出了由HCPN模型至B语言符号的转换方法。该模型转换方法优化了模型转换机制,能够兼容HCPN多种类型的颜色集。该方法实现HCPN模型转换至B抽象机的转换,生成的B抽象机能够通过Atelier B软件的模型验证,为代码的自动生成提供了保证。(4)针对单一形式化建模方法的不足之处,本文提出了一种融合基于函数的建模方法与基于逻辑的建模方法的组合建模方法。该建模方法克服了单一HCPN建模不能反映时间的问题,使得模型更易于发现系统设计中的错误、不一致性、模糊性和不完备性。将时间自动机的建模方法运用到CBTC联锁系统模板中,增强了联锁模板的通用性。
[Abstract]:As the security key equipment of communication Based Train control system based on communication, the interlocking system is a typical complex security demanding system with complex structure, complex function logic and high integration of hardware and software. How to ensure the correctness and security of interlocking system and find a set of comprehensive and effective modeling and verification methods has become an urgent problem in CBTC system. In recent years, the formal method based on strict mathematical definition has more and more advantages. It can not only describe the structure and function of the system accurately and clearly, but also verify the characteristics of the system. It has become an important theoretical method for modeling and verification of CBTC interlocking systems. Based on this, aiming at the key problems of formal modeling and verification of CBTC interlocking system, this paper studies the reusability of the model, concurrency, transformation method and combinatorial formalization method. The main achievements and innovations of this paper are as follows: (1) in view of the complex state space of CBTC interlocking system model and the huge cost of repeated component model, this paper proposes and implements a CBTC interlocking system model template based on layered colored Petri net. The template belongs to a hierarchical parameterized model, which has strong reusability and is suitable for different CBTC stations. It improves the efficiency and universality of the interlocking system. The template solves the state space explosion problem of the model by the idea of hierarchical modeling. Aiming at the synchronous trigger and concurrency of the HCPN model of CBTC interlocking system, this paper introduces the message-driven mechanism of the model. It solves the problem that the HCPN model can not support concurrent behavior and synchronous trigger among different network layers. Based on the existing HCPN framework, the method adds message-driven mechanism, which can realize synchronous trigger of control objects such as signal generator and switch in the model, and make up the deficiency of traditional HCPN.) aiming at the problem of model transformation and code generation, the method aims at the problem of model transformation and code generation. In this paper, the transformation method from HCPN model to B language symbol is given. The model transformation method optimizes the model transformation mechanism and can be compatible with various color sets of HCPN. This method realizes the conversion of HCPN model to B abstract machine. The generated B abstract machine can be verified by the model of Atelier B software, which can guarantee the automatic generation of code. In this paper, a combination modeling method based on function and logic is proposed. This method overcomes the problem that single HCPN modeling can not reflect time, and makes it easier for the model to find errors, inconsistency, fuzziness and incompleteness in system design. The modeling method of time automata is applied to the CBTC interlocking system template, which enhances the generality of interlocking template.
【学位授予单位】：中国铁道科学研究院
【学位级别】：博士
【学位授予年份】：2017
【分类号】：U284.48

【相似文献】