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

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