基于项重写系统的联锁系统模型检测方法研究  

Research on modeling and verification methods of interlocking system based on term rewriting system

作　　者：张舒青 徐中伟[1] 陈祖希[1] 

机构地区：[1]同济大学电子与信息工程学院,上海201804

出　　处：《计算机工程与应用》2014年第3期49-54,共6页Computer Engineering and Applications

基　　金：国家自然科学基金(No.60674004);国家高技术研究发展计划(863)(No.2012AA112801);国家十二五科技支撑项目(No.2011BAG01B03)

摘　　要：模型检测方法对安全苛求系统建模的完整性需要一套严谨的方法论与技术,对于验证系统的正确性,具有传统方法无法比拟的优势。提出利用项重写系统建立安全苛求系统模型与验证方法,采用基于项重写系统原理的Maude工具语言,对铁路联锁系统的站场进行形式化建模,通过其语法和语义定义各类约束和离散事件,构架联锁系统属性和行为。在模型建立的基础上,对联锁站场的静态属性和安全属性进行形式化模型验证。结果表明,基于项重写系统的模型检测方法可以较好地应用于实际联锁系统软件的开发,对开发安全苛求系统和模型检测方法的实际应用提供借鉴。Modeling and verification methods require a rigorous methodology and technology for the integrity of the safety-critical system modeling, which have incomparable advantages on the correctness, compared with the traditional methods. This paper proposes a method of using the Term Rewriting System to build the model, and using Maude based on Term Rewriting System to ensure the formal description and verification of interlocking system. With the syntax and semantics of Maude, the specification of various types of constraints and discrete events constitutes the properties and behavior of the interlock system. The safety properties and static properties of interlocking station are validated on the basis of formalized model. The result shows that the modeling and verification methods based on Term Rewriting System can be used for the verification of interlocking systems scalability, and this research provides a good reference for the formal modeling and verification of the safety-critical system.

关 键 词：项重写系统 联锁 Maude语言 安全苛求系统 模型检测 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]