自主车辆行为决策的安全验证方法

刘秉政，曹 凯，马建军

（1．山东理工大学交通与车辆工程学院，山东淄博255091；2．中国人民解放军驻上海航天局，上海201109）

混合系统（hybrid system）由连续变量动态系统和离散事件动态系统构成，系统中连续变量和离散事件之间存在相互关联．也就是说，该系统受不同类型离散事件的触发，在各自具有不同动态规律的模式间切换．混合系统广泛存在于商业、工业、交通和军事领域，特别是对安全性要求极高的系统，如车辆、飞机、导弹、核电站等．在这样的系统中一个很小的错误也会造成严重的、甚至灾难性的后果．因此，混合系统的安全验证研究极为重要，且有着重要的科学价值和工程意义，是目前国际上研究热点之一．

融合了认知科学、智能控制、生理学和心理学、机械电子工程、计算机应用、车辆工程、应用数学等学科前沿科研成果的自主车辆是一个对安全性要求极高的混合系统．对这个混合系统的安全验证在模拟人类驾驶员操作经验方面已取得了许多重大成果，但是以系统可达性分析为基础的自主车辆安全验证问题却刚刚起步．目前，国外一些研究者在这一领域已经取得一些的成果：文献［1] 和［2] 给出了在静态环境下，车辆对冲突规避的路径规划方法；对于动态环境，文献［3] 提出通过模拟仿真得到不可避免的冲突区域，并对这些区域进行回避，达到安全行驶的目的．

在国内，自主车辆的安全验证研究主要集中在模拟人类驾驶员操作经验，并且取得了举世瞩目的成果．在面向车辆主动安全的智能驾驶技术方面，国防科技大学与一汽集团联合研制的“红旗旗舰”自主驾驶系统，在高速公路上最高稳定自主行使速度为130km／h，且具备超车功能；吉林大学利用机器视觉系统、三维激光雷达以及GPS实现了紧急制动停车、安全车速转弯、保持安全车距等功能；清华大学研制的THASV－V，采用计算机视觉和雷达作为传感器，能够实现智能巡航、碰撞报警、车道线跟踪等功能；西安交通大学对车辆主动安全中的障碍物检测和分类、驾驶员实时姿态和道路的识别等车辆自主和辅助驾驶关键技术进行研究；上海交通大学联合法国国家信息与自动化研究所、葡萄牙Coimbra大学启动了CyberC3项目，重点研究面向城市环境的无人驾驶车辆，旨在为未来的城市提供一种灵活、高效、安全、环保的新型公交工具［4]．

模拟的最大优点是它能产生一个反例（系统过程轨迹与某一不安全状态相冲突），以此展现一个系统的不安全状态．但是，在没有反例产生的条件下，模拟却无法证明系统是安全的．为此，本文以系统可达性分析为基础，实现对自主车辆所有可能路径的覆盖，研究其行为决策的在线安全验证问题．为了满足在线安全形式验证对时效性的要求，本文对系统状态空间以及输入空间进行离散化，将自主车辆和其他车辆的系统动态抽象为马尔科夫链，实现对车辆状态随机可达集快速计算的目的．

1 系统的形式验证

自主车辆是一个混合系统，它以主动安全为核心，模拟有经验的人类驾驶员的决策能力和行为特征，通过各种传感器感知交通环境，理解和预测交通环境的变化以及目标的意图，规划安全行驶路径，确保车辆安全可靠行驶．由于自主车辆的换道、超车、转弯等逻辑决策行为的动态变化，呈现受事件驱动的离散系统特性，适宜采用离散方法建模；然而在自主车辆的具体决策行为上，车辆的动态特征却又呈现随时间发展而不断变化的连续系统特征，其最佳表达方式则是连续微分方程．因此，在各种不同类型交通事件的触发下，自主车辆在连续和离散模式间动态切换，表现出更加复杂的混合系统的动态行为．然而，目前对于这种混合系统的动态行为安全性验证基本采用两种方法：一是基于人类操作经验或过程的模拟建模技术；二是以系统可达性分析为基础的形式验证技术．由于模拟建模技术从系统的某一初始状态出发，检验系统的一次行为轨迹或操作过程，纵使进行多次模拟仍然可能错过重要的非安全因素；而形式验证技术是在系统模拟的基础上，从系统的某一初始行为状态集合出发，通过计算系统行为可达集，一次性检验所有可能行为轨迹或操作过程，因此可以一次性验证系统的安全性．

安全验证的过程就是自主车辆追踪某一规划路径，同时考虑到各种可能的扰动，以此确定一个行为变化范围（纵向和横向），即可达范围，就这个可达范围推断自主车辆运行状态的变化趋势，并预测未来某一时间间隔内自主车辆的交通行为的安全性．因此，需要计算自主车辆从某一初始运动状态在未来时间段上的随机可达集，以及其它车辆在相同时间段上的随机可达集．判断自主车辆可达集在未来某一时刻与其它车辆可达集的交集状态，如果交集是空集，那么自主车辆在规划路径上的行驶是安全的，否则为不安全，并计算与其它车辆的冲突概率．系统安全验证过程如图1所示．

图1 系统安全验证过程

2 验证过程及基本假设

系统安全验证以自主车辆对环境的感知为依据，因此，给定自主车辆的初始位置、速度以及行驶方向等参数，并依据车辆动态目标位置［5]预先确定自主车辆行驶路径．自主车辆通过传感器获取某一时刻其它车辆的位置、速度等参数，进而对其它车辆的未来行为做出估计．此外，自主车辆可达集的变化范围与趋势以其规划路径为约束，而其它车辆可达集的变化范围与趋势则以自主车辆对其未来交通行为的估计为参考．这种约束和参考的意义在于：整个验证过程以自主车辆的视角来观察道路交通环境，而且可达集变化范围与趋势力图反映车辆的真实行为，避免可达集变化无约束扩展，造成无意义的系统安全验证结果．

对于自主车辆的安全评估而言，预测其它车辆的行为是至关重要的．像人类驾驶员一样，通常自主车辆预判其它车辆行为的前提条件是：

（1）其它车辆必须遵循道路交通法规，以此排除诸如反向车道中的车辆随意闯入自主车辆行驶车道等扰乱交通秩序的违法行为．

（2）其它车辆的行为分两个阶段建模，即路径生成和路径追踪．路径生成可以由诸如车道保持、左／右转向及车道变换等基本行为轨迹构成，图2展示的是车辆接近交叉口即将采取的基本行为轨迹．路径由长度为s，且由满足条件s≤s′≤2s的Bezier线段组成．对于s′约束条件的理由是确保计算的合理性，使到达交叉口的车辆有尽可能大的行为选择空间．

图2 交叉口车辆基本行为轨迹

（3）车辆路径追踪的基本行为由静止、加速、减速和限速行驶等行为构成．

3 模型的建立

3．1 动态目标位置

动态目标位置是自主车辆在跟踪、转弯、超车或避让行驶过程中，依据时间、障碍物位置、距离和方向的变化以及道路线形变化的预判而改变的预期到达位置［5]．它是一个由动态位置坐标和方向组成的向量，即，T＝［xt，yt，θt] ，其中xt和yt为动态目标位置在t时刻的坐标，θt为动态目标位置的车头方向与水平方向的夹角．在本文的研究中，动态目标位置是自主车辆规划路径的终端参照点，它表达了自主车辆根据当前局部交通态势确定下一步将要到达安全位置的决策过程，这一决策过程是依据停车视距分段进行的．于是，本文依据动态目标位置对自主车辆参考路径进行建模．

3．2 自主车辆参考路径

参考路径表达的是自主车辆当前和未来若干时间段内的状态变化，由自主车辆当前状态点、动态目标位置点构成．参考路径依据自主车辆动态目标位置按长度s进行划分，并在交叉路口处满足条件：s≤s′≤2s．依据车辆行驶轨迹的特点，车辆行驶轨迹曲线y＝f（x）应该是连续的，且曲线应具备以下特征：

（1）轨迹曲线分段构成，以便适应道路曲率变化．

（2）轨迹曲线整体是C2连续的．

（3）在轨迹曲线的起点和终点处应当满足条件．

和

其中，x（ts）和x（te）为曲线段起点和终点．

这里选用贝塞尔（Bezier）曲线进行参考路径曲线拟合．由于利用Bezier曲线方程进行轨迹生成时，最主要是利用其切矢量性，即Bezier曲线的起点和终点处的切线方向和特征多边形的第一条边及最后一条边的走向一致，因此生成的轨迹具备车辆行驶轨迹曲线特征．

假设已知自主车辆的初始状态点Ps（x1，y1）和初始速度Vs（朝向角为θ1），自主车辆动态目标点Pe（x4，y4）和速度Ve（朝向角为θ2），则连接Ps和Pe两点的三阶贝塞尔曲线方程为［6]其中，λ为正系数，u的取值范围为［0，1] ．

将式（3）～式（5）代入式（1）和式（2），易证采用该方法进行路径规划，满足式（1）和式（2）的端点条件，即该路径是满足非完整约束的．

3．3 自主车辆模型

由于车辆在机动行驶中车轮与地面之间有不可避免的滚动约束，使得车辆系统成为最典型的非完整控制系统，而链式系统模型可以将非完整系统的难点以简单的形式表达出来，便于在线处理．

这里，自主车辆模型使用一个前轮转向四轮运动模型，即

其中，xt，yt为动态目标位置在t时刻的坐标；φt为动态目标位置的车头方向与水平方向的夹角；v和ω为智能车辆的线速度和角速度．此研究中v是常量，ω则根据上文参考轨迹规划的不同阶段几何表达式而定．这个模型是一类典型的非完整系统，本文采用文献［6] 中将车辆运动模型转化成链式系统模型的方法，根据文献［6] 的推导，设计车辆运动系统（6）的控制如下：

式中，d1，d2为常数，它们对系统有扰动作用，以便当系统初始位置处在奇异点时，能够使其离开奇异点．

3．4 其它车辆模型

本文以自主车辆的视角为观察依据进行在线安全验证，自主车辆通过传感元件感知周围环境中的其它车辆．按照前面的基本假设，其它车辆的路径生成限定为车道保持，因此，对其它车辆车道保持的纵向动态行为采用混合自动机建立一个切换系统模型．混合自动机是描述混合系统的计算模型，它是有限状态自动机的推广，可用来描述和计算具有连续和离散变量的混合系统的行为．建立的切换系统模型由静止、速度限制、制动和加速四个模块以及它们之间的切换关系构成，如图3所示．

模型中I为不变集合，E为切换关系（事件），常数c2表示车辆的速度限制，且模型中的切换关系是单向的，即一次切换发生以后，系统的连续状态随之发生而无法重现．切换系统模型中的制动模型h1（u）与加速模型h2（v，u）的表达式如下：

图3 其它车辆混合自动机模型

式中，常数c1表示最大加速度，常数c3表示车辆速度上限（这一特定指标因车辆类型不同而不同）．需要注意的是，加速模型和减速模型中的输入变量u在其边界内是不确定的，并且切换系统模型的离散动态也包含不确定性．此外，除了切换事件E1和E3以外，其它切换事件E2、E4、E5和E6均以概率Pi（i＝1，2，3，4）随机发生．

4 系统状态空间的近似表达

以上基于混合系统构筑了自主车辆和其它车辆模型，下面对模型状态空间在某一初始条件下的连续变化范围进行系统可达性建模．为此，需要建立和计算系统状态可达集．

给定一个车辆的动态表达式：

这里的x∈Rn表示状态，u∈U表示符合莱布尼兹连续条件的输入．当t＝r时，车辆状态精确可达集Re（t）表示如下：

由于计算系统精确可达集仅适用于特殊案例［7]，因此一般采用超近似计算方法求出Re（r）的近似值R（r），使R（r）⊇Re（r）．因此，某一时间间隔上的超近似可达集可以定义为

于是，如果假设S（0）＝和V（0）＝分别表示车辆初始位移区间和速度区间，则车辆的初始状态可以表示为一种联合状态形式：

那么，车辆的初始状态可达集R（t）就可以用位移与速度二维区间近似表示为X（t）＝的计算方法为

一个马尔科夫链就是由离散状态z∈N＋组成的随机动态系统，它包含离散时间的马尔科夫链和连续时间的马尔科夫链．本文采用离散时间的马尔科夫链，于是，时间t∈｛t1，t2，…，tf｝，其中，tf表示预测时间范围，tk＋1－tk＝T∈R＋为时间步长．马尔科夫链的当前时刻ti状态无法精确表达，而是通过概率pi＝p（ti）描述．那么，设p为概率分布向量，下一时刻ti＋1概率分布向量p可以表达为前一时刻ti概率分布向量的线性组合，即

其中，Φ（T）是马尔科夫过程的转移矩阵．这里，马尔科夫模型的建立分为两个步骤：（1）将初始连续系统的状态空间分割为若干栅格，以此对系统状态空间离散化．具体地说，按照车辆的等间隔位移s（与路径划分一致）和速度v间隔构成的矩形栅格，由位移s和速度v构成一个二维离散状态空间．（2）计算由一列栅格转移到另一列栅格的概率，并将结果储存到马尔科夫转移矩阵中．具体过程如下：

（1）状态空间和输入空间的划分：将连续状态空间X⊂R2分割为若干均等矩形栅格Xi，下标i表示相应的离散状态，每个栅格上的系统状态坐标（x1，x2）定义为（s，v）．于是，依据式（13）的定义，栅格Xi可以用二维区间Xi＝近似表示，即系统的状态空间可以近似表示为：X＝∪Xi．类似地，将车辆动态表达式（10）的输入空间U⊂R分割为若干区间Uα，即U＝∪Uα，其中上标α表示相应离散输入值．

（2）马尔科夫链的转移概率：马尔科夫链的转移矩阵中储存的是该系统从状态i到状态j的转移概率Φji（如图4所示），其中Φji（T）＝p（z（tk＋1）＝j｜z（tk）＝i），而且这一转移概率也取决于离散输入值α．因此．对于每一个离散输入α需要计算一个不同的转移概率矩阵Φα．为了计算转移概率（T），假设（T）表示在输入u∈Uα的影响下，由初始状态x（0）∈Xi出发，在时间T处的可达集．因此，可以通过计算可达集（T）得到转移概率的值．为此，本文利用MATLAB的混合系统验证工具箱Checkmate作为运算平台，计算可达集（T），从而求得转移概率．需要注意的是，可达集（T）［8]中的时间T与马尔科夫链的时间步长增量T是相等的，而且由栅格i出发，经过时间T后，到达栅格j的转移概率（T）等于该时刻可达集与栅格j交集，∩Xj），所占的几何容积比为

其中V（）表示容积算子．

图4 状态空间的分割及转移

由式（16）可以看出，只有当可达集到达某一栅格时，到达这个栅格的概率才是非零的．这就意味着转移概率矩阵只会储存当前到达栅格的概率，并替代了此前到达这个栅格的信息．因此，具有非零概率的马尔科夫链可达栅格能够超近似表达对应的可达集与超近似可达集相比，在式（16）中假设的可达集范围内这些概率本身是以系统状态均匀分布的形式近似表达的，即马尔科夫链可用于表达某时刻对应可达集上的系统状态（如图5所示）．

图5 马尔科夫链对可达集的近似

5 在线验证

系统状态空间离散划分之后，随机可达集完全可以由马尔科夫链的概率向量p表达．由于公式（15）只能针对马尔科夫链进行单次推演计算，而本研究需要根据不同的离散输入α、时间点以及时间间隔条件建立马尔科夫链，因此，必须扩展公式（15），即对于一个给定的输入α，依据某一个时间点处分布状况计算某一时间间隔内的概率分布．于是，时间点处的概率分布可以作为时间间隔计算的支持，即

计算自主车辆与其它车辆在规定时间内的马尔科夫链，检验两者的可达集是否相交，若相交，计算得出相交概率，即冲突概率．为了更好地验证上述提出的方法，本文给出一个如图6所示的典型交通情形．图6中，自主车辆保持匀速行驶，其既定行驶路线前方有一个固定障碍物，而且反向车道也有车辆驶来，自主车辆在判断反向车道车辆位置和速度的基础上，规划躲避障碍物轨迹，并依据式（19）进行马尔科夫链推演计算．为此，给出参数设定如下：

图6 假设交通场景

自主车辆参数设定：自主车辆均匀行驶速度v＝15m／s，起始位置x0＝［1．8，2．2] m，y0＝［3，6] m，φt＝0＝［－0．01，0．01] rad．

未知车辆参数设定：起始速度v∈［3，8] m／s，起始位置s∈［75，80] m，最大加速度c1＝15m2／s，速度限制c2＝15m／s，速度上限c3＝60m／s．加速输入u∈［0．2，0．4] ，减速输入u∈［－0．4，－0．2] ；由图3可知，未知车辆的行为状态含有4个模块，根据起始速度的设定，未知车辆可进入的状态只包含在加速模块和减速模块中，考虑到未知车辆行为信息的不确定性，此处假设加速模块与减速模块的发生概率分别为p加＝0．5和p减＝0．5；事件切换概率分别为p1＝p2＝p3＝p4＝0．5．根据以上初始条件，对所有车辆在时间间隔［0，3．2] s上的随机可达集做出分析预测，并进行安全验证．

验证结果如图7所示，线条表示采用贝塞尔曲线对自主车辆蔽障给出的参考路径拟合曲线，自主车辆与其它车辆在给定时间范围内的道路占有概率分布由阴影方块表示，其中颜色深处表示车辆中心和车体中心的概率分布．在预测时间间隔［0，3．2] s内，当t∈［2．4，3．2] s时自主车辆与其它车辆的冲突概率为0．01，其他时间段内的冲突概率为0，从而验证了自主车辆蔽障行为安全．

6 结束语

本文将交通参与者的行为建立为混合系统模型，并通过分析系统在初始条件下的可达状态即可达集来进行在线安全验证，并且考虑到交通参与者的行为中存在的诸多随机因素，提出利用马尔科夫链对交通参与者行为的随机过程进行表示，这种表示方法的应用不仅将随机因素考虑在内，而且可以大大地缩短在线验证的时间．

图7 车辆蔽障安全验证示意图

例证表明了此研究提出的方法对于冲突概率的计算具有良好的时效性．如果遇到更加复杂的情况，适当地扩大起始状态的划分单元，便可实现简便与快速的计算，这就使得此方法可以广泛地运用于诸多交通环境下的安全验证．

［1] Iwan U，Johann B．VFH＊：Local obstacle avoidance with lookahead verification［C] ／／Proceedings of the IEEE Int．Conf．Robotics Automation，2000：2 505－2 511．

［2] Adrian B，Simon B，Takeo K．A prediction and planning framework for road safety analysis，obstacle avoidance and driver information［C] ／／Proceedings of the 11th World Congress on Intelligent Transportation Systems，2004：270－277．

［3] St′ephane P，Thierry F．Safe motion planning in dynamic environments［C] ／／Proceeding of the IEEE－RSJ Int．Conf．on Intelligent Robots and Systems，2005：3 512－3 518．

［4] 徐昕，贺汉根，蔡自兴，等．车辆智能驾驶技术的研究前沿与展望［C] ／／中国自动化大会暨两化融合高峰会议．杭州：2009．

［5] 曹凯，于少伟，周芦芦．基于动态目标位置的智能车辆控制研究［J] ．信息与控制，2008，37（4）：476－480．

［6] 曹凯，周芦芦．车辆弯道机动驾驶控制算法［J] ．信息与控制，2011，40（2）：262－267．

［7] Gerardo L，George J．P，Sergio Y．A new class of decidable hybrid systems［C] ／／Proceedings of the 10th International Conference on Hybrid Systems：Computation and Control，1999：137－151．

［8] 刘秉政，曹凯．基于混合自动机的车辆控制建模及可达集分析［J] ．山东理工大学学报：自然科学版，2010，24（增）：72－75．

［9] Matthias A，Olaf S，Martin B．Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization［C] ／／Proceedings of the 47th IEEE Conference on Decision and Control，2008：4 042－4 048．