摘要: 分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。
[1] BAIER C,KATOEN J P.Principles of model checking[M].Cam-bridge:The MIT Press,2008. [2] LI Y M,DROSTE M,LEI L H.Model checking of linear-time properties in multi-valued system[J].Information Sciences,2017,7:51-74. [3] KHOUSSAINOV B,NERODE A.Automata Theory and its Ap-plications[M].Birkauser,2001. [4] LI Y M,LI L J.Model checking of linear- time properties based on possibility measure [J].IEEE Transaction on Fuzzy Systems,2013,1(5):842-854. [5] LI L,LI J.Model-checking of linear-time properties in possibilistic Kripkestructure [C]∥Quanitative Logic and Soft Computing-the QI&SC.2012:287-294. [6] LI Y M.Two methods for Model-checking ofLTL[J].Journal of Shaanxi Normal University(Natural Science Edition),2014,42(4):22-25.(in Chinese) 李永明.可能LTL模型检测的两种方法[J].陕西师范大学学报(自然科学版),2014,2(4):22-25. [7] LI L J.Model checking of linear-time properti-es based on possibility measure [D].Xi’an:Shaanxi Normal University,2012.(in Chinese) 李丽君.基于可能性测度的LTL 模型检测[D].西安:陕西师范大学,2012. [8] EDMUND E,GRUMBERG O,PELED D.Model checking [M].Cambridge:The MIT Press,1999. [9] EVANGELISTA Y M,PRADAT-PEYRE J F.Memory Efficient State Space Storage in Explicit Software[C]∥InternationalSpin Workshop on Model Checking of Software.2005:43-57. [10] BARNAT J,BRIM L,ROCKAI P.Scalable multicore LTL modelchecking[M]∥ Model Checking Sofware.Springer Berlin Heidelberg,2007:187-203. [11] HOU G,ZHOU K J,YONG J W,et al.Research overview of state explosion in the model checking[J].Computer Science,2013,0(6A):77-86.(in Chinese) 候刚,周宽久,勇嘉伟,等.模型检测中状态爆炸问题研究综述[J].计算机科学,2013,0(6A):77-86. [12] JIANG Y X,LIN C,XING X J.Model checking of Petri netbased on linear logic[J].Journal of System Simulation,2003,15(21):6-10.(in Chinese) 蒋屹新,林闯,刑栩嘉.基于线性逻辑的Petri 网的模型检测[J].系统仿真学报,2003,5(21):6-10. [13] BOURAHLA M.Distributed CTL model checking[J].IEEEProceedings Software,2005,2(6):297. [14] LERDA F,SISTO R.Distributed-memory model checking with spin[C]∥International Spin Workshops on Theoretical & Practical Aspects of Spin Model Checking.Spinger-Verlag,1999:22-39. [15] BARNAT J,BRIM L,STˇBRN J.Distributed LTL model-checking in SPIN[C]∥Proceedings of the 8th International SPIN Workshop on Model Checkingof Software.2001:200-216. |
No related articles found! |
|