基于通信的列车控制(Communication Based Train Control,CBTC)系统是利用连续、大容量的车地双向数字通信实现列车控制信息和列车状态信息传输的先进列车控制系统,是今后轨道交通列车运行控制系统的发展趋势。区域控制器(Zone Controller,简称ZC)是CBTC系统的核心,对应用软件设计的合理性和安全性有很高的要求。论文首先介绍了CBTC系统区域控制器的基本原理和结构,根据安全苛求系统的“V”型框架,从功能需求的角度入手,结合安全计算机平台的安全性需求,对区域控制器应用软件进行了详细的功能划分。并基于软件蓝图方法论进行了应用软件的设计,体现了结构化设计的特点。论文选择了统一建模语言(UML)及其嵌入式开发环境Rhapsody的形式化建模方法建立了CBTC系统区域控制器的模型,以区域控制器系统为模型主体,描述了区域控制器应用软件的系统模型,随后对ZC子系统中发挥关键作用的功能模块进行了具体细化,完善整体功能。通过形式化的建模和分析,有效地排除了系统原有设计中存在的矛盾、二义性、含糊性等情况,保证区域控制器应用软件切实满足功能需求和安全性需求。论文最后在建立模型的基础上,通过将模型导入高安全性应用开发环境(SCADE)中对ZC子系统应用软件的设计进行相关的安全性验证,通过对模型的模拟仿真、形式验证以及覆盖率分析,验证了设计的安全性、功能的完备性以及模型的覆盖程度,为ZC子系统的设计提供了理论依据,给应用软件设计的完善提供了参考和指导。