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

doi:10.3969/j.issn.0372-2112.2018.12.002

电子学报 ›› 2018, Vol. 46 ›› Issue (12): 2824-2831.DOI: 10.3969/j.issn.0372-2112.2018.12.002

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

房丙午^1,2, 黄志球¹, 王勇¹, 李勇¹

1. 南京航空航天大学计算机科学与技术学院, 江苏南京 210016;
2. 安徽财贸职业学院云桂信息学院, 安徽合肥 230061

收稿日期:2018-05-03 修回日期:2018-07-15 出版日期:2018-12-25
- 通讯作者:
- 黄志球
- 作者简介:
- 房丙午 男,1974年生于安徽枞阳.现为南京航空航天大学计算机科学与技术学院博士研究生,副教授.主要研究方向软件工程、软件系统安全性分析.E-mail:bingwufang@163.com
- 基金资助:
- 国家重点研发计划 (No.2016YFB1000802）; 国家自然科学基金资助项目 (No.61772270）; 安徽省高校自然科学基金重点项目 (No.KJ2017A859）; 安徽省高校学科 (专业）优秀拔尖人才学术资助计划 (No.gxbjZD32）

Runtime Verification of States Unobservable Cyber-Physical System

FANG Bing-wu^1,2, HUANG Zhi-qiu¹, WANG Yong¹, LI Yong¹

1.College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, Jiangsu 210016, China;
2.School of YunGui Information, Anhui Finance and Trade Vocational College, Hefei, Anhui 230601, China

Received:2018-05-03 Revised:2018-07-15 Online:2018-12-25 Published:2018-12-25
- Corresponding author:
- HUANG Zhi-qiu
- Supported by:
- National Key Research and Development Program of China (No.2016YFB1000802); National Natural Science Foundation of China (No.61772270); Key Program of Natural Science Foundation for Colleges and Universities in Anhui Province (No.KJ2017A859); University Discipline (Major) Top-notch Talent Support Program of Anhui Province (No.gxbjZD32)

摘要/Abstract

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

关键词: 信息物理融合系统, 运行时验证, 隐马尔科夫模型, 确定性有限自动机, 安全性, 反例

Abstract: Ensuring the correct behavior of cyber physical systems (CPS) at runtime is critical, and it is more so in safety-critical area, such as aerospace, automotive, nuclear power and medical. A method of runtime safety verification based on hidden Markov model (HMM) is proposed for the CPS with stochastic behavior and unobservable states. First, a runtime safety verification framework of the CPS is constructed where the system model is represented by HMM, and the negation of safety property is specified by deterministic finite automaton (DFA), and then the product automata of DFA and HMM is used as a runtime monitor. Thus, the problem of CPS runtime safety verification is reduced into a probabilistic inference problem on the monitor. Second, an incremental iterative safety verification algorithm and a counterexample generation algorithm are proposed. The experimental results show that the prediction error rate of the safety verification algorithm is nearly 20% lower than that of the particle filter algorithm. When the system violates the safety property, the proposed method can product a counterexample which the particle filtering method cannot do.

Key words: cyber-physical system, runtime verification, hidden Markov model, deterministic finite automaton, safety, counter-example

中图分类号:

TP311

房丙午, 黄志球, 王勇, 等. 状态不可观测的信息物理融合系统运行时验证[J]. 电子学报, 2018, 46(12): 2824-2831.

FANG Bing-wu, HUANG Zhi-qiu, WANG Yong, et al. Runtime Verification of States Unobservable Cyber-Physical System[J]. Acta Electronica Sinica, 2018, 46(12): 2824-2831.

参考文献

[1] 黄志球,徐丙凤,阚双龙,胡军,陈哲.嵌入式机载软件安全性分析标准、方法及工具研究综述[J].软件学报,2014,25(2):200-218. Huang ZQ,Xu BF,Kan SL,Hu J,Chen Z.Survey on embedded software safety analysis standards,methods and tools for airborne system[J].Journal of Software,2014,25(2):200-218.(in Chinese)
[2] Chen F,Ye H,Yang J,et al.A standardized design methodology for complex digital logic components of cyber-physical systems[J].Microprocessors & Microsystems,2015,39(8):1245-1254.
[3] Zheng X,Julien C,Chen H,et al.Real-time simulation support for runtime verification of cyber-physical systems[J].ACM Transactions on Embedded Computing Systems,2017,16(4):106.
[4] Jiang Y,Song H,Wang R,et al.Data-centered runtime verification of wireless medical cyber-physical system[J].IEEE Transactions on Industrial Informatics,2017,13(4):1900-1909.
[5] Medhat R,Bonakdarpour B,Kumar D,et al.Runtime monitoring of cyber-physical systems under timing and memory constraints[J].ACM Transactions on Embedded Computing Systems,2015,14(4):79-108.
[6] Yu K,Chen Z,Dong W.Apredictive runtime verification framework for cyber-physical systems[A].IEEE Eighth International Conference on Software Security and Reliability-Companion[C].San Francisco,California,USA:IEEE,2014.223-227.
[7] Bak S,Huang Z,Abad F A T,et al.Safety andprogress for distributed cyber-physical systems with unreliable communication[J].ACM Transactions on Embedded Computing Systems,2015,14(4):1-22.
[8] Mao J,Chen L.Runtimemonitoring for cyber-physical systems:a case study of cooperative adaptive cruise control[A].Second International Conference on Intelligent System Design and Engineering Application[C].Sanya,Hainan,China:IEEE,2012.509-515.
[9] Sistla A P,?efran M,Feng Y,et al.Timely monitoring of partially observable stochastic systems[A].International Conference on Hybrid Systems:Computation and Control[C].Chicago,Illinois,USA:ACM,2014.61-70.
[10] Stoller SD,Bartocci E,Seyster J,et al.Runtime verification with state estimation[A].International Conference on Runtime Verification[C].Berlin Heidelberg:Springer-Verlag,2011.193-207.
[11] Han T,Katoen JP.Counter examples in probabilistic model checking[A].International Conference on Tools and Algorithms for the Construction and Analysis of Systems[C].Berlin Heidelberg:Springer-Verlag,2007.72-86.
[12] Rabiner L.A tutorial onhidden Markov models and selected applications in speech recognition[J].Proceedings of the IEEE,1989,77(2):257-286.
[13] Zhao C,Wu C,Chai J,et al.Decomposition-based multi-objective firefly algorithm for RFID network planning with uncertainty[J].Applied Soft Computing,2017,55(6):549-564.
[14] Amditis A,Bimpas M,Thomaidis G,et al.A situation-adaptive lane-keeping support system:overview of the SAFELANE approach[J].IEEE Transactions on Intelligent Transportation Systems,2010,11(3):617-629.
[15] Kalajdzic K,Bartocci E,Smolka SA,et al.Runtimeverification with particle filtering[A].International Conference on Runtime Verification[C].Berlin Heidelberg:Springer-Verlag,2013.149-166.

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

Runtime Verification of States Unobservable Cyber-Physical System

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	田晖, 严艳, 汤莉莉, 吴俊彦, 王慧东, 全韩彧. 基于分数基音延迟动态搜索的语音隐写算法[J]. 电子学报, 2023, 51(1): 67-75.
[2]	赵耿, 马英杰, 陈磊, 董有恒, 侯艳丽. 基于扰动时空混沌系统的动态S盒设计[J]. 电子学报, 2022, 50(8): 2037-2042.
[3]	胡文文, 周日贵. 基于d维单个量子态的半量子密钥分发方案[J]. 电子学报, 2022, 50(5): 1025-1032.
[4]	徐佳伟, 罗倩. 基于遗传非参数MDL-BW方法的HMM结构优化[J]. 电子学报, 2022, 50(11): 2765-2772.
[5]	郑秋华, 胡程楠, 崔婷婷, 申延召, 曾英佩, 吴铤. 一种基于概率分析的DHR模型安全性分析方法[J]. 电子学报, 2021, 49(8): 1586-1598.
[6]	支婷, 刘颖, 周华春, 张宏科. 智慧标识网络服务机理研究进展及安全性分析[J]. 电子学报, 2021, 49(8): 1653-1664.
[7]	欧庆于, 罗芳, 吴晓平, 杨鹏. 基于电压毛刺故障扰动的分组密码安全性度量方法研究[J]. 电子学报, 2021, 49(3): 417-423.
[8]	汪榆淋, 窦家维. k-min问题安全多方计算方案及应用[J]. 电子学报, 2021, 49(11): 2256-2260.
[9]	魏铎, 高海英. 一种支持算术张成程序的密文策略属性加密方案[J]. 电子学报, 2020, 48(10): 1993-2002.
[10]	雷涛, 张肖, 加小红, 刘侍刚, 张艳宁. 基于模糊聚类的图像分割研究进展[J]. 电子学报, 2019, 47(8): 1776-1791.
[11]	宋云. 基于GHZ态局域测量的量子秘密共享[J]. 电子学报, 2019, 47(7): 1443-1448.
[12]	孙朋朋, 董云卫. 二维全向无线充电信息物理融合系统建模与优化方法[J]. 电子学报, 2019, 47(3): 568-575.
[13]	杨曦, 罗平, 贾古丽. 基于社会学信任理论的软件可信性概念模型[J]. 电子学报, 2019, 47(11): 2344-2353.
[14]	李雅, 黄少滨, 李艳梅, 迟荣华, 郎大鹏. 一种基于最弱前置条件的软件错误定位算法[J]. 电子学报, 2019, 47(1): 25-32.
[15]	李俊志, 关杰. 非线性反馈移存器型序列密码的完全性通用算法[J]. 电子学报, 2018, 46(9): 2075-2080.