%0 Journal Article
%T 基于梯形逻辑的联锁系统形式化验证方法
%A 于丽贞
%A 徐中伟
%A 陈祖希
%A 张舒青
%J 计算机应用
%D 2013
%X ？铁路联锁系统设计通常采用梯形逻辑进行建模。为了实现对铁路联锁系统进行形式化验证的目的，根据梯形逻辑的状态变迁语义，将梯形逻辑表示的联锁系统模型转换成模型检测工具nusmv的语言，并将铁路联锁系统的安全需求表示为计算树逻辑(ctl)，最后实现基于nusmv的铁路联锁系统设计模型的形式化验证。
%K 铁路联锁系统
%K 模型检测
%K 形式化方法
%K 梯形逻辑
%K nusmv模型检测
%U http://www.joca.cn/CN/abstract/abstract16888.shtml