积分商城

最新搜索： ZIMO it67 野火K60中文资料整理版 si9000 filter 膨胀阀开度
您现在的位置是：首页 > 技术资料 > 状态不可观测的信息物理融合系统运行时验证
推荐星级：
  • 1
  • 2
  • 3
  • 4
  • 5

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

更新时间：2019-12-24 00:38:57 大小：783K 上传用户：守着阳光1985查看TA发布的资源 标签：信息物理融合系统 下载积分：1分 评价赚积分 （如何评价?） 打赏 收藏 评论(0) 举报

资料介绍

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


部分文件列表

文件名 大小
状态不可观测的信息物理融合系统运行时验证.pdf 783K

【关注视频号领20积分】   【关注公众号立即送20积分】

部分页面预览

（完整内容请下载后查看）
12  
Vol． 46 No． 12  
Dec． 2018  
第
期
电
子
学
报
2018  
12  
ACTA ELECTRONICA SINICA  
年
月
状态不可观测的信息物理融合系统运行时验证  
1，2  
1
1
1
， ， ，  
房丙午 黄志球 王 勇 李 勇  
( 1.  
，
南京航空航天大学计算机科学与技术学院 江苏南京  
210016; 2.  
，
安徽财贸职业学院云桂信息学院 安徽合肥  
230061)  
:
( Cyber-Physical System，CPS) ，  
运行时行为正确性是至关重要的 尤其在航空航  
摘
要
确保信息物理融合系统  
、 、 ．  
天 汽车 核电和医疗等安全攸关领域 本文针对具有随机行为且状态不可观测的  
CPS，  
提出一种基于隐马尔科夫模型  
．
的运行时安全性验证方法 首先构造状态不可观测的  
CPS  
，
运行时安全性验证框架 该框架通过隐马尔科夫模型表示  
， ， ，  
系统 使用确定性有限自动机规约系统安全属性的否定 两者的乘积自动机作为运行时监控器 从而将  
CPS  
运行时安  
． ， ．  
全性验证问题约简到监控器上的概率推断问题 然后 提出一种增量迭代安全性验证算法以及反例生成算法 实验结  
20% ， ，  
并且当系统违背安全属性时 本文的方法能给出  
果表明本文算法和粒子滤波算法相比预测错误率下降了近  
．
反例  
:
;
;
;
;
;
关键词  
中图分类号  
URL: http: / /www． ejournal． org． cn  
信息物理融合系统 运行时验证 隐马尔科夫模型 确定性有限自动机 安全性 反例  
TP311 0372-2112 ( 2018) 12-2824-08  
DOI: 10． 3969 /j． issn． 0372-2112． 2018． 12． 002  
:
:
A
:
文章编号  
文献标识码  
电子学报  
Runtime Verification of States Unobservable Cyber-Physical System  
1，2  
1
1
1
FANG Bing-wu ，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)  
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 algo-  
rithm 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; safe-  
ty; counter-example  
CPS  
．
运行时行为正确性的有效方法 文献  
［3 ～  
是保证  
1
引言  
5］  
针对实时性要求较高的  
CPS，  
验证与时间相关的功能  
CPS  
、 、  
在航空航天 汽车 核电和医疗等安全攸关的  
． ［6］  
正确性 文献 针对  
CPS  
．
运行时失效行为进行监控  
［1，2］  
， ，  
因此 确保  
CPS  
运行时  
领域有着广阔的应用前景  
CPS  
， ［7］  
运行时安全性验证方面 文献 给出在不可靠  
在
．
行为正确性是至关重要的 运行时验证通过监控系统  
，
的网络通信下 对  
CPS  
的安全属性不变式进行运行时  
［3］  
，
运行时的执行轨迹来验证系统是否满足属性规约  
，
验证 不变式是一类基于状态的使用谓词逻辑描述的  
: 2018-05-03;  
: 2018-07-15;  
:
收稿日期  
修回日期  
责任编辑 覃怀银  
国家自然科学基金资助项目  
( No． gxbjZD32)  
:
基金项目 国家重点研发计划  
( No． 2016YFB1000802) ;  
( No． 61772270) ;  
( No．  
安徽省高校自然科学基金重点项目  
KJ2017A859) ;  
(
)
安徽省高校学科 专业 优秀拔尖人才学术资助计划  
2825  
12  
:
房丙午 状态不可观测的信息物理融合系统运行时验证  
第
期
，
安全属性 该方法不能验证无限状态时序序列的安全  
3
相关定义与监控器模型  
． ［8］  
属性 文献 使用混成自动机建模自适应巡航控制系  
3. 1  
相关定义  
，
CHARON  
，
语言规约安全属性 验证了自适应巡  
统 使用  
航控制系统运行时安全性 虽然研究人员提出了多种  
CPS  
HMM  
， DFA  
建模系统 采用 描述系统安全  
本文采用  
．
，
．
属性 下面给出相关的定义  
DFA A = ( Q，  
是如下形式的五元组  
，
:
运行时验证的方法 但目前的研究存在以下不足  
1
定义  
一个  
( 1)  
现有的研究都假设系统运行时的状态可以直接观  
CPS  
，，q ，F) ．  
Σ δ  
0
，
其中  
，
测的 实际上大多数复杂的  
在运行时其状态是不  
［9，10］  
( 1) Q  
，
是有限的 非空的状态集合  
，
． ( 2)  
，
在运行时安全性验证中 当系统违背  
可观测的  
AP  
［11］  
( 2)  
， = 2 ，AP  
Σ 是输入字母表 Σ  
，
为原子命题集合  
，
安全属性时 而没有给出相应的反例  
．
( 3) : Q ×  
δ
Q
，
是一个状态转换函数  
Σ
→
，
针对上述不足 本文提出了状态不可观测的具有  
( 4) q  
Q
，
是一个初始状态  
∈
CPS  
．
运行时安全性验证方法 由于系统状  
0
随机行为的  
( 5) F  
Q
．
是接受状态的集合  
， ，  
态不可观测 因此 采用隐马尔科夫模型  
( Hidden Mark-  
AP  
A q Q， B 2 | ( q，B) | = 1，  
如果在 中 ∈  ∈ 都有 δ  
ov Model，HMM)  
．
来建模系统 使用确定性有限自动机  
A
DFA．  
DFA  
对于每个  
那么 是一个完全的  
一个完全的  
都存在一个唯一的运行与之对应  
( Discrete-Time  
一个离散时间马尔科夫链  
( Deterministic Finite Automaton，DFA)  
规约安全属性的  
DFA  
AP  
ω
( 2  
)
．
输入字 σ∈  
，
否定 安全属性监控器由  
HMM  
和
的乘积自动机表  
CPS  
运行时安全性验证问  
2
定义  
，
示 从而将状态不可观测的  
Markov Chain，DTMC)  
C = ( S，P， ，L) ．  
ι
init  
是一个四元组  
．
题约简到监控器上的概率推断问题  
:
其中  
2
运行时验证框架  
( 1) S  
，
表示可数非空的状态集合  
( 2) P: S × S ［0，1］ ，  
是状态转换概率分布函数 对  
→
:
本文的验证问题可描述为 给定系统状态转换模  
TS，  
系统安全属性 φ 以及系统运行时的观测序列  
safe  
型
s
每一个状态 ∈  
S，  
P( s，s') = 1，  
∑
s'  
S
∈
o ，…，o ，  
目标是  
t
( 1)  
t
计算在 时刻系统满足安全属性  
| o ，…，o ; TS) ，( 2)  
当系统违背安  
1
( 3)  
: S ［0，1］ ，  
是 初 始 状 态 概 率 分 布 函 数  
→
ι
init  
Pr ( TS  
t
的概率  
φ  
safe  
1
t
( s) = 1，  
ι
∑
init  
，
全属性时 求解系统最大可能的执行路径  
argmaxPr( s ，  
1
s1，s2，…，st  
s
S
∈
AP  
( 4) L: S  
2
→
．
是标签函数  
s ，…，s | o ，o ，…，o ; TS)  
2
作为系统违背安全属性的反  
2
t
1
t
3
HMM  
H = ( C，O， ) ．  
是一个三元组 μ  
定义  
一个  
． ， 1 ．  
例 针对该问题 图 给出了本文验证方法的框架  
:
其中  
( 1) C  
DTMC，  
是一个  
( 2) O  
，
是系统可观测符号的有限集合 即系统模型  
，
输出的有限集合  
O
( 3) : S × 2  
μ
［0，1］  
是一个观测符号概率分布函  
→
， s  
数 对于 ∈  
S，  
( s，o) = 1.  
μ
∑
O
o 2  
∈
( s，o)  
( o)  
s o  
表示系统在状态 时产生观测 的  
μ
或 μ  
s
， ，  
概率 相同的观测可能由几个不同的系统状态产生 因  
，
此 在已知目前观测的情况下系统的状态是不确定的  
．
1
， ，  
中 虚线框中是运行时验证的监控器单元 监  
图
3. 2  
监控器模型  
本文将安全属性监控器定义为一个  
， ，  
控器由系统模型和属性自动机的乘积来表示 其中 系  
A
H
的乘积  
和
HMM ， DFA  
表示 属性自动机由  
．
表示 监控器  
统模型由  
， ，  
自动机 系统安全属性是基于可观测符号描述 因此  
，A  
O
的输入是运行时系统的观测序列和系统安全性的阈值  
2 ．  
的输入字母表 Σ  
P ，  
th  
，
监控器输出是当前系统满足安全性的概率 当系统  
4
A
H
和 的乘  
定义  
积自动机  
安全属性监控器定义为一个  
M = A H = ( S'，P'，' ，F'，O，') ． ，  
其中  
， ．  
安全性概率低于阈值时 输出反例 系统模型的构造可  
ι
μ
init  
［9］  
，
以来自于系统设计模型  
或通过领域专家指定系统  
( 1) S' = S × Q，  
监控器状态集合  
;
，
状态以及状态的观测值 然后模拟系统运行获取系统  
( 2) P'( 〈s，q〉，〈s'，q'〉) =  
［10］  
．
观测数据并学习一个系统模型  
系统的安全属性采  
P( s，s') ( t) ，if T  
μ
∑
≠   
s
，
用线性时序逻辑描述 使用  
DFA  
来识别安全属性的否  
t
T
∈
，
表示状态转换概率分布  
{
．
0，otherwise  
定也就是识别系统运行中违反安全性的有限前缀  

相关下载

全部评论(0)

暂无评论
评论赚积分>>

上传资源 上传优质资源有赏金

热门标签

更多>>

最新上传

  • 打赏
  • 30日榜单

热门下载

推荐下载

本站上的所有资源均为源于网上收集或者由用户自行上传，仅供学习和研究使用，无任何商业目的，版权归原作如有侵权，请 来信指出，本站将立即改正。

ICP许可证号：京ICP证070360号     21IC电子网 2000- 版权所有

京ICP备11013301号

京公网安备 11010802024343号