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

2012 Journal of Software 软件学报 Vol.32, No.7, July 2021

个贝叶斯深度学习框架,并在模拟场景中展示了它相对于传统方法的优势.该方法是每个模块在系统中的传递
和输入都服从概率分布函数,而不是一个精确的结果.另一种方法是单独评估驾驶场景下的风险水平.可以理解
为,前者是从系统内部进行评估,后者是从系统外部进行评估.Yamazaki 等人 [26] 将传感器数据输入到一个风险推
理框架中,利用隐马尔可夫模型(hidden Markov model,简称 HMM)和语言模型检测不安全的车道变更事件.
Yurtsever [27] 引入了一个深度时空网络来推断驾驶场景的总体风险水平,从而评估车道变更的风险水平.牛津大
学的 Wu 等人 [28] 提出了基于双方回合博弈的(two-player turn-based game)框架来对神经网络加以验证,用于评估
安全攸关自动驾驶系统对交通标志识别的准确性.Wicke 等人 [29] 研究了对抗性输入扰动下的贝叶斯神经网络
BNN 的概率安全性,基于非凸优化的技术,开发了用于计算概率安全性的算法框架,从而验证具有数千个神经元
的概率安全性并应用于自动驾驶系统.Huang 等人 [30] 提出了可以表达社会信任概念(如能力、性格和依赖性)的
算子,将扩展逻辑 PCTL*变为概率理性时间逻辑 PRTL*,建立了一个基于人的信任度的模型验证框架,可用于自
动驾驶系统以根据行人的反应进行决策.Sun 等人 [31] 通过将覆盖率指导的神经网络测试工具 DeepConcolic 与
车辆跟踪系统集成,对深度神经网络(deep neural network,简称 DNN)进行了验证.伯克利大学的 Sanjit 等人 [32] 提
出了一种通过深度强化学习来改善布尔逻辑回溯搜索算法的方法,这是一种对使用 ML 进行感知的系统进行形
式分析的方法.在基于深度神经网络的感知组件上显示了该技术的有效性.实际环境中的自动驾驶决策还有周
围驾驶员的意图与行为相关.目前,该技术在自动驾驶领域尚不常见.Geng 等人 [33] 用隐马尔可夫模型(HMM)对
目标车辆的未来行为进行了预测,通过学习人类驾驶特征,将预测时间范围延长了 56%.这里,主要是利用了预定
义的移动行为来标记观测值,然后再使用 HMM 以数据为中心学习每种类型的特征.除此之外,还有一些其他方
法,比如贝叶斯网络分类器、混合高斯模型和隐马尔可夫模型相结合 [34] 、支持向量机等.这一类评估的主要问
题在于观测时间短,实时计算量要求高,大多数情况下,自动驾驶系统只能观测周围车辆几秒钟,因此不能使用
在需要较长观察周期的复杂模型中.
针对不确定性的模型检测技术,关于随机模型检验的研究开始于 20 世纪 80 年代初,Harts 等人 [35] 使用离散
时间马尔可夫过程建模概率程序,研究概率并发程序的终止性质和概率程序性质的证明方法.Vardi 等人 [36,37] 提
出基于自动机理论的定性线性时间性质的验证方法,Courcoubetis 和 Yannakakis [38] 研究了线性时间框架下的定
性、定量验证理算时间马尔可夫链.英国牛津大学的 Kwiatkowska 团队开发出图形化随机模型检验工具
PRISM [39] ,该工具可以验证包括 DTMC、CTMC、MDP、PA、PTA 及其 reward 扩展模型等多种类型的随机系
统模型,其性质规约包括 PCTL、CSL、概率 LTL、PCTL*及其 reward 扩展等定量性质规约语言.PRISM 基于
BDD(binary decision diagram)和 MTBDD(multi-terminal binary decision diagram)的符号数据结构和算法 [40] ,通
过离散事件模拟引擎来实现定量抽象精化和系统归约等验证技术,支持多目标定量性质的随机模型检验和统
计随机模型检验 [41] .德国亚琛工业大学的 Hartmanns 等人提出了支持验证随机混成自动机、随机时间自动机的
工具集 MODEST [42] .通过为现有语言提供导入和导出功能,允许重复使用现有模型;并通过将它们集成在统一
的建模和分析环境中而允许重复使用现有工具.MRMC(Markov reward model checker) [44] 采用基于系数矩阵的
数据结构和算法 [43] ,支持精确的 on-the-fly 稳态检查和互模拟最小化等验证技术,其优势在于验证规模较小的连
续时间随机系统的稳态性质效率较高.Katoen 等人近年来开发的工具 Storm [45] 支持对马尔可夫链和马尔可夫决
策过程的离散和连续时间变体进行分析,支持包括 JANI 和 PRISM 建模语言、动态故障树、广义随机 Petri 网
和概率保护的命令语言.模块化设置可以轻松交换求解器和符号引擎,通过封装 Python API 使得 Storm 工具可
以使用扩展的算法来实现快速原型制作.丹麦乌普萨拉大学的研究人员 Larsen 和 David 等人基于随机混成自动
机 SHA,开发了统计模型验证工具 UPPAAL-SMC [46] ,统计模型检测是一种高效的验证技术,常用于复杂的随机
系统验证.该工具所采用的技术主要是参数估计式和假设检验.目前使用上述工具所进行建模的系统需要设计
人员在建模初期就确定好参数,以便验证.但在不确定性环境中,参数是不断变化的,采用这种验证方法无法满
足时效性的要求.目前结合机器学习的统计验证模型框架的相关工作比较少,还缺乏统一的理论框架.