Runtime Verification of States Unobservable Cyber-Physical System

FANG Bing-wu; HUANG Zhi-qiu; WANG Yong; LI Yong

doi:10.3969/j.issn.0372-2112.2018.12.002

您当前的位置：

首页 >

文章列表页 >

Runtime Verification of States Unobservable Cyber-Physical System

更新时间：2025-07-16

- Runtime Verification of States Unobservable Cyber-Physical System
- Acta Electronica Sinica Vol. 46, Issue 12, Pages: 2824-2831(2018)
- 作者机构：
  
  1. 南京航空航天大学计算机科学与技术学院,江苏,南京,210016
  2. 安徽财贸职业学院云桂信息学院,安徽,合肥,230061
  3. 南京航空航天大学计算机科学与技术学院,江苏,南京,210016
  4. 安徽财贸职业学院云桂信息学院,安徽,合肥,230061
- 作者简介：
- 基金信息：
- DOI：10.3969/j.issn.0372-2112.2018.12.002
  CLC： TP311
- Published Online：25 December 2018，
  
  Published：2018
- 稿件说明：
移动端阅览
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.
DOI：

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. DOI： 10.3969/j.issn.0372-2112.2018.12.002.

摘要

确保信息物理融合系统（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.

关键词

Keywords

references

Views

317

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Time Series Prediction Algorithm Based on GOSSA and HMM

Voice Conversion Technology and Its Development

N-order Neighbor Road Network Based Vehicle Travel Time Estimation Model

A Regular Expression Matching Algorithm Based on Multi-Dimensional Cube

Related Author

LI Da-she

SUN Yuan-wei

RUAN Jun-hu

RUAN Xiao-gang

LIU Wen-ju

ZUO Guo-yu

WU Wen-li

OUYANG Chu-fei

Related Institution

School of Economics and Management， Northwest Agriculture & Forestry University

School of Computer Science and Technology， Shandong Technology and Business University

School of Electronics Information and Control EngineeringBeijing University of TechnologyBeijing 100022China

National Laboratory of Pattern RecognitionInstitute of AutomationChinese Academy of SciencesBeijing 100080China

School of Electronics Information and Control Engineering,Beijing University of Technology

⁰