针对传统算法在车辆自主决策安全性验证中置信水平较低、验证结果不完备的问题,本文基于形式化的可达性方法分析车辆自主决策行为状态的可行性,并给出车辆自主决策的行为状态完备性集合。采用有向凸多面体算法对自主车辆非线性混合系统进行保守线性化处理,再利用迭代原理和Zonotope近似方法计算可达集。本文得到以下三个在不同道路环境下自主车辆安全性验证结果:一、城市狭窄道路多自主车辆避让的仿真实验表明,在采用A*算法的路径规划后得到各自主车辆的参考轨迹,在初始状态集和传感器噪声边界条件下,在简单估计跟踪器控制下,多辆自主车辆的位置可达集给出了高置信水平的安全保证,并且在分析各自主车辆可达集与不安全集交集后计算了各自主车辆在此过程中的不安全系数。二、变道避碰的仿真实验表明,采用优化遗传算法的路径规划后得到各自主车辆的参考轨迹,在初始状态集和传感器噪声边界条件下,在横、纵向轨迹跟踪器控制下,自主车辆位置可达集和速度可达集给出了高置信水平的安全保证,证明变道避碰环境下,自主车辆能够安全、合规的完成自主驾驶。三、多自主车辆超车避碰的仿真实验表明,在采用A*算法的路径规划后得到各自主车辆的参考轨迹,在初始状态集和传感器噪声边界条件下,在基于ADRC自主车辆的轨迹跟踪控制器控制下,自主车辆位置可达集和速度可达集给出了高置信水平的安全保证,证明超车避碰环境下,多自主车辆都能够安全、合规的完成自主驾驶。本文所包含的创新点:1.本研究将车辆自主决策系统作为混合系统,提出利用形式化方法验证车辆自主决策系统的安全性,并在此基础上利用可达集表达车辆自主行为状态。通过自动化遍历、求解系统的完整状态空间,从理论上保障了自主车辆自主驾驶过程中系统安全性验证的完备性;2.本研究提出利用zonotope表达方式近似计算可达集,进行可达集可视化表达,方便、直观地检测自主车辆的位置、速度等参数;3.本研究在CORA工具箱基础上,开发了可运用到复杂的道路几何形态和车辆自主控制方式变换中的计算方法,利用此方法可以很好的计算出自主车辆各种运行参数;