Formal method applied to safety verification for computer interlocking software
-
摘要: 铁路信号系统中的联锁系统对安全性要求极高，仅通过普通的功能测试无法保障其安全性。采用形式化验证的方式可以验证联锁系统的应用逻辑与安全需求的一致性。将通用安全需求结合具体的站场图进行实例化，得到具体的安全需求后输入带归纳功能的布尔可满足问题（SAT）约束求解器进行验证，通过覆盖所有的实例、所有周期以及每个周期所有的状态空间，保证了验证方法的完备性。Abstract: The Interlocking System is a safety critical system. Its safety cannot be guaranteed only by testing. Formal verification can be used to verify the consistency between the applied logic and the safety requirements of the System. In this article, the general safety requirements were instantiated with the specific station layout. Then the specific safety requirements were verified through inputting them to the SAT induction constraint solver. The completeness of the method was guaranteed by covering all the instances, all the cycles and all the state space of each cycle.
-
-
[1] Nicolas Halbwachs, FabienneLagnier, Christophe Ratel. Programming and Verifying Real-TimeSystems by Means of the SynchronousData-Flow Language LUSTR[J]. IEEE Transactions of Software Engineering,1992,18(9):785-793. [2] 古天龙. 软件开发的形式化方法[M]. 北京：高等教育出版社，2005 ：15-22. [3] 石纯一，王家廞. 数理逻辑与集合论[M]. 北京：清华大学出版社，2000 ：54-111. [4] 何文卿. 6502 电气集中电路[M]. 北京：中国铁道出版社，2007 ：112-132. [5] 童湖东，宁 滨，王海峰. 基于Event-B 的联锁进路控制建模验证方法研究[J]. 铁路计算机应用，2013，22（6）：57-61. [6] 季晓慧，张 健. 约束问题求解[J]. 自动化学报，2007，33（2）：125-131. [7] Y Vizel，G Weissenbacher，S Malik. Boolean Satisfiability Solvers and Their Applications in Model Checking[J]. Proceedings of the IEEE, 2015 (11):1-15. [8] J Marques-Silva. Model checking with Boolean Satisfiability[J]. Journal of Algorithms, 2008, 63(1–3):3-16. -
期刊类型引用(5)
1. 王绍新，王燕芩，闫连山. 面向形式化验证的联锁翻译器软件设计. 铁路通信信号工程技术. 2022(02): 18-23+42 . 
百度学术
2. 李卫娟，王燕芩. 基于场景分析的联锁系统安全需求识别过程研究. 铁道通信信号. 2021(03): 32-36 . 百度学术
3. 罗耀云. 铁路车站联锁软件进路搜索算法优化. 电子设计工程. 2021(10): 51-55 . 百度学术
4. 张程，王燕芩. 基于Prover的联锁软件形式化验证过程研究. 铁道通信信号. 2020(03): 17-21 . 百度学术
5. 张恬. 基于SCADE的计算机联锁软件开发研究. 铁路计算机应用. 2020(12): 53-56 . 本站查看
其他类型引用(6)
计量
- 文章访问数: 107
- HTML全文浏览量: 1
- PDF下载量: 26
- 被引次数: 11
下载:
