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

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

3.1 构建NSHA模型
将无人驾驶车辆进行建模,UPPAAL-SMC 可以进行验证 NSHA 模型.所构建出的 NSHA 模型由 5 个子模型
组成,分别是组合模型 Composite、开始模型 Start、风险模型 EnvRisk、人工驾驶模型 HumanDrive 和无人驾驶
模型 Autodrive.因此,随机混成自动机网络可以表示成:
ChangeLane  Composite  Start  EnvRisk  HumanDrive  Autodrive.
图 8 表示复合状态抽象成的 SHA 模型,主要包括 STOP、STRAIGHT 和 CHANGE_LANE 这 3 个状态和两
个 Urgent 状态,在 Urgent 状态中时间不流失,会跳转到下一个状态.受篇幅所限,其他 SHA 模型的建立过程详见
https://github.com/DongdongAn/DrivingStyleClassification.git,这里不再一一列举.

Fig.8 Composite state of SHA model
图 8 复合状态抽象成的 SHA 模型
3.2 采用UPPAAL-SMC对NSHA模型进行验证
建立好 NSHA 模型后,接下来是对其进行验证.首先需要结合 PCTL 公式定义所要验证的性质,见表 3.
(1) P1 表示在 15 个时间单位内人工驾驶车辆允许无人驾驶车辆通过的概率.当人工驾驶风格分类模型预
测结果为 normal driver 时,图 9 表示在模拟了 1 305 次之后,所得的概率区间是[0.549862,0.609859],其中,置信度
为 0.97.概率密度分布和累积分布如图 10 所示.图中的 x 轴表示时间,y 轴分别表示概率密度和概率.图 11 表示,
当人工驾驶风格分类模型预测结果为 aggressive driver 时,概率密度分布和累积分布的情况.
Table 3 Property list
表 3 性质列表
序号 性质
P1 Pr[<=15] (<> HumanDrive.LET_PASS)
P2 Pr[<=30](<>AutoDrive.CHANGE_LANE)

Fig.9 The verification result of P1 for normal driver
图 9 当学习出的结果是 normal driver 时性质 P1 的验证结果