论文部分内容阅读
作为基于通信的列车控制(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联锁系统模板中,增强了联锁模板的通用性。