计算机联锁形式化验证典型反例分析

doi:10.3969/j.issn.1673-4440.2024.11.007

铁路通信信号工程技术 ›› 2024, Vol. 21 ›› Issue (11): 41-45.DOI: 10.3969/j.issn.1673-4440.2024.11.007

计算机联锁形式化验证典型反例分析

刘丽娟，陈虹，陈耀华

卡斯柯信号有限公司，北京 100070

收稿日期:2023-05-15 修回日期:2024-09-19 出版日期:2024-11-25 发布日期:2024-11-25
作者简介:刘丽娟（1984—），女，高级工程师，硕士，主要研究方向：计算机联锁及其形式化验证，邮箱：liulijuan2015163@163.com。
基金资助:
卡斯柯信号有限公司科研课题项目(RB.1X123015)

Analysis of Typical Counterexamples for Formal Verification of Computer Based Interlocking

Liu Lijuan, Chen Hong, Chen Yaohua

CASCO Signal Ltd., Beijing 100070, China

Received:2023-05-15 Revised:2024-09-19 Online:2024-11-25 Published:2024-11-25

摘要/Abstract

摘要： 形式化验证是确保计算机联锁系统满足特定安全需求的有效且重要的手段。由于形式化方法的特殊性，要求对于系统模型和安全需求模型的描述完全准确，否则均会导致验证不通过。根据计算机联锁形式化验证的实际经验，总结在安全需求模型建立过程中由于模型建立不完善导致验证失败的典型场景，为形式化验证的实践提供参考。

关键词: 形式化验证, 计算机联锁, 安全需求, 反例

Abstract: Formal verification is an effective and important means to ensure that the computer based interlocking system can meet specific safety requirements. Due to the particularity of the formal methods, the descriptions of the system model and the safety requirement model need to be completely accurate, failing which the verification will not be passed. Based on the practical experience in the formal verification of the computer based interlocking system, this paper summarizes the typical scenarios of failing to pass the validation when establishing the safety requirement model due to imperfect model establishment, which provides practical reference for formal verification.

Key words: formal verification, computer based interlocking, safety requirement, counterexample

中图分类号:

U284.3

刘丽娟, 陈虹, 陈耀华. 计算机联锁形式化验证典型反例分析[J]. 铁路通信信号工程技术, 2024, 21(11): 41-45.

Liu Lijuan, Chen Hong, Chen Yaohua. Analysis of Typical Counterexamples for Formal Verification of Computer Based Interlocking[J]. Railway Signalling & Communication Engineering, 2024, 21(11): 41-45.

图/表 6

参考文献

[1]吕毅.形式化方法介绍及其在工程中的应用[J].微电子学与计算机，2003，20（10）：26-31，34.
Lv Yi. The State of the Art in Formal Methods:a Survey[J]. Microelectronics & Computer, 2003, 20(10): 26-31, 34.
[2]郦萌，徐翥，王铁江.计算机联锁软件制式的安全性评价[J].铁道学报，2004，26（1）：59-63.
Li Meng, Xu Zhu, Wang Tiejiang. Safety Assessment of Computer Interlocking Software Systems for a Typical Railway Station[J]. Journal of the China Railway Society, 2004, 26(1): 59-63.
[3]吴彤，徐建华.基于逻辑的形式化验证方法:进展及应用[J].北京大学学报：自然科学版， 2016（2）：11.
[4]张萍，赵阳.铁路车站计算机联锁控制系统的可靠性和安全性分析[J].中国安全科学学报（4）：48.
[5]赵海新.区段占用状态对联锁系统的影响研究[J].都市快轨交通，2022，35（4）：168-174.
Zhao Haixin. The Influence of Section Occupancy Status on Interlocking System[J]. Urban Rapid Rail Transit, 2022, 35(4): 168-174.
[6]陈邦兴，吴芳美.铁路信号联锁逻辑形式化建模研究[J].铁道学报，2002，24（6）：50-54.
Chen Bangxing, Wu Fangmei. Research on Formal Models of Railway Signal Interlocking Logics[J]. Journal of the China Railway Society, 2002, 24(6): 50-54.
[7]谢雨飞，唐涛，徐田华，等.CTCS-3级列控系统规范的建模与形式化验证方法研究[J].铁道学报，2011，33（7）：67-72.
Xie Yufei, Tang Tao, Xu Tianhua, et al. Research on Method of Modeling and Formal Verification of the CTCS-3 Train Control System Specification[J]. Journal of the China Railway Society, 2011, 33(7): 67-72.
[8]彭丽维，宋鹏飞，江雪莹，等.基于模型的联锁软件测试用例生成方法[J].铁路通信信号工程技术，2022，19（11）：32-36.
Peng Liwei, Song Pengfei, Jiang Xueying, et al. Model-Based Test Case Generating Method of Interlocking Software[J]. Railway Signalling & Communication Engineering, 2022, 19(11): 32-36.
[9]王铁江，郦萌.计算机联锁软件的Z规格说明[J].铁道学报，2003，25（4）：62-66.
Wang Tiejiang, Li Meng. Z Specification of the Computer Interlocking Software[J]. Journal of the China Railway Society, 2003, 25(4): 62-66.
[10]王绍新，王燕芩，闫连山.面向形式化验证的联锁翻译器软件设计[J].铁路通信信号工程技术，2022，19（2）：18-23，42.
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.
[11]赵梦瑶，陈小红，孙海英，等.轨道交通联锁领域特定语言的形式化[J].软件学报，2020，31（6）：1638-1653.
Zhao Mengyao, Chen Xiaohong, Sun Haiying, et al. Formalizing Railway Interlocking Domain Specific Language[J]. Journal of Software, 2020, 31(6): 1638-1653.
[12]刘宁，韩程，王峥，等.基于B方法的道岔控制系统形式化建模与验证[J].铁路通信信号工程技术，2022，19（6）：5-11.
Liu Ning, Han Cheng, Wang Zheng, et al. Formal Modeling and Verification of Point Control System Based on Method B[J]. Railway Signalling & Communication Engineering, 2022, 19(6): 5-11.
[13]程鹏，王恪铭，王峥，等.基于B方法的轨道交通控制系统配置数据的形式化验证[J].铁路通信信号工程技术，2022，19（5）：7-16.
Cheng Peng, Wang Keming, Wang Zheng, et al. Formal Verification of Configuration Data of Rail Transit Control System Based on B Method[J]. Railway Signalling & Communication Engineering, 2022, 19(5): 7-16.
[14]姜楠.高速铁路信号系统安全性改进探讨[J].铁路通信信号工程技术，2018，15（1）：59-64.
Jiang Nan. Discussion on Improvement of High-Speed Railway Signal System Safety[J]. Railway Signalling & Communication Engineering, 2018, 15(1): 59-64.
[15]王曦，徐中伟.基于场景分析的系统形式化模型生成方法[J].计算机科学，2012，39（8）：136-140，163.
Wang Xi, Xu Zhongwei. Method for Generating Formal System Model Based on Scenarios Analysis[J]. Computer Science, 2012, 39(8): 136-140, 163.

计算机联锁形式化验证典型反例分析

Analysis of Typical Counterexamples for Formal Verification of Computer Based Interlocking

PDF

可视化

摘要/Abstract

引用本文

使用本文

图/表 6

参考文献

相关文章 15

编辑推荐

Metrics

本文评价

[1]	孙超. 面向不同生命周期的计算机联锁设备可靠性综合评估 [J]. 铁路通信信号工程技术, 2024, 21(9): 1-10.
[2]	柳新. DS6-100计算机联锁的IO仿真系统设计与实现[J]. 铁路通信信号工程技术, 2024, 21(5): 27-31.
[3]	周帅, 周培, 武恒颉, 周灵钰. 铁路平交道口智能集控预警系统[J]. 铁路通信信号工程技术, 2024, 21(3): 106-112.
[4]	王定明. 计算机联锁接发列车故障设置盘的设计与实现[J]. 铁路通信信号工程技术, 2024, 21(2): 14-19.
[5]	梁栋. 测试逻辑和测试数据分离模式的联锁测试脚本研究[J]. 铁路通信信号工程技术, 2024, 21(11): 34-40.
[6]	何顶, 刘重均, 邹瑶, 董妍, 苏琛. 计算机联锁试验综合管理系统的分析与应用[J]. 铁路通信信号工程技术, 2024, 21(10): 22-28.
[7]	胡井海, 王宇琮, 蔡微微. 站间联系电路的问题分析与改进[J]. 铁路通信信号工程技术, 2023, 20(8): 95-100.
[8]	戴明福. 一起计算机联锁与CTC通信异常故障案例简析[J]. 铁路通信信号工程技术, 2023, 20(7): 110-114.
[9]	宿秀元. 联挂解编进路处理逻辑研究[J]. 铁路通信信号工程技术, 2023, 20(6): 87-92.
[10]	吴金元, 王菁. CBTC系统点式模式下临时限速方案分析[J]. 铁路通信信号工程技术, 2023, 20(4): 73-76.
[11]	雷少龙, 成鹏, 莫运前. 咽喉区设置总出站信号机特殊联锁处理方案[J]. 铁路通信信号工程技术, 2023, 20(3): 7-10,16.
[12]	乔福明. 灭灯模式下信号机点灯区域的分析与确定[J]. 铁路通信信号工程技术, 2023, 20(3): 68-71.
[13]	孙志科. 应用图像识别技术开发联锁自动测试工具的研究[J]. 铁路通信信号工程技术, 2023, 20(2): 7-12.
[14]	丁建莉. 关于到发线出岔联锁技术条件的探讨[J]. 铁路通信信号工程技术, 2023, 20(12): 21-25.
[15]	金松岳. 塞尔维亚联锁侧防功能研究[J]. 铁路通信信号工程技术, 2023, 20(12): 106-109.