Design of Interlocking Translator Software Oriented to Formal Verification

doi:10.3969/j.issn.1673-4440.2022.02.005

Railway Signalling & Communication Engineering ›› 2022, Vol. 19 ›› Issue (2): 18-23,42.DOI: 10.3969/j.issn.1673-4440.2022.02.005

Previous Articles Next Articles

Design of Interlocking Translator Software Oriented to Formal Verification

Wang Shaoxin^{1, 3}, Wang Yanqin², Yan Lianshan³

1. CASCO Signal (Chengdu) Ltd., Chengdu 610083, China;
2. CASCO Signal Ltd., Shanghai 200071, China;
3. College of Information Science and Technology, Southwest Jiaotong University, Chengdu 611756, China

Received:2020-12-30 Revised:2021-07-20 Online:2022-02-25 Published:2022-02-25

面向形式化验证的联锁翻译器软件设计

王绍新^1，3，王燕芩²，闫连山³

1.卡斯柯信号（成都）有限公司，成都 610083；
2．卡斯柯信号有限公司，上海 200071；
3．西南交通大学信息科学与技术学院，成都 611756

作者简介:王绍新（1982—），男，工程师，博士，主要研究方向：铁路通信信号、计算机联锁、形式化开发与验证、铁路北斗系统应用，邮箱：wangshaoxin@my.swjtu.edu.cn
基金资助:
中国国家铁路局集团有限公司科技研究开发计划重点课题（N2021S003）；四川省重大科技专项（2019ZDZX0007）

Abstract

Abstract: According to the system requirements in formal veriﬁcation of the interlocking system, this paper designs an overall scheme of translator software for interlocking data, which realizes the translation and conversion of station interface ﬁles, TLE ﬁles and Boolean logic ﬁles, and generates the LCF ﬁles for formal verification. Finally, the code implementation of the translator software based on the functional language OCaml is explained in detail.

Key words: interlocking system, formal veri?cation, translator software, OCaml, functional programming

摘要： 根据联锁系统的形式化验证系统需求，设计一种联锁数据翻译器软件的总体方案，实现站点接口文件、TLE文件和布尔逻辑文件等文件的翻译转换，生成形式化验证所需要的LCF文件。最后详细说明翻译器软件基于函数式语言OCaml的代码实现。

关键词: 联锁系统, 形式化验证, 翻译器软件, OCaml, 函数式语言

CLC Number:

U294.36⁺2

Wang Shaoxin, Wang Yanqin, Yan Lianshan. Design of Interlocking Translator Software Oriented to Formal Verification[J]. Railway Signalling & Communication Engineering, 2022, 19(2): 18-23,42.

王绍新, 王燕芩, 闫连山. 面向形式化验证的联锁翻译器软件设计[J]. 铁路通信信号工程技术, 2022, 19(2): 18-23,42.

Figures/Tables 9

References

[1]Yaron Minsky，Anil Madhavapeddy，Jason Hickey.Real World Ocaml（中文版）[M].苏金国，彭小姣，译.北京：中国电力出版社，2015.
[2]崔惠珊，张路，刘亚磊，等.城市轨道交通计算机联锁实训系统设计与实现[J].铁路通信信号工程技术，2019，16(6):73-77.
Cui Huishan, Zhang Lu, Liu Yalei, et al. Design and Implementation of Computer Based Interlocking Training System of Urban Rail Transit[J]. Railway Signalling & Communication Engineering, 2019, 16(6): 73-77.
[3]孙晓光.一种联锁图表自动生成软件研究与设计[J].铁路通信信号工程技术，2021，18(6):1-6.
Sun Xiaoguang. Research and Design of Software for Automatic Generation of Interlocking Charts[J]. Railway Signalling & Communication Engineering, 2021, 18(6): 1-6.
[4]田文军.信号计算机联锁系统安全性可靠性分析[J].铁路通信信号工程技术，2013，10(6)：32-35.
Tian Wenjun. Analysis of Safety and Reliability of Computer Interlocking System[J]. Railway Signalling & Communication Engineering, 2013, 10(6): 32-35.
[5]付立民.全电子联锁开发和应用研究[J].铁路通信信号工程技术，2020，17(3)：32-38.
Fu Limin. Research on Development and Application of Full Electronic Interlocking[J].Railway Signalling & Communication Engineering, 2020, 17(3): 32-38.
[6]罗娟，王燕芩.形式化方法应用于计算机联锁软件的安全验证研究[J].铁路计算机应用，2016，25(11):53-57.
Luo Juan, Wang Yanqin. Formal Method Applied to Safety Verifi Cation for Computer Interlocking Software[J]. Railway Computer Application, 2016, 25(11): 53-57.
[7]谢雨飞，唐涛，徐田华，等.CTCS-3级列控系统规范的建模与形式化验证方法研究[J].铁道学报，2011，33(7):67-72.
Xie Yufei, Tang Tao, Xu Tianhua, et al. Research on Method of Modeling and Formal Veriﬁ cation of the CTCS-3 Train Control System Speciﬁcation[J]. Journal of the China Railway Society, 2011, 33(7): 67-72.
[8]陈钢，于林宇，裘宗燕，等.基于逻辑的形式化验证方法:进展及应用[J].北京大学学报(自然科学版)，2016，52(2):363-373.
Chen Gang, Yu Linyu, Qiu Zongyan, et al. Logic Based Formal Verification Methods:Progress and Applications[J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2016, 52(2): 363-373.
[9]李勇，曹子宁.基于需求的形式化建模与验证方法研究[J].计算机技术与发展，2017，27(6)：7-10.
Li Yong, Cao Zining. Investigation on Formal Modeling and Verification Method Based on Specification[J]. Computer Technology and Development, 2017, 27(6): 7-10.

Design of Interlocking Translator Software Oriented to Formal Verification

面向形式化验证的联锁翻译器软件设计

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 9

References

Related Articles 2

Recommended Articles

Metrics

Comments

[1]	Zhang Biyan. Discussion on Application Prospect of Train Control and Interlocking Integrated Equipment [J]. Railway Signalling & Communication Engineering, 2021, 18(5): 22-27.
[2]	Qin Xiaohu, Sun Xiaoguang. Research on Fully Automatic Train Washing Scheme of Urban Rail Transit [J]. Railway Signalling & Communication Engineering, 2021, 18(4): 77-82.