雷丽晖,王静.可能性测度下的LTL模型检测并行化研究[J].计算机科学,2018,45(4):71-75, 88
可能性测度下的LTL模型检测并行化研究
Parallelization of LTL Model Checking Based on Possibility Measure
投稿时间:2017-05-19  修订日期:2017-07-21
DOI:10.11896/j.issn.1002-137X.2018.04.010
中文关键词:  可能的Kripke结构,状态空间划分,定量分布式模型检测
英文关键词:Possibilistic Kripke structure,State partition of system,Quantitative distributed model checking
基金项目:本文受国家自然科学基金(11271237,11301321),中央高校基本科研业务费专项资金(GK201603086)资助
作者单位E-mail
雷丽晖 陕西师范大学计算机科学学院 西安710062 leilihui@snnu.edu.cn 
王静 陕西师范大学计算机科学学院 西安710062  
摘要点击次数: 267
全文下载次数: 180
中文摘要:
      分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量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.
查看全文  查看/发表评论  下载PDF阅读器