基于隐马尔科夫模型的随机系统运行时安全性验证

中文摘要: 随机系统运行时验证中，由于可靠地传感系统运行状态的成本非常高以及一些事件的监控严重影响系统时间相关的行为，因此，复杂随机系统在运行时其状态是难以观测的。为了对该类系统进行运行时验证，提出了状态不可观测的随机系统运行时安全性验证方法。首先，给出了随机系统安全性验证框架，框架使用隐马尔科夫模型建模运行时系统，使用确定性有限自动机规约系统安全属性，使用两者的乘积自动机作为属性验证器。然后，提出了属性验证器的构造算法，该算法消除了从初始状态不可达的状态以及与验证属性关的组合状态，约简了验证器的规模。最后，基于验证器，提出增量迭代安全性验证算法，该算法接收到一个新的观测值，立即计算已观测到的整个有穷序列的监控结论，不需要保存当前观测值之前的有穷观测序列。实验仿真结果表明该方法能有效性地在线验证状态不可观测的随机系统安全性。
Abstract: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.