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

摘要：

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

关键词：铁路运输、铁路道口、需求规范、形式化方法、系统设计、模型验证

所属期刊栏目：54

分类号：TP301.2;U213.8;U298.5(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目71502146,61673320;中央高校基本科研业务费资助项目2682017ZT12

在线出版日期：2019-06-19（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：573-578,603