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