随着无线通信技术的飞速发展,无线通信的可靠性、可用性大大提高,基于通信的列车运行控制(Communications-Based Train Control,CBTC)系统是今后轨道交通列车运行控制系统的发展趋势。论文介绍了VOBC设备的基本原理和结构以及基于安全计算机平台设计的软件结构。根据安全苛求系统开发的“V”型框架,给出VOBC设备应用软件的需求分析、概要设计、详细设计、模型建立、功能验证和性能分析的整个过程。论文详细分析了VOBC设备应用软件的安全性需求和功能需求,在此基础上给出了VOBC设备应用软件的功能划分和子模块设计,重点介绍了在设计过程中采用的结构化的软件设计方法。论文引入了有色Petri网对VOBC设备应用软件进行形式化的建模。首先介绍了有色Petri层次化的建模方法,然后根据应用软件的结构化设计建立VOBC设备应用软件的层次化有色Petri网模型。采用“由上而下”的思路建立VOBC设备应用软件的顶层模型和各级子功能模型,子功能模型包括基本防护模型、进入CBTC区域模型、折返操作模型、模式转换模型等。在建立的模型的基础上,研究了将CPN的状态空间分析和仿真分析应用于VOBC设备应用软件的验证和分析的方法和过程。重点研究了模式转换和折返操作子功能模型。利用状态空间分析完成了模式转换模块的功能验证和安全性分析,利用仿真分析完成了折返过程的性能分析。通过对应用软件的验证和分析,达到验证设计是否满足需求的目的,给应用软件设计的完善提供参考和指导。