Page 93 - 《软件学报》2021年第7期

安冬冬 等:不确定环境下 hCPS 系统的形式化建模与动态验证 2011

Fig.13 The probability distribution and cumulative distribution of P2 for aggressive driver
图 13 当学习出的结果是 aggressive driver 时,P2 性质的概率密度分布和累积分布情况

3.3 采用参数比较法进行动态验证
在上一节我们得到 UPPAAL-SMC 可以验证的模型后,通过写入要验证的性质,即可对模型进行验证.上一
小节的验证都是线上验证的,通过设置不同的参数,可以对同一个模型进行多次验证,得到不同的验证结果.由
于在风险等级较高的环境中,需要保证车辆的安全,但是验证时间在二十几秒之后才能得到,这对于系统来说是
难以接受的.若车辆不能及时地对周边环境做出反应,那么对于无人驾驶车辆来说将造成无法承担的后果.对于
场景 A,Probability uncertaintyϵ 参数为 0.01,我们得到了验证结果.那么,我们将其存入场景库中.在车辆实时运行
在场景 B 中,如果场景 B 的大部分指标与 A 相同,个别项比场景 A 还要宽松,例如在相同环境下,人流量相对于场
景 A 较少.那么,我们就不再需要对场景 B 进行耗时的线上验证,而只需参考场景比 B 更严格的场景 A 的验证结
果即可.这种参数对比方法,大大节省了线上验证的时间,获得了动态实时的验证效果,进而保障了系统在复杂
环境中的安全运行.在得到验证结果后,接下来就是决策阶段,基于不同的驾驶环境,无人驾驶车辆根据验证结
果来决定是否改变车道.
(1) 当车辆行驶在高速公路上,车速大于 80km/h 时,车辆换道的概率大于 95%.
(2) 当车辆行驶在城区,车速小于 30km/h 时,车辆换道的概率大于 80%.
例如,上面案例中 P1 的结果为 90%,如果所处的场景为高速公路,90%<95%,所以不能完成变道.如果所处的
场景为城区,90%>80%,可以进行变道.可见不同场景下指定不同的动作阈值可以保证系统在更安全的情况下进
行决策并决定未来状态.
本节以无人驾驶车辆与人工驾驶车辆交互过程中的变道过程为案例,首先基于上一节提出的基于机器学
习的环境感知模型得到驾驶风格分类结果,接着基于 SHA 模型对无人驾驶汽车的运动状态进行了建模,并使用
统计模型检测工具 UPPAAL-SMC 来验证所建立的 NSHA 模型.

4 相关工作比较

目前,对于驾驶风格识别的研究尚处于起步阶段.人与机器最大的不同在于人是有情绪的,有些驾驶员比较
激进,有些比较稳重.2016 年,谷歌公司的自动驾驶汽车在换道时与迎面而来的巴士相撞,原因就是自动驾驶汽
车以为巴士会减速,而巴士司机却加速行驶.如果能够事先知道司机的驾驶风格,并结合进行预测,这场事故也
许是可以避免的.当然,驾驶风格目前还没有一个准确的定义,因此分类的依据也有很多种,比如油耗、均速、跟
车行为等.目前,还没有将驾驶风格识别成功应用到真实的自动驾驶系统的相关报道,但是这些研究可能是未来
自动驾驶发展的一个方向.
2011 年 11 月 15 日,首个适用于汽车电子电器相关产品的功能安全标准 ISO 26262 正式发布.功能安全的
设计议题在汽车领域开始受到重视.为了更好地量化驾驶场景的不确定性和风险水平以提高自动驾驶系统的
安全性,Geng 等人 [24] 提出了利用贝叶斯方法来量化深度神经网络不确定性的方法.Gadepally 等人 [25] 设计了一