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

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

减少事故的发生.机器学习可以帮助我们提高系统的“智能性”,但是并不能保证系统的“安全性”.数据驱动的方
式可能会由于某个数据的变化导致学习出的结果是错误的,从而产生无法预料的后果,这对安全的系统是不可
接受的 [68] .该方案显示出了对于数据的敏感性,由于机器学习算法本身可解释性较差的缺点导致系统无法预
知所学习的结果.所以,仅仅依靠机器学习的方法无法保证无人驾驶系统的安全性.目前,无人驾驶由于安全问
题的不断出现仍然面临巨大的挑战.2016 年,一辆特斯拉汽车由于传感器失灵没有及时感知到前方的障碍物而
[9]
与之发生碰撞 .2018 年,Uber 的无人驾驶汽车由于夜间识别能力较差没有及时感知到前方的行人而加以避让
从而发生车祸事故,导致行人的死亡 [10] .城市交通环境日趋复杂,面对自动驾驶场景复杂多变、时空数据的爆发
以及其他人工驾驶车辆的主观驾驶行为所导致的环境中不确定性的增加,因此,如何避免事故的发生以保证
系统的“安全性”仍是目前的研究难点.
随着 hCPS 应用空间的扩大,开发具有安全保证的设计框架至关重要.在对 hCPS 建模的过程中,需要重点考
虑 hCPS 动态行为的 3 个特性.(1) 混成性:hCPS 依赖行为离散的计算系统,同时也依赖行为连续的物理环境(例
如:连续的温度变化、时间及空间的变化等),其异构的本质导致其行为具有混成性;(2) 随机性:hCPS 系统处在
开放的环境中,不确定的环境(例如:环境中人的行为不确定、用户的行为不确定以及天气的变化等),造成 hCPS
的行为具有随机性;(3) 安全性:hCPS 经常被用于安全攸关的系统(例如:智慧医疗系统、列车控制系统和智能驾
驶系等),因此需保证 hCPS 的行为必须是安全可信的.
形式化方法(formal method,简称 FM)是基于严谨的数学(逻辑)语言和精确的数学语义的方法学,主要应用
于对系统软件进行建模分析和验证等工作,以保证系统的正确运行 [11] .面对系统规模的扩大和复杂度的增加,形
式化方法越来越频繁地被应用于安全攸关软件的验证,以此来保证其安全性 [12,13] .模型检测(model checking,简
称 MC)是通过对系统的状态空间进行全遍历,从而对系统的安全性进行自动验证 [14] ,其本质是将一个过程或系
统抽象成一个有穷状态机模型加以分析验证.传统的模型检测由于状态爆炸的问题,增大了对系统进行分析验
证的难度.统计模型检测技术(statistical model checking,简称 SMC) [15] 可以通过评估系统所满足的概率区间对
系统进行定量分析,从而有效地解决状态过多而难以验证的问题 [1618] .统计模型检测是一种高效的验证技术,常
用于复杂的随机系统的验证.该工具所采用的技术主要是参数估计式和假设检验.其中,参数估计是基于所收集
到的足够的样本,给出模型满足给定性质的近似概率,属于定量的结果;而假设检验是基于样本给出模型是否满
足给定的性质,属于定性的结果.本文主要考虑人类驾驶车辆和自动驾驶车辆共存的混合交通流下的驾驶环境,
由于人的行为以及物理环境,从而导致不确定性因素的增加.而 UPPAAL-SMC 具有定性和定量分析的能力,能
够分析验证出自动驾驶车辆的相对安全性,因此,本文选用 UPPAAL-SMC 作为自动验证工具.
本文采用时空数据驱动的方法来处理环境的不确定性,目前,针对安全攸关 hCPS 的建模与验证还缺乏统
一、系统的理论、方法.围绕“不确定环境下的人机物融合系统的建模与验证”这一关键科学问题,提出了以数据
驱动和模型驱动相结合的创新方式构建不确定环境下的 hCPS,并对其关键支撑技术进行创新性研究.
(1) 针对系统所处的物理环境的不确定性,应用机器学习技术,以环境中的时空数据为驱动、环境感知计算
为切入点,提出了不确定环境下的基于朴素贝叶斯的人类行为分类模型.
(2) 为了应对大规模系统的结构化建模,构建了不确定环境场景下的 hCPS 系统模型,使用验证工具
UPPAAL-SMC 实现对模型的动态验证.
(3) 提出基于统计模型验证的运行时动态验证技术,采取线下和线上验证相结合的方法,即通过比较参数
即可快速得出验证结果,从而达到动态、实时的验证效果,进而保障系统在复杂环境中的安全运行.
本文以构建安全智能的人机物融合系统的理论框架及应用作为主要的研究目标.第 1 节主要介绍所涉及
到的一些背景知识,包括概念及其主要应用.第 2 节介绍不确定环境下的感知模型,针对系统所处物理环境的不
确定性,应用机器学习算法,以环境的时空数据为驱动,提出不确定环境下的基于朴素贝叶斯的人类驾驶行为分
类模型.第 3 节提出线下与线上验证相结合的动态验证方法,即通过验证工具 UPPAAL-SMC 实现对模型的动态
验证,从而定量评估不确定性环境以及人的行为对系统安全性的影响.第 4 节对相关工作进行比较.最后总结全
文,并对未来值得关注的研究方向进行初步探讨.