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