随着信息科学技术的快速发展,新型复杂系统如信息物理融合系统(Cyber-Physical System,CPS)逐渐融入人类社会生活。自动驾驶作为CPS经典应用场景,它根据驾驶环境的感知并通过计算做出相应驾驶决策,且具备自主性、安全性等特性。然而,复杂多变的城市交通驾驶场景、大量实时时空数据、驾驶环境中的固有不确定性等,都为确保自动驾驶的安全性带来挑战。本文采用形式化方法研究分析自动驾驶的安全性。形式化方法采用数学(逻辑)证明的手段对计算机系统进行建模、规约、分析、推理和验证。鉴于其严谨性,该方法已被广泛运用到系统安全性研究中。然而,采用形式化方法研究分析自动驾驶系统安全性仍存在诸多挑战。比如,目前时空约束大多基于微分方程建模,并不利于时空约束的抽象分析,需要提出时空逻辑支持规约和推理时空约束;对于自动驾驶环境中的状态空间爆炸问题,需要提出抽象模型以及对不确定性的建模方法;在此基础上,还需将验证系统安全问题转化为基于形式模型的判定问题,并验证安全性质。本文基于上述自动驾驶系统的特点,结合形式化方法,以自动驾驶系统安全评估为研究目标,研究了基于时空抽象模型的自动驾驶系统的形式化建模与验证方法。本文主要研究内容与贡献如下:·提出基于自动驾驶系统单车视角的时空逻辑:有界多维模态逻辑(Bounded Multi-dimensional Modal Logic,BMML)。该逻辑可以规约基于相对时间和相对空间的约束条件,并支持时空约束的推理。·定义场景并提出场景组合方法。根据场景定义和满足的相应时空约束,从而定义基本场景结构。基于基本场景结构,不仅可以根据场景连接性实现场景转换,而且可以根据场景组合性实现从基本场景结构组成各种复杂场景,为基于场景的模型检验框架奠定基础。·构建基于场景的自动驾驶系统抽象模型。抽象模型能够基于环境感知描述实时观察和估算的交通数据,并采用概率模型显式表达除却自动车之外的车辆的不确定驾驶决策。·实现自动驾驶安全性质自动化验证。基于抽象模型的验证框架,通过建立映射关系,将抽象模型转化到随机混成自动机(Stochastic Hybrid Automaton,SHA),通过验证工具UPPAAL SMC实现自动化的定性和定量安全性质验证。本文以多车道环岛为案例,展现了基于场景的形式化建模和验证方法的实用性和普适性。