Timed RAISE方法在列控系统等级转换场景中的应用研究

摘要：

高速铁路列车运行控制系统是一个复杂的实时性系统，结合其实际特点，将域方法作为系统描述的切入。通过对模型检验和定理证明两种验证方法的分析比较，提出使用基于定理证明的时间化工业软件工程的严格方法Timed RAISE形式化方法对等级转换( CTCS-2级至CTCS-3级)场景进行描述，并对其场景交互一致性和实时性进行验证，结果表明该场景不会出现场景交互一致性错误，也不会违反时间的约束。

关键词：高速铁路、Timed RAISE、CTCS、等级转换场景、实时性、场景交互一致性

分类号：U283(铁路通信、信号)

资助基金：国家自然科学基金地区项目61164101

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

页数：共6页

页码：164-168,169