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

计算机应用 ›› 2013, Vol. 33 ›› Issue (12): 3419-3422.

• 2013年全国开放式分布与并行计算学术年会（DPCS2013）论文 • 上一篇下一篇

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

于丽贞,徐中伟,陈祖希,张舒青

同济大学电子与信息工程学院，上海 201804

收稿日期:2013-07-19 出版日期:2013-12-01 发布日期:2013-12-31
通讯作者: 张舒青
作者简介:于丽贞(1989-),女,陕西岐山人,硕士研究生,主要研究方向:形式化验证;
徐中伟(1964-),男,江苏无锡人,教授,主要研究方向:基于通信的列车控制系统与软件、通信协议的安全性形式验证和测试评估;
陈祖希(1981-),男,四川泸州人,博士研究生,主要研究方向:安全软件测试与评估;
张舒青(1989-),男,上海人,硕士研究生,主要研究方向:模型检测。
基金资助:
国家自然科学基金资助项目;国家863计划项目

Formal verification of railway interlocking system based on ladder logic

YU Lizhen,XU Zhongwei,CHEN Zuxi,ZHANG Shuqin

College of Electronics and Information Engineering, Tongji University, Shanghai 201804, China

Received:2013-07-19 Online:2013-12-31 Published:2013-12-01
Contact: ZHANG Shuqin
Supported by:
National Natural Science Foundation

摘要/Abstract

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

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

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.

Key words: railway interlocking system, model checking, formal method, ladder logic, NuSMV model checking

中图分类号:

TP311

于丽贞徐中伟陈祖希张舒青. 基于梯形逻辑的联锁系统形式化验证方法[J]. 计算机应用, 2013, 33(12): 3419-3422.

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.

[1]	武鹏, 吴尽昭. 基于线性误差断言的推理方法[J]. 计算机应用, 2021, 41(8): 2199-2204.
[2]	包玉龙, 朱雪阳, 张文辉, 孙鹏飞, 赵颖琪. 物联网应用中访问控制智能合约的形式化验证[J]. 计算机应用, 2021, 41(4): 930-938.
[3]	安鑫, 夏近伟, 杨海娇, 欧阳一鸣, 任福继. 基于离散控制器合成的异构多核系统资源管理方法[J]. 计算机应用, 2020, 40(6): 1698-1706.
[4]	秦楠, 马亮, 黄锐. 基于系统理论过程分析的软件安全性需求分析与验证方法[J]. 计算机应用, 2020, 40(11): 3261-3266.
[5]	毛昕怡, 钮俊, 丁雪儿, 张开乐. 基于模型检测的微服务组合平台QoS验证[J]. 计算机应用, 2020, 40(11): 3267-3272.
[6]	韩德帅, 邢建春, 杨启亮, 李决龙. 自适应软件动态过程时间特性建模与验证方法[J]. 计算机应用, 2018, 38(3): 799-805.
[7]	鲁金钿, 尧利利, 何旭东, 孟博. 改进的OpenID Connect协议及其安全性分析[J]. 计算机应用, 2017, 37(5): 1347-1352.
[8]	常天佑, 魏强, 耿洋洋. 基于状态转换的PLC程序模型构建方法[J]. 计算机应用, 2017, 37(12): 3574-3580.
[9]	莫礼平周恺卿. 方块苗文动态构造方法的形式化描述[J]. 计算机应用, 2014, 34(3): 861-864.
[10]	熊金波姚志强金彪. 云计算环境中结构化文档形式化建模[J]. 计算机应用, 2013, 33(05): 1267-1270.
[11]	李劲张华吴浩雄向军. Web服务组合行为一致性的形式化描述和分析[J]. 计算机应用, 2012, 32(02): 545-550.
[12]	廖紫骅谭红艳吴尽昭. 基于Groebner基的模型检测技术及其工具实现[J]. 计算机应用, 2009, 29(10): 2841-2843.
[13]	李沁曾庆凯. 知性Cord逻辑：验证Ad Hoc网络匿名路由协议[J]. 计算机应用, 2009, 29(09): 2432-2434.
[14]	陈晨陈永生. 基于层次单元划分的软件模型检测技术研究[J]. 计算机应用, 2008, 28(8): 2109-2112.
[15]	闫志华李成郑艳萍. 工作流模型检测研究[J]. 计算机应用, 2007, 27(6): 1448-1451.

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

Formal verification of railway interlocking system based on ladder logic

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics