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

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


| s    iff s 
| s     iff | s   and s  | 
1 2 1 2
| s  P ( ) iff Pr( | s  )  p

 p
s|=P⨝ p (ψ)中 P 表示在起始状态为 s 的路径集合中满足路径公式 ψ 的概率,P⨝ p 比较得出的概率 P 与给定的
概率值 p 的对比结果⨝{≤,<,>,≥}是 true 还是 false.给定一个路径公式,第 i 个状态和初始状态分别定义为
[i]和[0].对于路径公式$\psi$的满足关系定义如下:
| X
  iff  [1]|  
k
i
 |   1 U  ≤ k 2 iff i  ,0≤≤
 []|i   _ 2( ,0i i k  [ ]|i   ≤≤ 1 )
1.4 统计模型检测
统计模型检测(statistical model checking,简称 SMC)问题可以描述为:给定一个随机系统模型 M 和一个性质
规约公式,“统计模型检测技术建立在蒙特卡洛(Monte Carlo)模拟技术之上,它能够有效地评估系统模型满足
目标约束的概率区间,对系统进行验证分析”.SMC 算法主要分为定性和定量两种类型,其中,定性算法用来验证
“系统 M 满足约束的概率是否大于或者等于某个概率阈值 p,p[0,1],即 s|=P⨝ p ()”包括:single sampling plan
(SSP)、sequential probability ratio(SPRT)和 Bayesian hypothesis testing(BHT).定量算法用来验证“系统 M 满足约
束 2 的概率是多少,即 s|=P =? ( 2 )”包括 Bayesian interval estimation(BIE)和 approximate probabilistic model
checking(APMC).不同类型的 SMC 算法的主要区别在于统计参数的计算和置信度满足条件的判断这两个方面.

2 基于朴素贝叶斯分类器的人工驾驶风格分类模型

在 hCPS 软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合的情况下,作为人机物融合系
统主体的智能体在与所处的环境不断进行交互的过程中,智能体需要像人一样具有学习能力,拥有“智能性”来
应对各种环境.无人驾驶系统作为 hCPS 的典型应用系统,无人驾驶汽车是集感知、决策和控制等功能于一体的
自主交通工具,其中,感知系统代替人类驾驶过程中人的视、听、触等功能,融合摄像机、雷达等传感器采集的
海量交通环境数据,精确识别各类交通元素,为自动驾驶汽车决策系统提供支撑.在无人驾驶和人工驾驶的混合
交通场景中,由于人类驾驶员在驾驶过程中会疲劳或者分心,这就使得人类驾驶行为很随机.无人驾驶系统由于
高精度的传感、执行、控制,其技术是规定好的,不会退化,在交互过程中,智能化的技术对于未知环境的理解,
其认知理解能力是有限的.而目前的一些无人驾驶设计基于规则驾驶的一些模式来设定,有相关的一些逻辑参
数,在自适应方面包括人性化方面做得很不到位,这就导致无人驾驶和人工驾驶有可能产生一定的冲突.如何保
证系统在不确定的复杂环境下智能运行仍是目前无人驾驶系统设计所面临的挑战.在本节中,为了提高系统的
“智能性”,我们提出了基于朴素贝叶斯分类器的人工驾驶行为的分类模型(drving style classification,简称 DSC).
本节重点介绍人工驾驶行为的分类模型,一方面从环境中接收数据,将环境数据和智能体自身的相关数据
作为模型输入,基于朴素贝叶斯的分类算法对周边人工驾驶车辆的驾驶行为进行分类,学习器的学习结果将作
为参数输入到后续的系统模型中.
无人驾驶车辆在行驶过程中要面对大量的不确定因素,在与人工驾驶的车辆交互的过程中,由于人类驾驶
员在驾驶过程中的驾驶行为具有很强的主观性,所以在无人驾驶车辆的角度来看,驾驶员的行为状态具有一定
的不确定性.例如,面对相同的驾驶环境,不同的驾驶员可能会产生不同的驾驶行为.如果无人驾驶车辆不能及
时、准确地判定周围人类驾驶员的驾驶行为,势必会导致本车进入不安全的状态.因此需要对周边车辆的驾驶
行为进行分析.本节将重点聚焦于对人工驾驶车辆的驾驶风格进行分类.本节的目标是通过无人驾驶与人工驾
驶交互所产生的数据进行分类学习,构建人类驾驶员的驾驶行为分类模型,无人驾驶车辆根据周围人工驾驶车
辆的当前状态来对其驾驶行为进行分类,并预测周边车辆的未来状态.从而指导无人驾驶车辆做出智能决策.为
了实现该目标,本文提出了基于朴素贝叶斯的驾驶行为分类模型,使用有监督的机器学习训练模型以对数据进