模型檢測中的偏序約簡

摘要:檢查并發系統的性質變得日益困難。隨著驗證方法的發展，一些復雜系統并發性越來越高，越來越難以理解。偏序約簡方法被提出以減少自動驗證并發系統所需要的時間和內存。文中介紹了偏序約簡技術的主要概念和基本算法，介紹了其在LTL中的應用，提出了改進方法。

關鍵詞:并發系統;模型檢測;偏序簡化;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)=?覫當且僅當 enabled(s)=?覫。

2) C1: 從s開始的每條路徑，依賴于ample(s)中某些變遷的變遷，不能在ample(s)中的變遷執行之前執行。

3) C2: 如s沒有全部擴展，對任意一個α∈ample(s)，α不可見。

4) C3: 狀態圖中不允許這樣一個循環存在，循環中變遷α可以發生，但α不屬于循環中任何狀態s的ample(s)。

2.2 偏序約簡算法

偏序約簡算法如圖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.