等级转换是CTCS(Chinese Train Control System,中国列车运行控制系统)主要场景之一,其功能能否精确、实时完成直接关系到列车运行效率及人民生命财产安全。随着自动化与智能控制技术的不断提高,铁路列控系统在不断更替,我国现有铁路线路主要有CTCS-2级和CTCS-3级两种,实现不同线路区段条件下的等级转换是列控系统开发中应对当前现状的关键课题之一。然而,列控系统结构复杂、规模庞大、实时性强,系统中各功能模块出现的任何设计缺陷都有可能造成严重后果,如何实现系统体系结构及逻辑功能的正确、严谨描述,成为系统开发中的关键和研究的热点。相比仿真和测试方法,具有严密数学逻辑的形式化方法不但可以实现对系统构架和特征的严谨描述,而且可以严格地验证系统特性,近年来已发展成为安全苛求系统建模和验证的一种重要方法。本文采用域方法和Timed RAISE(Timed Rigorous Approach to Industrial Software Engineering,时间化的工业软件工程的严格方法)对列控系统等级转换功能模块进行描述,并实现在系统信息交互正确性和实时性方面的验证。主要研究内容如下:首先,通过分析对比国内外已有列控系统等级转换功能模块的形式化建模研究,针对Timed RAISE在等级转换场景研究中不够深入的现状,在收集系统设计标准规范的基础上,深刻分析了等级转换场景中各设备信息交互处理的过程,研究得到了系统在固定点进行转换的信息时序交互图。其次,以信息交互图为依据,划分出系统执行的各设备状态,建立状态迁移图,在对司机和应答器处理逻辑作以归纳的基础上,得到该场景的功能状态划分。随后,采用五元组域模型为基础,设计并建立了等级转换场景下的系统体系结构,通过研究Timed RAISE语言规范,根据域模型各特征元素的形式化实现,完成了对整个等级转换场景的形式化表达。最后,使用公理形式表述系统设计约束,根据Timed RAISE推理规则并结合系统功能模块的形式化描述,对系统的切换正确性和实时性进行了验证。本文的研究深入分解了等级转换场景下系统各部分之间的信息处理逻辑,形成了规范的系统场景形式化表述,为系统体系结构设计及开发提供了依据,在系统开发的生命周期内可保障模块功能描述的语义一致性和正确性,可提高系统设计开发效率。