帶有啟發式因子的死鎖模型檢測算法

王 焱，吳 濤，楊 斐

(1.成都信息工程大學 計算機學院， 成都 610225；2.中國核動力研究設計院 核反應堆系統設計技術重點實驗室， 成都 610041)

0 引言

系統和軟件設計的可靠性非常重要，因此如何構建可靠的軟件和系統的相關技術就極為關鍵。特別是在一些關鍵領域，如航天航空領域、核領域等等，系統一旦出現故障，其帶來的損失往往是不可接受的。由于傳統的測試仿真只能尋找系統的錯誤，而不能證明系統不存在錯誤，形式化驗證就能夠解決這個問題。

模型檢測是一種自動驗證有限狀態并發系統的形式化驗證技術[1]，它能夠通過對所給模型的所有可能狀態進行分析，驗證其是否滿足所給定的規范。如果不滿足，則生成相應的反例。系統規范一般是通過線性時序邏輯(LTL)或者分支時序邏輯(CTL)刻畫的[2]。

在顯式模型檢測中，系統的設計模型通常用有向圖表示。它表示了并發系統的所有可能的行為，同時還包含了各個狀態之間的變遷關系。一般的，模型檢測器采用確定性算法和窮盡搜索狀態空間來驗證是否滿足某些性質。當狀態空間過大時，就會導致檢測效率較低，甚至不能完成檢測目標。在核領域的DCS系統中，由于系統較為復雜，這種問題尤為明顯。

為了提高模型檢測的效率，業界提出了幾種通過減少狀態空間大小的方法來緩解這個問題，比如符號模型檢測、抽象方法、偏序規約等等[3-5]。同時，除了上述的方法，提高在狀態空間中搜索算法的效率也是可行的。為了提高確定性算法在狀態空間過大的情況下的表現，研究人員進行了相關研究。文獻[6]提出了一種基于磁盤的寬度優先搜索算法(BFS)。該方法針對BFS出現的某些層所擁有的狀態無法全部存儲到內存中而影響模型檢測的問題，將每一層的狀態進行分區劃分，從而提高算法效率。

同時，并行化技術也能夠提高確定性算法的表現。文獻[7]采用了并行化和分布式的BFS，從而能夠發現長度更短的反例。文獻[8]采用并行化的BFS，完成了對模型安全性質的檢測。

除了以上的確定性算法研究之外，基于啟發式算法的模型檢測算法也得到了研究人員的關注。通過啟發式因子讓搜索方向向目標狀態靠攏，從而加快搜索。文獻[9]提出了一種基于A*算法的模型檢測算法。文獻[10]也提出了基于粒子群算法的模型檢測算法，利用粒子群高效完成了對違反安全性的路徑的搜索。同時，粒子群算法在概率模型檢測中也有較好的表現。文獻[11]提出了一種混合粒子群算法和引力搜索的算法完成了死鎖性質的檢測。文獻[12]提出了一種基于蟻群算法的模型檢測算法，同時通過增加目標節點的信息素操作，加快了模型檢測的效率。文獻[13]提出一種新的蟻群算法ACOhg，通過對搜索深度的動態選擇，在狀態空間過大時有良好的表現。文獻[14]將蒙特卡洛樹算法應用到了模型檢測算法中，該方法能夠有效搜索狀態空間從而得到相應的反例。

在以上的文獻中，沒有考慮到路徑長度對所生成反例的影響。因此，探討了差分進化算法(DE)在針對狀態空間數量較大時檢測死鎖狀態的可行性。差分進化算法是一種基于遺傳和自然選擇的啟發式算法。這種啟發式算法結合了優勝劣汰和隨機性的信息，可以較好地兼顧檢測速度和檢測質量。同時針對模型檢測的具體背景，設計了新的路徑生成算法，用以解決狀態遷移圖中的編碼問題。同時在算法原有框架下，增添了模擬退火操作，與關鍵參數的自適應用以提高算法的表現。最后設計了用于評估路徑優劣的適應值函數。

主要內容組織如下：第1節描述了模型檢測的相關背景，同時回顧了一些已經提出了的提高檢測效率的方案；第2節詳細描述了所提出的研究內容；第3節描述的是相關實驗，同時分析了實驗結果；最后在結語部分，對工作做出了總結，同時分析了存在的不足，并在最后對未來的相關工作做出了展望。

1 死鎖檢測解決方案

在本節中，形式化了死鎖檢測問題，同時介紹了標準差分進化算法的過程以及詳細描述了基于差分進化算法框架提出的模型檢測算法。

1.1 問題形式化

死鎖是指2個或者2個以上的進程在執行過程中，由于競爭資源從而造成的一種阻塞的情況。若無外力的情況下，進程將永遠無法進行下去，永遠處于互相等待的情況，這就是死鎖。

在顯式模型檢測中，死鎖狀態對應的是系統狀態圖中只有入邊而沒有出邊的節點。因此死鎖檢測問題可以形式化為有向圖中從初始狀態開始到目標狀態結束的路徑搜索問題。將這個問題形式化如下：

設G=(S,T)為一個有向圖，其中S表示圖中的節點的集合，T表示有向圖的邊的集合。設q為圖的初始節點，F是圖中所有目標節點的集合。設有向圖中的一條有限路徑Π=S1,S2,S3,…,Sn，Si∈S，i=(1,2,3,…,n)。|Π|表示該條路徑的長度。T(S)表示當前節點的后繼節點。

現給定一個有向圖G，死鎖檢測問題可以形式化為找到一個從起始節點開始且結束于目標節點的路徑Π。Π需要滿足以下約束：

S1=q，Sn∈F

(1)

1.2 差分進化算法

差分進化算法[15]是一種基于群體的啟發式算法，最早由Storn和Price于1995年首次提出，其優化的核心是基于群體個體之間的相互合作和相互競爭從而引導搜索的方向，達到加快搜索的目的。其主要由差分、交叉變異、選擇策略3個部分組成。具體算法流程如圖1所示。

圖1 標準差分進化算法流程框圖

作為一種基于群體的進化算法，差分進化算法中每一個個體都代表了一個可能解，這些個體稱為染色體，通過特定的操作生成子代個體，再從子代個體中選擇出相對較優的個體組成下一代種群，從而推動算法的進行。差分進化算法的基本步驟如下：

步驟1設置算法初始參數，初始化種群。

步驟2對種群中的每一個個體進行差分操作，產生變異個體Vi。具體差分操作是隨機選擇種群中兩個不同的個體，將其向量縮放之后與待變異個體進行向量合成生成變異向量Vi。公式如下:

Vi=X1+F(X2-X1)

(2)

步驟3對于個體向量Xi和變異向量Vi進行交叉操作，生成實驗個體向量Ui。具體交叉操作是設定一個初始值CR，CR具體值參考后文。該值決定了哪些維度是應該采用變異向量的維度，哪些向量保持不變。公式如下：

(3)

步驟4根據選擇策略選擇出合適的下一代解，作為下一代種群。

步驟5判斷當前解是否滿足終止條件。若滿足則輸出最優結果；否則轉至步驟2。

因此，當把死鎖檢測問題看作一個優化問題時，就可以考慮將有向圖看作一個狀態空間，然后通過染色體的個體行為聯合整個種群的群體行為共同尋解，而尋到的解就是檢測到的反例。

1.3 應用于死鎖檢測的改進差分進化算法

基于原有的差分進化算法框架，提出了以下的在模型檢測背景下的改進差分進化算法。與原算法相比，提出了新的路徑生成算法：模擬退火算子用以提高算法表現，Cr自適應參數以及針對路徑的適應值函數。

1.3.1粒子編碼以及路徑生成

傳統的差分進化算法由于用于解決優化問題，采取的是隨機編碼的方式。但是這種方式在模型檢測的背景下是不合適的。因此編碼方式也是相當關鍵的。

傳統的編碼方式主要有2種：直接編碼和間接編碼。

直接編碼：直接按照節點的標識號順序進行編碼。這些標識號隨機分配給狀態圖中所有的節點。這種編碼方式中，由于節點序列是隨機的，可能會產生大量的無效路徑(即編碼順序和遷移關系不匹配)。

間接編碼：隨機序列在有向圖中的路徑生成不是一個好的選擇，間接編碼相比而來會是一個更好的選擇，且解決了直接編碼在遷移關系不匹配的問題。提出的間接編碼方式具體如下：隨機初始化一定長度的字符串，然后依次擴展狀態，直到達到最大的路徑長度到達目標節點。在每一次擴展路徑，且有多個遷移可以選擇時，通過當前編碼的字符去選擇相應的節點。

通過這種方式依次擴展路徑，直到結束路徑找到目標狀態或者達到最大搜索深度。同時，這種編碼可以在每一次擴展完一個狀態的時候，判斷當前狀態是否是目標狀態，如果是的話就停止狀態的擴展，減少了模型檢測的耗時，同時因為后續的所有差分進化算法都通過對字符串的編碼進行操作從而間接影響路徑生成，可以避免產生大量的無效路徑。這也是為什么選擇的是差分進化算法的一個原因，差分進化算法的優化過程是不會跟隨最優解的，而是采用隨機的方法。這樣通過改變字符的編碼間接改變狀態節點的選擇，對于整個優化過程不會帶來影響。

路徑生成算法見算法1。

算法1路徑生成算法

1.設置當前路徑的開始節點為初始節點S0，Π1=S0

2. fori=1->MaxLength

3.統計當前路徑的最后一個節點的后繼節點集合T，并得到集合長度size

4.計算ID=chromesome(i)%size，并且通過ID選擇集合中的第ID個后繼節點，即T(ID)

5.將選擇的節點作為當前路徑的最后一個節點，Πi=T(ID)

6.ifΠi==goal

7.停止循環，算法結束

8.end if

9. end while

算法1中，Π表示當前的路徑節點序列，MaxLength為狀態空間中搜索的最大深度，chromesome表示隨機的字符串，S0表示狀態搜索的初始節點，goal表示狀態搜索的目標節點。

1.3.2模擬退火操作

該操作是在差分進化算法已經生成了所有交叉個體之后的操作。為了防止當前種群中較優的部分個體依然沒有找到目標節點或者找到了目標節點但是路徑的適應值較差，即路徑較差。因此通過此處的變異操作在當前適應值最優的個體進行模擬退火操作，按照模擬退火中的Metropolis準則，以一定的概率接收次優解從而去尋找更優的路徑。其中，每一次對原始最優解進行高斯擾動來生成新解。模擬退火算法見算法2。

算法2模擬退火算法

1.oldchromesome=chromesome;oldroad=

Bestroad

2. whileTem>Tmin

3. for 馬爾科夫鏈長度

4.newchromesome=oldchromesome*g;

//對最優路勁對應的字符串進行高斯擾動

5. 根據算法1生成當前字符串對應的路徑newroad

6.Fitness(newroad);

//計算newroad的適應值

7.ifFitness(newroad)-Fitness(oldroad)<0

8.oldroad=newroad

9.oldchromesome=newchromesome

10. else

11. 按照Metropolis準則判斷當前新解是否要取代舊解

12. end for

13.Tem=Tem*alpha;//溫度衰減

14. end while

算法2中，Tem表示初始溫度，Tmin表示最低溫度，alpha表示溫度衰減率，oldchromesome和oldroad分別代表舊的字符串編碼和舊路徑，newchromesome和newroad分別代表新的字符串編碼和新路徑。

Metropolis準則就是以一定的概率選擇接受或者不接受新解。避免了算法每次都選擇適應值較高的路徑，從而局限了在狀態空間中的搜索范圍。

1.3.3Cr自適應參數

在搜索后期，對于路徑的搜索已經達到了一個穩定的狀態。為了讓差分進化算法的變異的概率Cr隨著迭代的過程依次增加，在后期提高其尋找更優路徑能力，同時增強跳出局部最優的能力。主要采用的是根據迭代的次數，逐漸增加變異的概率?；谶@樣一個直覺，隨著迭代過程的進行，優化的過程是—個逐漸趨近于更優的過程，同時也是一個趨向于更穩定的一個過程。在算法進行的后期，種群會保持相對穩定。因此，這種方法可以在后期增大變異概率，讓算法在后期依然保持較好的尋優能力。對于Cr的求值公式如下：

Cr=Crmin+(Crmax-Crmin)×iter/MaxEva

(4)

式中：Crmin表示最小變異概率，Crmax表示最大變異概率，iter表示當前迭代次數，MaxEva表示最大迭代次數。

1.3.4適應值函數

針對死鎖的模型檢測，其目標是在有向圖中找到一條從初始節點開始，且結束于目標節點的一條路徑，即反例。且如果反例的長度越短，就更有利于分析出問題?；谶@個認識，對于都找到了目標節點的2個路徑，其中，路徑長度越短，其適應值就越小，代表了其更優。同時，針對處理的關于死鎖的模型檢測問題，特別設置了—個啟發式量，即狀態可遷移量。統計一條完整路徑的狀態可遷移量的和，這是基于對于找到了死鎖的路徑，其可遷移量總和相比長度相當的未找到死鎖狀態的路徑，其可遷移量較少。對于沒有結束于目標節點的路徑，處理如下，添加一個較大的懲罰值，同時，以上的對于找到目標節點的路徑在該處同樣適用。根據以上的認識，對于具體適應值長度的計算公式如下：

(5)

1.3.5選擇策略

選擇的是錦標賽選擇算法。通過以上的過程，生成的路徑包括初始種群所生成的路徑N條，變異、交叉過程生成的路徑N條與模擬退火算法生成的路徑1條，共計2N+1條。將其中適應值最佳的路徑對應的字符串直接放入下一代種群，然后將剩下的2N條路徑分為N-1組，其中每組的路徑數為L=2N/N-1，通常L是除不盡的，采取的是向下取整的方式。

通過這種方法，在每一次的迭代過程中，既保證了最佳的路徑進入了下一代種群，同時也保證了其在狀態遷移圖中的搜索不會過于集中，影響搜索的效果。算法過程見算法3，其中N表示種群的大小。

算法3選擇策略

1.將當前路徑集合中最佳的路徑對應的字符串放入下一代種群

2.從集合中刪除該路徑

3.fori=1∶2->(N-1)

4.從剩余集合中隨機選擇L條路徑

5.將L條路徑中適應值最佳的路徑對應的字符串放入下一代種群中。

6.從集合中刪除已經選擇過的路徑

7.end for

基于以上內容，提出的算法具體流程如圖2所示。

圖2 死鎖檢測流程框圖

3 實驗與分析

采用Matlab實現了所設計的算法。采用隨機構造了多組含有死鎖節點的狀態空間圖并與多種算法相比，進行了下述實驗。分別是在不同狀態空間大小下2種算法所生成遷移數量的變化和所生成反例長度之間的變化。

在以上的搜索中，限定的最大迭代次數為100次。

圖3表明了算法迭代次數與狀態空間大小的關系。

圖3 迭代次數與狀態空間大小的關系曲線

從圖3中可以看出，算法在尋找目標路徑的過程中，隨著狀態空間的增大，迭代次數并不是一直保持線性增加，當狀態空間達到一定的大小時，迭代次數的增加會減緩。即表明該算法在狀態空間一直增大的情況下，依然可以保證一定的尋找目標路徑的速度。

同時比較了在采用Cr自適應參數和固定Cr的情況下，算法的收斂情況。可以看出，在前期狀態空間較小的情況下，兩者的收斂速度相差不大，隨著狀態空間的擴大，設置了自適應Cr參數的算法能夠擁有更快的收斂速度。

圖4表明隨著狀態空間的變化，4種模型檢測算法所生成反例長度的變化，其中包含了3種不確定算法和一種確定性算法。

從圖4中可以看出，基于啟發式因子選擇下一步節點的不確定算法與盲目搜索確定性算法相比，可以更快地找到目標節點，從而得到更短的反例。隨著狀態空間的增加，差距也會越來越大。

而與其他2種帶有啟發式因子的算法相比，由于在引導搜索方向上的優化，提出的算法在尋找最短反例上的表現也是更優的。

圖5表明了4種算法在進行檢測時，在狀態圖中所生成的遷移數量的關系?？梢钥闯觯瑔l式算法在生成更少的遷移，即在搜索相對較少狀態空間的情況下能夠找到死鎖節點，且在狀態空間增大的情況下，其生成遷移數量的增大幅度也小于傳統的確定性算法。從而證明了該帶有啟發式因子的算法在檢測時有更高的效率，在搜索較少的狀態節點的情況下，就能夠完成對于死鎖的檢測。

圖5 生成遷移數與狀態空間大小的關系曲線

同時對于3種不確定算法，提出的算法在搜索狀態空間的表現上仍然優于其他2種算法。這也是通過引導搜索方向和加速收斂帶來的優勢。

圖6表明了隨著狀態空間的增大，4種算法檢測用時的變化?？梢钥闯?，在狀態空間較小時，4種算法檢測用時差距不大，但是在狀態空間過大時，BFS由于是盲目搜索，與3種帶有啟發式因子的算法相比，其檢測用時極大，且增大幅度也是。相比于3種不確定算法，由于提出的算法優化了引導搜索的環節和加速收斂的方法，其檢測用時也均小于其他2種。

圖6 檢測用時與狀態空間大小的關系曲線

分析上述多個實驗可知，設計的基于差分進化算法的模型檢測算法，對比傳統的確定性算法BFS，其生成的反例長度和探索的遷移關系都遠小于BFS。同時，與其余不確定性算法相比，也優于其余2種算法。證明了在檢測死鎖方面，該算法能夠在搜索較少狀態空間的前提下，生成較短的反例，更有利于分析錯誤。

4 結論

1) 提出了一種新的啟發式模型檢測搜索算法，經過實驗證明，可以有效提高死鎖檢測的效率。

2) 針對路徑的特殊性，提出一種路徑生成算法，有效減少了不確定算法框架帶來的后續操作的復雜性。

3) 在差分進化算法原有框架下，增加額外的模擬退火操作，跟隨迭代次數自適應的Cr值，用以提高算法表現，加速算法的收斂。同時根據死鎖檢測的具體背景，設計了新的適應值函數用以評估路徑的優劣性。

未來的工作中，將擴展所提出算法的適用場景，使其能夠檢測更多的性質。同時將該算法與其他技術相結合，如偏序規約、抽象技術等，進一步降低搜索所需要的內存空間，即減少所生成的狀態圖大小。最后，基于以上的設想，開發出實際的模型檢測器。