• 中国期刊全文数据库
  • 中国学术期刊综合评价数据库
  • 中国科技论文与引文数据库
  • 中国核心期刊(遴选)数据库
戴敏, 潘海玉. 基于Kripke的状态保留模型修复算法[J]. 桂林电子科技大学学报, xxxx, x(x): 1-7.
引用本文: 戴敏, 潘海玉. 基于Kripke的状态保留模型修复算法[J]. 桂林电子科技大学学报, xxxx, x(x): 1-7.
DAI Min, PAN Haiyu. The state-preserving model repair algorithm of Kripke structures[J]. Journal of Guilin University of Electronic Technology, xxxx, x(x): 1-7.
Citation: DAI Min, PAN Haiyu. The state-preserving model repair algorithm of Kripke structures[J]. Journal of Guilin University of Electronic Technology, xxxx, x(x): 1-7.

基于Kripke的状态保留模型修复算法

The state-preserving model repair algorithm of Kripke structures

  • 摘要: 针对模型验证中受到广泛关注的模型修复问题,在极小模型修复的基础上保留原模型中尽可能多的可达状态,并给出了具有多项式时间复杂度的修复算法。模型经过检验后,若被判定存在违反给定性质的行为,则可以借助经典模型检验的不动点思想,找出模型中的验证失败路径,从而进行修复。此外,由于全局模型修复已被证明是NP问题,将修复算法的范围约束在CTL的一个子集内进行讨论。根据极小修复思想,选取对原模型中状态影响最小的修复操作,同时在经典模型检测的基础上,结合不动点思想以及图算法的部分性质构造出相应逻辑公式的修复算法,使状态保留的修复算法时间复杂度得以降低到多项式时间。

     

    Abstract: In order to solve the problem of model repair which has been widely concerned in model checking, this paper proposes to preserve as many reachable states as possible in the original model on the basis of minimal model repair, and gives a repair algorithm with polynomial time complexity.If the model is checked to violate the given property,we can find out the failure paths in the model by the fixed point idea of classical model checking and then repair them.In addition, since global model repair is proven to be NP-hard, the scope constraint of the repair algorithm is discussed in a subset of CTL.According to the idea of minimal model repair,we consider two kinds of repair operations which have the least influence on the states in the original model . At the same time, based on the classical model checking, the fixed point idea and some properties of the graph algorithm are combined to construct the State-Preserving model repair algorithm of the corresponding logical formulas,the time complexity of state-preserving model repair algorithm is reduced to polynomial time.

     

/

返回文章
返回