模型检测中的偏序约简
开篇：润墨网以专业的文秘视角，为您筛选了一篇模型检测中的偏序约简范文，如需获取更多写作素材，在线客服老师一对一协助。欢迎您的阅读与分享！
摘要:检查并发系统的性质变得日益困难。随着验证方法的发展,一些复杂系统并发性越来越高,越来越难以理解。偏序约简方法被提出以减少自动验证并发系统所需要的时间和内存。文中介绍了偏序约简技术的主要概念和基本算法,介绍了其在LTL中的应用,提出了改进方法。
中图分类号:TP311文献标识码:A文章编号:1009-3044(2009)26-7545-02
Partial Order Reduction in Model Checking
ZHU Xin-feng, LI Bin, WU Jun
(College of Computer Science and Engineering, Yangzhou University, Yangzhou 225009, China)
Abstract: Checking the properties of concurrent systems is an ever growing challenge. Along with the development of improved verification methods, some critical systems that require careful attention have become highly concurrent and intricate. Partial order reduction methods were proposed for reducing the time and memory required to automatically verify concurrent asynchronous systems. Some main concepts and algorithms are introduced in this paper, and improving methods are proposed in the paper.
Key words: concurrent systems; model checking; partial order reduction; LTL; algorithm
模型检测是一种形式化的软硬件验证技术。软件不同状态的个数,代表了不同状态变量的赋值,随着并发系统组件数量的增长急速增长,即称为所谓的状态爆炸问题,有图1所示。偏序简化技术是其中一种重要技术,本文对偏序简化技术作了一些介绍。
状态变迁系统是一个四元组(S,S0,T,L) 其中S为有限状态集合,S0为初始状态集合, T表示变迁关系,对任意一个α∈T, α?哿S×S,α(s,s') 表示s,s'之间存在变迁α,也可以表示为s'=α(s)。L:S->2AP 是一个赋值函数,用来表示状态对于原子命题的赋值。状态s能够发生的变迁的集合称为Enabled(s),从状态s开始的路径被定义为 π=s0α0 s1α1…,其中s=s0,对于任意一个i,αi(si,si+1)成立。
偏序简化的基本思想是找到enabled(s)的子集ample(s)来生成状态s的后继 ample(s)?哿enabled(s),通过选择可变迁子集,属性的正确性检查在简化了的状态空间和全状态空间中得以保持。图2所示即为由图1通过偏序约简得到的简化图。
1 几个定义
1.1 不依赖性:
独立性I定义为 I?哿T×T,?坌(α,β)∈I ,s∈S, α,β∈enabled(s)有如两个条件成立:
1) α∈enabled(β(s))且β∈enabled(α(s))相互之间不能使对方失效;
2) α(β(s))= β(α(s)),说明α, β之间的先后执行次序无关。
如果(α,β)∈I,ample(s)中就没有必要包含α, β两者,可只包含其中之一。
1.2 不可见性
一个变迁α∈T是不可见的当 对s, s'∈S, s'=α(s), L(s)=L(s'),也就是说一个变迁在执行过程中没有改变原子命题的值就可以称该变迁是不可见的。对于两个独立变迁α, β而言,有下列等式成立
1) 如α不可见,L(s)=L(α(s)),L(β(s))=L(α(β(s)))
2) 如β不可见,L(s)=L(β(s)),L(α(s))=L(β(α(s)))
3) 如α, β不可见,L(s)=L(α(s))=L(β(s))=L(α(β(s)))
1.3 stuttering相等
stuttering相等性是与不可见性相类似的概念,是对执行路径而言的,|(ρ)表示连续相同的标记被用一个标记来表示,如 if AP = {p,q}, σ = (p)(p,q)(p,q)(q)(q)(p,q),ρ=(p)(p)(p,q)(p, q)(p,q)(q)(p,q),则|(σ)=(p)(p,q)(q)(p,q)=|(ρ),由于|(σ)=|(ρ),可以称σ与ρ stuttering相等。
2 偏序简化的应用及算法
2.1 对LTL进行简化
为了选择ample(s)?哿enabled(s),首先需要定义四个条件。
1) C0: ample(s)=?I当且仅当 enabled(s)=?I。
2) C1: 从s开始的每条路径,依赖于ample(s)中某些变迁的变迁,不能在ample(s)中的变迁执行之前执行。
3) C2: 如s没有全部扩展,对任意一个α∈ample(s),α不可见。
4) C3: 状态图中不允许这样一个循环存在,循环中变迁α可以发生,但α不属于循环中任何状态s的ample(s)。
偏序约简算法如图3所示,其中conditionally safe定义为:在条件p(t)下,变迁t和t'能够相互交换 p(t)?哿S。
2.3 偏序约简算法的改进
图3提供的算法可以减少模型检测中的状态数,但是由于加了限制条件,很多时候效率并不高,为了提高效率,可以考虑两阶段方法,第一阶段执行确定性的进程产生状态s,第二阶段,检查所有在状态s能够发生的变迁。也可以考虑并行DFS算法,该算法可看作为一种BFS算法,最终能用BDD符号技术来实现。
3 结束语
本文介绍了模型检测中偏序技术以及其中的一些基本概念和算法,提出了一些改进的方法,该研究领域还有待在以后的工作进一步的进行深入的研究。
参考文献:
[1] Clarke E, Grumberg O, Peled D A.Model Checking[M].Cambridge, MA, USA: MIT Press,2000.
[2] Godefroid P. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Lecture Notes in Computer Science[M].Berlin: Springer-Verlag,1996:1032.
[3] Peled D. Ten years of partial order reduction[C].Proceedings of the 10th International Conference on Computer Aided Verification, Springer-Verlag ,1998:17-28.
[4] Palmer R, Gopalakrishnan G. A distributed partial order reduction algorithm[J].Formal techniques for networked and distributed systems FORTE 2002, 2002(2529):370.
[5] Nalumasu R. Gopalakrishnan G. An efficient partial-order reduction algorithm with an alternative proviso implementation[J].Formal Methods In System Design,2002,20(3):231-247.