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

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

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.