基于形式化与Ad-Hoc方法的车辆自主决策安全性在线验证

Although fully functioning tests of autonomous vehicle has been completed, but the security of autonomous decision-making system for vehicle need to be verified when it will be faced with complex traffic environment. However, the testing and the system simulation technology for safety verification at present are not enough to guarantee the creditability of safety testing, and the completeness is little protection from the theory. Based on the theory of formal verification, this project propose new ideas on the formal method and Ad-Hoc artificial potential field integrated modeling, its purpose is to establish a theory and method system of online security verification for autonomous vehicle and other traffic participants interaction in the open-loop system. Through the establishment of "the reachable set potential field" of autonomous vehicle driving state and "stochastic reachable set potential field" of motion state for other traffic participants, the mechanism and the influence degree to affect the safety of autonomous vehicle decision by interaction behavior of the multi traffic participants is revealed, and the dynamic change of direction and trend for micro situation of road traffic safety is predicted. Additionally, for the real-time maneuvering trajectory generation and control of the vehicle being tightly coupled, maneuvering trajectory database tracked by autonomous vehicle is constructed, and a integrated modeling method of real-time trajectory generation and tracking control is also designed. Last, the continuous state space and continuous input space of system is gridded by the Euler discretization technique, Markov chain off-line calculation and on-line verification of the operation mechanism is put forward.

尽管完整功能的自主车辆已测试完成，但面对复杂的交通环境，车辆自主决策系统的安全性扔需要验证。然而目前的测试和系统仿真安全验证技术还不足以保证安全检测的可信性，而且完备性难以从理论上得到保障。本项目从形式验证理论出发，提出将形式化方法与Ad-Hoc方法集成建模的新思想，旨在建立自主车辆与其它交通参与者动态交互开环系统的在线安全验证理论方法体系。主要研究的科学问题：1）通过建立自主车辆行驶状态的“可达集势场”和其它交通参与者运动状态的“随机可达集势场”，揭示多交通参与者交互行为对自主车辆决策安全性的影响机制及影响程度，预测道路交通微观态势动态变化方向和趋势；2）构建自主车辆路径追踪机动轨迹库，设计实时轨迹生成和追踪控制一体化的建模方法，将车辆的实时机动轨迹生成与控制紧密耦合在一起；3）利用欧拉离散化技术将系统连续状态空间和连续输入空间栅格化，提出了马尔科夫链离线计算和在线组合验证的操作机制。

在非结构化的、复杂道路环境中，车辆自主决策系统的安全性依然需要可靠的验证方法。本项目基于上述现实背景，将立项研究内容拆分为如下具体问题开展了相关研究：.1. 车辆混成行为安全验证机理研究。分析了车辆随机混成系统自主安全决策行为特征，阐述了其行为特征演化规律和表征方法，建立了车辆自主决策行为安全验证的形式化验证理论与方法。.2. 车辆自主行为不确定性建模研究。针对各种交通事件随机扰动，以及车辆初始状态、传感器测量和车辆模型参数等系统输入存在不确定偏差，提出车辆自主行为不确定性随机可达集建模方法，以此遍历车辆不确定的混成行为，为全面、准确地描述自主车辆不确定行为提供了一种有效表现手段。.3. 交通参与者互动影响下的行驶安全度研究。通过车辆自主行驶状态的可达集与目标集的交集状态及程度的表达方式，提出交通参与者互动影响下的安全影响程度等级划分方法，依据可达集的延展变化推断交通参与者不确定安全影响的变化趋势。.4. 自主车辆的实时机动轨迹生成与控制。通过构建车辆自主决策安全目标位置可达集以及车辆不确定初始状态集，在可达集内计算反映车辆不确定行为的轨迹束，在优化自主车辆机动轨迹的基础上，提出车辆行为实时控制方法。.5. 交通参与者随机交互行为可达集组合建模。借鉴Ad-Hoc组网思想，提出了将随机可达集势场与Ad-Hoc方法集成建模，以便形成一个车辆交互动态的局域网络。.6. 交通参与者不确定混成动态的概率近似。采用了将系统混成连续动态抽象为马尔科夫链随机离散动态的方法，将系统一般可达集扩展到随机可达集..7. 随机可达集计算方法。依据随机可达集动态隐式曲面演变特征，提出采用具有界面追踪和形状建模数值技术的水平集计算方法，通过求解Hamilton-Jacobi偏微分方程的粘性解，确定在向量场作用下的随机可达集隐式曲面演变形态。.8. 系统安全验证分析与评价。通过计算机与智能小车、无人机组成的多车（机）交互式模拟系统，采集仿真道路场景数据，分析验证系统参数、数据和模型，调整了模型误差，评价系统模型的稳定性和可靠性.