期刊文献+

可能性测度下的LTL模型检测并行化研究 被引量:3

Parallelization of LTL Model Checking Based on Possibility Measure
下载PDF
导出
摘要 分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。 Distributed model checking(DMC)is an effective solution for the state-explosion problem in model checking.The qualitative LTL distributed model verification algorithm has been proposed.However,the problem of parallelization quantitative LTL verification has not been solved effectively.In this paper,a new dynamic state partition method was presented and a quantitative DMC was proposed based on the qualitative LTL distributed verification algorithm.Firstly,the system model is transformed into a possible Kripke structure to choose a concurrent component,and its state space is divided by the relationships of states,which aims to allocate the related states to the same computing node.Secondly,the partition results are adjusted for the load balance of DMC system.Then,the partition results and the states of the rest components are done cross product to complete the state partition of the system.Finally,the properties are represented by nondeterministic finite automaton,and their cross products can complete the quantitative verfication of system based on the extended nested DFS distributed verification algorithm.
作者 雷丽晖 王静 LEI Li-hui;WANG Jing(School of Computer Science,Shaanxi Normal University,Xi’an 710062,China)
出处 《计算机科学》 CSCD 北大核心 2018年第4期71-75,88,共6页 Computer Science
基金 国家自然科学基金(11271237 11301321) 中央高校基本科研业务费专项资金(GK201603086)资助
关键词 可能的Kripke结构 状态空间划分 定量分布式模型检测 Possibilistic Kripke structure State partition of system Quantitative distributed model checking
  • 相关文献

参考文献3

二级参考文献172

  • 1孙伟,马绍汉.分布式博弈树搜索算法[J].计算机学报,1995,18(1):39-45. 被引量:1
  • 2袁志斌,徐正权,王能超.软件模型检测中的抽象[J].计算机科学,2006,33(7):276-279. 被引量:5
  • 3文艳军,王戟,齐治昌.并发反应式系统的组合模型检验与组合精化检验[J].软件学报,2007,18(6):1270-1281. 被引量:17
  • 4[1]A. Pnueli. The Temporal Semantics of Concurent Programs [J].Theoretical Computer Science, 1981, 13: 45-60.
  • 5[2]E.M. Clarke, et al. Automatic Verification of Finite State Concurrent System Using Temporal Logical Specification [J]. ACM transaction on Programming Language and Systems, 1986, 8(2): 244-263.
  • 6[3]Leslie Lamport. The Temporal Logic of Actions [J]. ACM transaction on Programming Language and Systems, 1994, 16(3): 872-923.
  • 7[4]E.M. Clarke, O. Grumberg, D. Peled. Model Checking. Cambridge[M], MA: MIT Press, 2001, 35-49.
  • 8[5]R. Gerth, D. Peled, M.Vardi, and P. Wolper. Simple On-the-fly Automatic Verification of Linear Temporal Logic [C]. In Proceedings of the 15th International Conference on Protocol Specification,Testing and Verification, Warsaw, Poland, 1993.
  • 9[6]Z. Manna, A. Pnueli. The Temporal Logic of Reactive and Concurrent System: Specification [M]. Spring-Verlag, 1992.
  • 10[7]A. Prasad Sistla, M. Y. Vardi and P. Wolper. The Complementation Problem for Btchi Automata with Applications to Temporal Logic [J].Theoretical Computer Science, 1987, 49: 217-237.

共引文献48

同被引文献16

引证文献3

二级引证文献2

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部