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

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

用样本预测,将线下训练好的模型导出到工作空间,这样就可以利用模型来测试新的数据.

Fig.3 The classification result of different driving style Fig.4 The classification result of confusion matrix
图 3 不同驾驶行为的分类情况 图 4 混淆矩阵结果

Fig.5 The classification result of parallel coordinates plot Fig.6 ROC (receiver operating characteristic)
图 5 分类结果的平行坐标图 图 6 ROC 曲线结果

3 线下与线上验证相结合的动态验证方法

在上一节我们得到 UPPAAL-SMC 可以验证的模型后,通过写入要验证的性质(query),即可对模型进行验
证.但是,目前使用 UPPAAL-SMC 进行验证的时间成本较高,通常需要十几秒钟甚至更长,对于复杂的系统很可
能由于要检测的状态过多而产生状态爆炸的问题.由于本文所研究的无人驾驶系统的物理车辆是行驶在不确
定且复杂多变的场景中,十几秒钟后才能出现的验证结果对于系统来说是难以接受的,若车辆不能及时地对周
边环境做出反应,那么对于无人驾驶车辆来说将造成无法承担的后果.所以我们从机器学习流程中线下训练和
线上学习的过程得到启发,通过采取线下验证和线上验证相结合的方法,比较参数后即可快速得出验证结果,从
而达到动态、实时的验证效果,进而保障系统在复杂环境中能够安全运行.
图 7 显示了线下与线上结合的动态验证方法示意图.上半部分显示的是线下的验证过程,下半部分所示为线
上验证过程.在线下验证过程中,统计模型检测工具 UPPAAL-SMC 接受的是属性和 NSHA 模型,其中所要验证的
属性基于不同场景下的安全需求进行形式化描述而产生,而 NSHA 模型由上一节提出的环境感知模型和线下训
练场景共同建模得到.不断加入新的线下场景进行验证.这样,在线上验证过程中,通过对比相关安全数据,在验证