尽管自主驾驶原型车辆已在结构化程度较高的高速公路上完成测试,但车辆自主决策系统的可靠性依然是这项高新综合技术的重要障碍,特别是在非结构化、复杂的道路环境中,其安全性仍然需要长期验证。由于道路交通环境的动态变化,使得车辆的行驶状态、传感器测量以及车辆模型等存在着复杂的不确定性,而传统的系统仿真与测试验证技术通过有限次仿真计算或实验无法检测车辆所有可能的不确定行为状态。与系统仿真与测试验证技术相比,本文所研究的基于严格数学定义的形式验证方法,不仅能精确、清晰地描述系统结构和相关特性,而且能够求出包含系统所有不安全状态的可达范围,从理论上保证了系统安全性验证的完备性。在验证车辆自主决策系统的安全性时,由于道路交通环境具有开放性和不确定性,使得“车辆自主行为不确定性表现机制”成为一个关键科学问题。为此,本文基于国家自然科学基金面上项目(61573009)《基于形式化与Ad-Hoc方法的车辆自主决策安全性在线验证》,开展如下研究:(1)针对自主车辆安全性验证在理论完备性上无法得到保证的问题,以及在车辆不确定性行为状态建模中存在的问题,提出将自主车辆视为在连续和离散模式间动态切换的混合系统,使用哈密尔顿--雅克比(Hamilton-Jacobi)方程求解车辆运行不安全状态可达范围的研究方法。将车辆运行临界不安全状态定义为目标集,逆时间求解目标集对应的车辆运行不安全状态边界范围(后向可达集),利用具有界面追踪和形状建模数值技术的水平集方法表示目标集和可达集。为了确定目标集在向量场作用下的后向可达集,提出求解Hamilton-Jacobi偏微分方程的粘性解的方法。试验验证结果表明,该方法在理论上能够提高自主车辆安全决策验证的置信水平,增强自主车辆安全性验证的可靠性。(2)将自主车辆追逃问题(二元零和微分博弈)应用到车辆追尾问题,通过可达性分析,理论上计算出不同刹车强度下,两自主车辆为避免发生追尾事故所要保持的最小安全距离,并对误差进行分析及修正,该数据为自主车辆安全性验证提供了理论和数据支持。