全自动驾驶(Fully Automatic Operation, FAO)系统是一种解决高速度、高密度城市轨道交通系统的安全、节能、高效、灵活运输等问题的重要手段,其核心是将列车驾驶员、调度员执行的工作,完全由自动化、智能化的系统所替代,是未来城市轨道交通发展方向之一。针对FAO系统核心部分高安全苛求的列控系统而言,在运营场景设计开始阶段,采用形式化方法分析运营场景的需求规范并验证其实时性,排除功能和性能隐患,对保障FAO系统安全高效运行具有非常重要的意义。本文综合分析了形式化方法在列控系统运营场景的应用状况,通过比较单独采用UML时序图或基于时间自动机理论和模型检测工具UPPAAL的优缺点,形成了基于UML和(?)JPPAAL的建模与验证流程,为FAO系统运营场景的形式化分析研究提供了重要参考和指导。论文的主要内容如下：1、总结了FAO系统有别于现有CBTC系统三个具有代表性的典型运营场景：建立和取消保护区、自动折返、出段作业,并从信号系统角度,详细给出了场景的实现流程、信息交互的数据流、以及功能和性能需求。2、采用规范描述的方法对三个典型运营场景的功能和性能需求规范进行整理和分类,分别从术语、功能、通信、环境、特性等方面提取实时动态行为,并整理出时序图模型元素对应图表,实现了需求规范与模型元素的跟踪管理。3、构建三个典型运营场景的时序图模型,根据时序图模型元素到时间自动机的模型元素语义上的对应关系,分别进行了时序图模型到时间自动机模型转换,并得到时间自动机网络模型。由于人工模型转换的繁琐,本文开发了软件工具实现自动转换过程。4、给出三个典型运营场景的功能和性能需求规范及安全属性的查询语句,采用UPPAAL验证器检测时间自动机网络模型,从可达性、受限活性、安全性三个方面分别验证分析了运营场景需求规范所反映的实时性的正确性,并举例说明了反例分析过程。