基于形式化方法的道口控制系统规范建模与验证

• 作者: 王峥 王恪铭
• 来源期刊: 西南交通大学学报
• 学科: 交通运输
• 关键词: 铁路运输 铁路道口 需求规范 形式化方法 系统设计 模型验证
• 年，卷（期）: 2019,（3）
• 页码范围: 573-578,603
• 页数: 7页
• 分类号: TP301.2|U213.8|U298.5
• 字数: 4104字
• 语种: 中文
• DOI: 10.3969/j.issn.0258-2724.20180607

摘要

为了增强铁路道口控制系统设计的可靠性,使用一种形式化方法对该系统进行建模与验证.基于道口管理规范,在分析系统各类属性与事件流程的基础上,使用UML图方法并结合精化策略建立了系统各层的Event-B语言模型.通过对不变式的证明义务进行证明,验证了系统设计中的安全、时间特性,检查出了需求规范分析中的缺陷,提出了增强系统稳健性的改进方案,修正了系统的设计原型.最后,通过不变式冲突与死锁检验进一步确认了模型的正确性.研究表明文中方法提高了形式化建模过程的准确性与层次性,且确认得出目前规范中存在列车驶入道口时不能确保道口出清的缺陷,证实了使用本文形式化流程可以验证道口控制系统的需求规范并形成可靠的设计原型,从而可提高铁路道口的安全性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王恪铭	西南交通大学信息科学与技术学院	5	22	2.0	4.0
5	王峥	西南交通大学信息科学与技术学院	2	1	1.0	1.0