| 基于梯形逻辑的联锁系统形式化验证方法 |
| |
| 引用本文： | 于丽贞,徐中伟,陈祖希,张舒青.基于梯形逻辑的联锁系统形式化验证方法[J].计算机应用,2013,33(12):3419-3422. |
| |
| 作者姓名： | 于丽贞 徐中伟 陈祖希 张舒青 |
| |
| 作者单位： | 同济大学 电子与信息工程学院，上海 201804 |
| |
| 基金项目： | 国家自然科学基金资助项目;国家863计划项目 |
| |
| 摘 要： | 铁路联锁系统设计通常采用梯形逻辑进行建模。为了实现对铁路联锁系统进行形式化验证的目的，根据梯形逻辑的状态变迁语义，将梯形逻辑表示的联锁系统模型转换成模型检测工具NuSMV的语言，并将铁路联锁系统的安全需求表示为计算树逻辑(CTL)，最后实现基于NuSMV的铁路联锁系统设计模型的形式化验证。
|
| 关 键 词： | 铁路联锁系统 模型检测 形式化方法 梯形逻辑 NuSMV模型检测 |
| 收稿时间： | 2013-07-19 |
Formal verification of railway interlocking system based on ladder logic |
| |
| YU Lizhen XU Zhongwei CHEN Zuxi ZHANG Shuqin.Formal verification of railway interlocking system based on ladder logic[J].journal of Computer Applications,2013,33(12):3419-3422. |
| |
| Authors: | YU Lizhen XU Zhongwei CHEN Zuxi ZHANG Shuqin |
| |
| Affiliation: | College of Electronics and Information Engineering, Tongji University, Shanghai 201804, China |
| |
| Abstract: | 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. |
| |
| Keywords: | railway interlocking system model checking formal method ladder logic NuSMV model checking |
|
| 点击此处可从《计算机应用》浏览原始摘要信息 |
|
点击此处可从《计算机应用》下载全文 |
