随着列控技术的发展,列车运行控制系统获得了巨大的进步和发展。在安全苛求系统的设计开发中,引入形式化技术不仅可以最大限度地保证各阶段开发过程的质量,同时可以改善开发效率、有效控制开发进度。然而,在保证列车运行的安全性方面,完全地应用形式化技术仍存在困难。1)在系统概要设计阶段,由于需求规范并不十分具体,导致所建立的系统形式化模型不可避免地包含某些不确定的参数。所以,在保证列车运行安全的前提下如何确定这类不确定参数的约束集,对系统初期设计显得极为重要。2)由于列控系统由多模块构成,无线通信系统模块在现代列车控制系统的作用越来越重要。在基于车-车通信的移动闭塞无人驾驶系统中,无线通信系统通信性能的不确定性可能影响列控系统的控制效率与安全性。因此,如何有效评估随机性事件对列车运行安全的影响程度对保障列车安全运行具有重要意义。3)智能学习算法作为一种概率学习算法,算法本身并不具有安全控制机制。在实现多列车的安全智能驾驶时,需要引入一种安全机制,来保证列车运行过程的安全性。4)当前的可靠性研究与系统的安全分析联系并不紧密,两者的研究分析模型往往相互独立,这严重影响了可靠性分析结果的可信度。系统的可靠性分析须建立在系统安全的基础上,系统安全是可靠性分析的重要前提条件。论文以保证列车运行过程的安全性为目标,通过结合形式化验证方法、机器学习算法及可靠性分析方法,实现对列车运行过程的安全控制和关键设备性能的动态评估。论文主要的研究成果如下:1.为了有效验证含有不确定参数的混成自动机模型,通过求解对应安全需求的控制参数的约束集的方式,实现对列车控制模型的概要设计。同时,提出时间有界的混成自动机验证算法来解决状态空间爆炸问题。该算法通过计算混成自动机控制模型在将来某段时间内的所有可执行路径,来降低传统形式化验证方法在工程实际中应用的难度,从而实现在线监控列车运行安全性的目的。2.为了实时监控列车的运行状态,提出了基于概率混成自动机模型的列车运行安全监控方法,通过将离线仿真验证和系统在线性能评估相结合的方式来降低形式化验证方法在实时监控方面的实现难度。首先,通过大量的离线验证获取与量化性能指标相对应的不确定控制参数和概率事件参数的可行域。其次,通过系统在线性能评估的方式实时获取系统的动态性能指标。最后,根据具体的系统性能指标,调取对应运行状态下列车控制参数的约束,评估系统的安全级别,并在安全级别下降的条件下提出相应的调整策略。3.为了提高列车控制过程的自主性和智能性,基于单列车的智能驾驶算法提出一种多列车安全智能驾驶策略。首先,智能驾驶算法使用的驾驶数据包括优秀司机的驾驶数据和ATO算法的仿真驾驶数据。其次,根据速度分级制动原理生成基于混成自动机的列车安全间隔控制模型。同时,运用迭代稀疏优化算法稀疏驾驶数据集,以降低智能驾驶模型的复杂性,提高智能驾驶模型的泛化能力。最后,运用集成分类回归树算法挖掘列车运行过程中潜在的驾驶规则。4.为了保证可靠性分析与安全验证结果的一致性,通过引入系统建模语言来描述系统的结构,并建立系统的动态故障树模型。其次,通过将所建立的动态故障树转换为连续时间Markov模型来评估系统的动态性能。为了提高系统可靠性计算效率,提出了分层迭代分析方法近似估算系统瞬态可靠性指标的方法。最后,研究了运用马尔可夫模型在不完全覆盖故障下的动态故障树模型的分析方法。