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

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

Application of Timed RAISE Method in Level Conversion Scene of Train Control System

The high-speed railway train control system is a complex real-time system. In the light of the actual features of the system,the domain method is employed for system modeling. With the analysis and comparison of model verification and theorem proving,the theorem-proving-based Timed RAISE( Timed Rigorous Approach to Industrial Software Engineering) is recommended to describe level transition scene( CTCS-2 to CTCS-3) and verify the scene interaction consistency and real-time capability. The results show that this scene will not cause errors in scene interactive consistency,nor violate time constraints.