状态不可观测的信息物理融合系统运行时验证

• 作者: 房丙午 李勇 王勇 黄志球
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 信息物理融合系统 运行时验证 隐马尔科夫模型 确定性有限自动机 安全性 反例
• 年，卷（期）: 2018,（12）
• 所属期刊栏目: 学术论文
• 页码范围: 2824-2831
• 页数: 8页
• 分类号: TP311
• 字数: 7182字
• 语种: 中文
• DOI: 10.3969/j.issn.0372-2112.2018.12.002

摘要

确保信息物理融合系统(Cyber-Physical System,CPS)运行时行为正确性是至关重要的,尤其在航空航天、汽车、核电和医疗等安全攸关领域.本文针对具有随机行为且状态不可观测的CPS,提出一种基于隐马尔科夫模型的运行时安全性验证方法.首先构造状态不可观测的CPS运行时安全性验证框架,该框架通过隐马尔科夫模型表示系统,使用确定性有限自动机规约系统安全属性的否定,两者的乘积自动机作为运行时监控器,从而将CPS运行时安全性验证问题约简到监控器上的概率推断问题.然后,提出一种增量迭代安全性验证算法以及反例生成算法.实验结果表明本文算法和粒子滤波算法相比预测错误率下降了近20％,并且当系统违背安全属性时,本文的方法能给出反例.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄志球	南京航空航天大学计算机科学与技术学院	183	1755	20.0	33.0
2	李勇	南京航空航天大学计算机科学与技术学院	142	1840	21.0	37.0
3	王勇	南京航空航天大学计算机科学与技术学院	34	241	9.0	14.0
4	房丙午	南京航空航天大学计算机科学与技术学院	8	75	4.0	8.0