中文摘要：

CTCS-3/4 是我国时速 350 公里以上高速列车运行控制系统规范。本项目将已有项目"基于计算机代数的嵌入式软件分析与验证方法及工具"的成果应用于 CTCS-3/4 的分析与验证。我们采用我国学者在通信顺序进程基础上设计的 HCSP 来建立 CTCS-3/4 共 14 个场景的形式模型，并用上述项目开发的系统可达性和程序终止性分析、不变式生成方法以及自创的计算机代数工具 DISCOVERER，对 CTCS-3/4重要场景的重要特性进行分析验证。列车控制系统是一种信息物理融合系统（Cyber-Physical system, CPS），CPS 是当今计算机科学研究热点。在本项目的资助下，我们还利用混成系统对CPS建模，并对混成系统的微分不变式生成、安全性验证、稳定性分析等问题进行了深入研究，取得了一些重要进展。