CTCS-3级列控系统规范的建模与形式化验证方法研究

摘要：

CTCS-3级列控系统规范是CTCS-3级列控系统设计与开发的基础,是实现互联互通以及确保系统高效率与安全性的关键环节.然而,依靠经验与直觉制定的规范不可避免地存在某些漏洞或者安全隐患,因此对CTCS-3级列控系统规范进行建模与形式化验证显得十分必要.本文提出CTCS-3级列控系统规范建模与形式化验证方法,此方法的特点是能够在系统规范、模型、验证工具以及验证结果之间建立一条跟踪链,从而始终保证系统规范、模型及程序代码之间的一致性.结合笔者运用此方法对CTCS-3级列控系统规范建模与形式化验证的实践,证明这种方法是可行的、高效的.

关键词：CTCS-3级列控系统、系统规范、建模、形式化验证

所属期刊栏目：33

分类号：TP301;U284.48(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目60634010;轨道交通控制与安全国家重点实验室自主研究课题RCS2008ZZ005

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

页数：共6页

页码：67-72