Formal verification of railway interlocking system based on ladder logic

Journal of Computer Applications ›› 2013, Vol. 33 ›› Issue (12): 3419-3422.

• 2013 National Open Distributed and Parallel Computing Confernece of China (DPCS2013) • Previous Articles Next Articles

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

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

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

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

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

Abstract

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

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

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

CLC Number:

TP311

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.

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

[1]	WU Peng, WU Jinzhao. Reasoning method based on linear error assertion [J]. Journal of Computer Applications, 2021, 41(8): 2199-2204.
[2]	BAO Yulong, ZHU Xueyang, ZHANG Wenhui, SUN Pengfei, ZHAO Yingqi. Formal verification of smart contract for access control in IoT applications [J]. Journal of Computer Applications, 2021, 41(4): 930-938.
[3]	AN Xin, XIA Jinwei, YANG Haijiao, OUYANG Yiming, REN Fuji. Discrete controller synthesis based resource management method of heterogeneous multi-core processor system [J]. Journal of Computer Applications, 2020, 40(6): 1698-1706.
[4]	MAO Xinyi, NIU Jun, DING Xueer, ZHANG Kaile. QoS verification of microservice composition platform based on model checking [J]. Journal of Computer Applications, 2020, 40(11): 3267-3272.
[5]	QIN Nan, MA Liang, HUANG Rui. Software safety requirement analysis and verification method based on system theoretic process analysis [J]. Journal of Computer Applications, 2020, 40(11): 3261-3266.
[6]	WANG Peng, WU Kang, YAN Fang, WANG Kenian, ZHANG Xiaochen. Security verification method of safety critical software based on system theoretic process analysis [J]. Journal of Computer Applications, 2019, 39(11): 3298-3303.
[7]	HAN Deshuai, XING Jianchun, YANG Qiliang, LI Juelong. Modeling and verification approach for temporal properties of self-adaptive software dynamic processes [J]. Journal of Computer Applications, 2018, 38(3): 799-805.
[8]	LU Jintian, YAO Lili, HE Xudong, MENG Bo. Improvement of OpenID Connect protocol and its security analysis [J]. Journal of Computer Applications, 2017, 37(5): 1347-1352.
[9]	MO Liping ZHOU Kaiqing. Formal description of dynamic construction method for square Hmong language characters [J]. Journal of Computer Applications, 2014, 34(3): 861-864.
[10]	LI Jin ZHANG Hua WU Hao-xiong XIANG Jun. Formal description and analysis of conformance of composite Web service behavior [J]. Journal of Computer Applications, 2012, 32(02): 545-550.
[11]	. Model checking technology and tool development based on Groebner base [J]. Journal of Computer Applications, 2009, 29(10): 2841-2843.
[12]	. Epistemic Cord logic: verifying anonymous routing protocols in Ad Hoc network [J]. Journal of Computer Applications, 2009, 29(09): 2432-2434.
[13]	Chen CHEN Yong-Sheng CHEN. Software model checking based on hierarchical unit partition [J]. Journal of Computer Applications, 2008, 28(8): 2109-2112.
[14]	XU Xiang WU jin-zhao Lin lian-nan Chen Jian-feng. Model checking interactive Markov chains [J]. Journal of Computer Applications, 2008, 28(7): 1868-1871.
[15]	. Study on workflow model checking [J]. Journal of Computer Applications, 2007, 27(6): 1448-1451.

Formal verification of railway interlocking system based on ladder logic

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

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics