基于隐马尔科夫模型的随机系统运行时安全性验证
Runtime Safety Verification of Stochastic System with Hidden Markov Model
作者：房丙午(南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106;安徽财贸职业学院 云桂信息学院, 安徽 合肥 230601)；黄志球(南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106)；李勇(南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106)；王勇(南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106)
Author：FANG Bingwu(College of Computer Sci., Nanjing Univ. of Aeronautics and Astronautics, Nanjing 211106, China;School of Yungui Info., Anhui Finance and Trade Vocational College, Hefei 230601, China)；HUANG Zhiqiu(College of Computer Sci., Nanjing Univ. of Aeronautics and Astronautics, Nanjing 211106, China)；LI Yong(College of Computer Sci., Nanjing Univ. of Aeronautics and Astronautics, Nanjing 211106, China)；WANG Yong(College of Computer Sci., Nanjing Univ. of Aeronautics and Astronautics, Nanjing 211106, China)
收稿日期：2018-05-29 年卷（期）页码：2018,50(6):198-204
期刊名称：工程科学与技术
Journal Name：Advanced Engineering Sciences
关键字：随机系统;安全性;运行时验证;隐马尔科夫模型
Key words：stochastic system;safety;runtime verification;hidden Markov mode
基金项目：国家重点研发计划资助项目（2016YFB1000802）；国家自然科学基金资助项目（61772270）；安徽省高校自然科学基金重点资助项目（KJ2017A859）；安徽省高校学科（专业）优秀拔尖人才学术资助项目（gxbjZD32）
中文摘要
随机系统运行时验证中，由于可靠地传感系统运行状态的成本非常高以及一些事件的监控严重影响系统时间相关的行为，因此，复杂随机系统在运行时其状态是难以观测的。为了对该类系统进行运行时验证，提出了状态不可观测的随机系统运行时安全性验证方法。首先，给出了随机系统安全性验证框架，框架使用隐马尔科夫模型建模运行时系统，使用确定性有限自动机规约系统安全属性，使用两者的乘积自动机作为属性验证器。然后，提出了属性验证器的构造算法，该算法消除了从初始状态不可达的状态以及与验证属性无关的组合状态，约简了验证器的规模。最后，基于验证器，提出增量迭代安全性验证算法，该算法接收到一个新的观测值，立即计算已观测到的整个有穷序列的监控结论，不需要保存当前观测值之前的有穷观测序列。实验仿真结果表明该方法能有效性地在线验证状态不可观测的随机系统安全性。
英文摘要
The state of a complex stochastic system for verification is difficult to be observed at runtime, since the cost of reliably sensing the operating state of the system is very high and the monitoring of some events can seriously affect time-related behaviors of the system. In order to perform runtime verification on such a system, a method for verifying runtime safety of a stochastic system with unobservable state was proposed. First, a runtime safety verification framework of stochastic system was constructed, in which the system model was represented by the hidden Markov model (HMM), and the negation of safety property was specified by deterministic finite automaton (DFA). Then, the product automata of DFA and HMM was used as a property verifier. Second, a construction algorithm of the verifier was proposed, which reduces the size of the verifier by eliminating the unreachable state starting from the initial state and the combined state independent of the verification property. Finally, an incremental iterative safety verification algorithm based on the verifier was proposed. Once a new observation value was received, the monitoring conclusions of the observed whole finite sequence without saving the sequence were immediately calculated. Experimental simulation results showed that the proposed method can effectively online verify the safety of stochastic systems with unobservable states.
【关闭】
