自从二十世纪八十年代以来,计算机和网络技术越来越深入到工业、交通、国防以及日常生活领域中，它对列车运行控制系统的影响也是性的,列车自动防护系统、车地实时通信的实现等等使得轨道交通运输自动化程度大大提高，使用计算机控制系统能够降低成本,增强系统功能,给系统设计和维护带来很多便利,可以最大限度的减少人为出错的概率,有利于提高系统的安全性[2]。

随着对于计算机系统安全技术研究的深入,国外有关学者己经把和安全功能有关的计算机系统看作安全苛求系统单独进行研究,提出了很多提高系统安全性的技术方法`,安全苛求系统是指对组成系统的软件、硬件安全性级别要求很高的计算机、电子或电气系统,系统出现故障后可能导致人员伤亡、重大经济损失或环境破坏等严重后果，轨道交通列车运行控制系统发生故障后可能导致行车事故,是一种典型的安全苛求系统[3]。

随着计算机技术的提高,应用在列车运行控制系统中计算机系统变得越来越复杂，规模也越来越大，复杂的系统很难设计开发,寻找错误和安全隐患也比较困难,一般的测试方法很难发现系统所有的设计故障,这会给轨道交通系统的安全、高效运行带来一定的安全隐患[4]。于是尝试使用形式化方法解决安全性问题。

形式化方法已经在轨道交通领域有了一定应用，它是基于离散数学和形式逻辑的一种方法，它采用形式语义符号和工具表述所要设计的计算机系统，并根据系统规范对系统的性质和正确性进行严格证明[2]。在系统设计开发过程中使用数学方法有许多优点，数学是准确的建模媒体，能够对系统状态、动作行为等进行准确的描述，数学方法的抽象性和演绎证明可以揭示系统设计中的矛盾性和不完整性[3]。

随着越来越多的实时嵌入式系统被部署到我们周边的环境中，并且有轨电车需要及时准确地感知周围的物理环境，形式化方法变得越来越重要，形式化设计如何满足关键的功能和实时要求也已成为主要挑战。为了解决这个问题，可以用多视角方法来协调不同的模型系统和物理环境，即协调不同语言的模型和多种工具；通过共享相同的参考架构来确保不同模型的协作；简化系统和架构，使用统一的观点来自上而下的整合系统建模；支持不同的方法来验证关键要素；最终向模型返回验证结果。

混合架构分析与设计语言（AADL）是形式化方法的一种，它可以对连续物理环境与嵌入式控制系统之间的相互作用进行建模。然而，AADL并不适合于整体系统性能的准确推理，特别是当有轨电车系统与不确定的外部环境紧密相互作用时。为了解决这一问题，可以采用一种基于统计模型检查的框架，针对不同的外部环境执行AADL模型设计的定量评估。该方法扩展了HybridAADL，可以对不确定性环境的建模。此外，本文尝试使用了一组转换规则，可以将AADL设计与设计人员的需求自动转换为定价自动机（NPTA）。