不确定环境下hCPS系统的形式化建模与动态验证 |
| |
作者姓名: | 安冬冬 刘静 陈小红 孙海英 |
| |
作者单位: | 上海师范大学信息与机电工程学院,上海201418;华东师范大学软件工程学院,上海200062 |
| |
基金项目: | 国家重点研发计划项目(2019YFA0706404);国家自然科学基金(61972150);上海市知识服务平台(ZF1213);上海市科技计划项目(20ZR1416000) |
| |
摘 要: | 随着科技的进步,新型复杂系统例如人机物融合系统(Human Cyber-Physical Systems,HCPS)已经与人类社会生活越来越密不可分.软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合.物理空间内环境的复杂多变、时空数据的爆发增长以及难以预料的人类行为等不确定因素威胁着系统安全.由于系统安全需求的增长,系统的规模和复杂度随之增加所带来的一系列问题亟待解决.因此,在不确定性环境下,构造智能、安全的人机物融合系统已经成为软件行业不可回避的挑战.环境不确定性使得人机物融合系统软件无法准确感知其所处的运行环境.感知的不确定性将导致系统的误判,从而影响系统的安全性.环境不确定性使得系统设计人员无法为人机物融合系统软件的运行环境提供准确的形式化规约.而对于安全要求较高的系统,准确的形式化规约是保证系统安全的首要条件.为了应对规约的不确定性,本文提出时空数据驱动与模型驱动相结合的建模方式,即通过使用机器学习算法,基于环境中时空数据对环境进行建模.根据安全软件的典型特征,采用动态验证的方式保证系统的安全,从而构建统一安全的理论框架.为了展示方案的可行性,本文以自动驾驶车辆与人驾驶的摩托车的交互场景为例说明了在不确定性环境下的人机物融合系统的建模与验证的具体应用.
|
关 键 词: | 人机物融合系统 机器学习 不确定性建模 形式化验证 统计模型检测 |
收稿时间: | 2020-09-17 |
修稿时间: | 2020-10-26 |
本文献已被 万方数据 等数据库收录! |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|