自动驾驶技术可有效解决社会面临的交通安全、道路拥堵、能源消耗等问题,以提供更舒适的交通环境。早期的自动驾驶技术主要研究特定场景下的驾驶任务,而在目前的城市交通中自动驾驶系统需要满足L3以上的功能。自动驾驶汽车在各种交通环境下的安全性评估是目前的研究热点和持续被关注的问题。其难点在于不同交通场景的分类、大量时空数据的计算、攻击者恶意攻击的预防、以及各种人工驾驶和自动驾驶混合交通造成的环境不确定性和复杂性。本文采用形式化方法研究分析自动驾驶的安全性。形式化方法是一种支持数学逻辑推导证明的严谨手段。通过对系统模型的建模、规约、推理和验证,能够减少模型对主观假设和非特定术语的依赖,所以应用此方法评估自动驾驶汽车的决策安全有着重要的意义。与此同时,基于场景的方法能够显著减少测试范围,二者的有效结合可以有效提高安全验证的效率。随着驾驶环境的复杂度急剧上升,冗余的时空信息也随之密集增涨,导致状态空间爆炸。所以合理的交通场景模型的构建是进行安全评估的基础,同时它也决定了模型对于实际场景的表达能力。其次,决策模型则直接决定所设计模型面对不确定性因素的可行性以及效率。因此,本文针对自动驾驶汽车的特点,结合了形式化方法,在现有研究基础上提出了一种新的安全评估方案,其中包括:（1）本文提出了抽象场景特征的可扩展建模框架。通过稳定的车道邻接关系提取抽象场景特征,可以有效避免已有研究定义路段邻接关系导致逆行路径也被视为合理道路的现象。（2）本文结合静态场景信息和动态驾驶环境提出了一种交通语义表达模型。根据分而治之的思想,结合车辆不断动态聚合的机动行为生成基本语义场景,可以将车辆执行整个驾驶任务的过程转化为语义场景的组合和连接,来实现对大型复杂场景的刻画。相比于已有研究中基于场景几何特征构建基本场景结构的方法,本文所提的模型能够更好的表达场景和决策之间的关联性。（3）本文基于知识库中的先验概率,显示的表达了干扰车辆的随机行为,并提出了基于语义场景的博弈估算模型。通过将系统需满足的性质转化为自动驾驶汽车的收益,其决策结果更加均衡。同时,根据干扰车辆的运动学数据状态的瞬时变化修正估算的随机行为的概率分布至符合实际的干扰车辆的驾驶意图,可以使自动驾驶汽车执行的最优反应足够安全。（4）本文通过将系统模型映射到自动化的模型效验工具UPPAAL SMC,构建了数学可信度计算的形式化验证过程并应用于具体案例分析。本文将上述系统模型应用于针对CAM协议分析出的欺骗攻击案例,展示了场景模型在网络安全评估的实际应用。实验结果表明,本文基于场景的形式化建模方法具有一定的普适性,且系统模型在事故追责问题上具有实用性。