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

摘要：

铁路联锁系统设计通常采用梯形逻辑进行建模.为了实现对铁路联锁系统进行形式化验证的目的,根据梯形逻辑的状态变迁语义,将梯形逻辑表示的联锁系统模型转换成模型检测工具NuSMV的语言,并将铁路联锁系统的安全需求表示为计算树逻辑(CTL),最后实现基于NuSMV的铁路联锁系统设计模型的形式化验证.

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

作者: 于丽贞 徐中伟 陈祖希 张舒青

作者单位: 同济大学 电子与信息工程学院,上海 201804

会议类型: 国内会议

会议名称: 2013年全国开放式分布与并行计算学术年会

会议地点: 昆明

会议语种:中文

页码: 3419-3422,3431

在线出版日期: 2013-08-16（万方平台首次上网日期，不代表论文的发表时间）