基于梯形逻辑的联锁系统形式化验证方法  

Formal verification of railway interlocking system based on ladder logic

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

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

出　　处：《计算机应用》2013年第12期3419-3422,3431,共5页journal of Computer Applications

基　　金：国家自然科学基金资助项目(60674004);国家863计划项目(2012AA112801)

摘　　要：铁路联锁系统设计通常采用梯形逻辑进行建模。为了实现对铁路联锁系统进行形式化验证的目的,根据梯形逻辑的状态变迁语义,将梯形逻辑表示的联锁系统模型转换成模型检测工具NuSMV的语言,并将铁路联锁系统的安全需求表示为计算树逻辑(CTL),最后实现基于NuSMV的铁路联锁系统设计模型的形式化验证。Ladder logic was used to model the railway interlocking system. In order to achieve the purpose of formal verification of the railway interlocking system, the model of the railway interlocking system expressed by ladder logic was converted to NuSMV language, which was a temporal logic model checker. Then Computational Tree Logic （CTL） specification representing the safety requirements of the railway interlocking system was verified. Finally, the formal verification of computer design model of the railway interlocking system was implemented based on NuSMV.

关 键 词：铁路联锁系统 模型检测 形式化方法 梯形逻辑 NuSMV模型检测 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]