模型檢測空間分解分布式算法的優(yōu)化與研究

潘懷宇，龍士工，鄭　涵

(貴州大學(xué) 計算機科學(xué)與技術(shù)學(xué)院，貴州 貴陽 550025)

?

模型檢測空間分解分布式算法的優(yōu)化與研究

潘懷宇，龍士工*，鄭涵

(貴州大學(xué) 計算機科學(xué)與技術(shù)學(xué)院，貴州 貴陽 550025)

模型檢測對于系統(tǒng)的校驗有著適用范圍廣、自動化驗證程度高、驗證速度快等優(yōu)勢。但是其狀態(tài)爆炸問題制約了其應(yīng)用，使用分布式技術(shù)緩解狀態(tài)爆炸問題引來了新的問題——如何對狀態(tài)空間進行分解。本文介紹了分布式SCC分解的兩個算法：FB與MP-MS算法，并在其基礎(chǔ)上，引入了OWCTY技術(shù)，對算法進行優(yōu)化。通過實驗，證明優(yōu)化后的算法有著更高的效率和更小的時間開銷，對于緩解狀態(tài)爆炸問題有著重要的意義。

模型檢測;狀態(tài)爆炸;OWCTY;分布式技術(shù)

日常生活中，人們對于ICT系統(tǒng)(Information and Communication Technology)的依賴正在迅速增長。隨著需求的增長，這些系統(tǒng)的結(jié)構(gòu)與分層也越來越復(fù)雜，類似的復(fù)雜系統(tǒng)我們隨處可見，比如智能卡、個人PC、手機和智能家居等。對于此類系統(tǒng)的可靠性、正確性與安全性保障，是系統(tǒng)在設(shè)計過程中的一個關(guān)鍵問題。模型檢測[1](Model Checking)作為形式化驗證方法的主要技術(shù)之一，其實質(zhì)是基于時序邏輯(LTL，CTL)的計算機自動化形式驗證的方法，利用窮舉搜索狀態(tài)空間來檢驗既有模型與一個時序邏輯公式，驗證該系統(tǒng)模型是否滿足此時序邏輯公式描述的具體性質(zhì)。模型檢測技術(shù)適用范圍廣、自動化驗證程度高、驗證速度快，只要計算機有足夠的處理能力，最終總能終止并給出驗證結(jié)果，當(dāng)驗證屬性不滿足時，還可以給出反例(Counterexample)，便于發(fā)現(xiàn)錯誤并進行修改。

模型檢測方法的嚴(yán)重缺陷是“狀態(tài)爆炸(state explosion)問題”。如圖1所示，隨著檢測的系統(tǒng)規(guī)模增大，其狀態(tài)空間由mn變大為mn1，模型檢測算法需要的時間、空間開銷呈指數(shù)增長，當(dāng)一個系統(tǒng)的并發(fā)分量非常多時，對其狀態(tài)空間進行直接窮舉搜索在實際上是不可行的。

圖1　狀態(tài)爆炸問題

分布式作為計算機科學(xué)當(dāng)前的熱門技術(shù)，主要研究如何把一個需要巨大計算能力才能解決的問題分成若干部分，然后把這些部分單獨處理，最后綜合以得到最終結(jié)果。其為解決狀態(tài)爆炸提供了良好的思路?？梢詫⑷譅顟B(tài)空間分解，多處理單元對各個子空間單獨驗證，最后得出驗證結(jié)果，理論上可以節(jié)約時間開銷。該思路的難點是全局狀態(tài)空間的分解。

本文中將系統(tǒng)有向圖的強連通分量(SCC)作為子狀態(tài)空間進行劃分，在整個空間狀態(tài)圖中尋找強連通分量。關(guān)于該問題的一個有效算法是基于深度優(yōu)先算法(DFS)的Tarjan算法，給定一個含有n個頂點，m條邊的圖，該算法能夠在O(n+m)的時間和O(n)的空間內(nèi)，識別并列出所有的強連通圖。但是，Tarjan算法所使用的DFS算法的并行化已經(jīng)被證明是困難問題，所以想要使用Tarjan算法來實現(xiàn)分布式的目的就非常困難。

本文中，我們將列出了兩種已有的分布式SCC分解算法：FB與MP-MS算法，給出算法思想與偽代碼，以及相關(guān)技術(shù)。并在其基礎(chǔ)上進行改進，引入OWCTY技術(shù)，提出改進算法O-BF算法。進行實驗，來比較各算法在時間開銷上的效率，比較的對象是Tarjan算法。

1　準(zhǔn)備知識

在介紹算法和相關(guān)技術(shù)之前，我們需要先了解一下分布式算法所涉及到的相關(guān)知識。

1.1分布式算法

分布式計算研究把一個大的問題分割成若干部分，使用多個處理單元分別處理，最后獲得結(jié)果。表1給出了分布式求π的例子來說明分布式算法的應(yīng)用，同時給出了使用單線程串行求解與多線程并行求解的時間開銷對比。

用數(shù)值積分法計算π，要求出在區(qū)間[0，1]內(nèi)函數(shù)曲線4/(1+x2)下的面積，此面積是π的近似值，為此先將區(qū)間[0，1]劃分成N個等間隔的子區(qū)間，每個子區(qū)間的寬度為1/N；然后計算出各子區(qū)間中點處的函數(shù)值；再將各個子區(qū)間面積相加就可得出π的近似值。其計算公式為：

表1　數(shù)值計分法求π，單線程串行與 多線程并行時間開銷對比

1.2有向圖

對于SCC的分解，首先要了解有向圖的相關(guān)定義。一個有向圖可以表示為一個二元集合(V，E)，其中V是圖中頂點的集合，而E∈V×V，是有向邊的集合。如果(u，v)∈E，則稱u是v的直接前驅(qū)，v是u的直接后繼。對于頂點v，它的直接前驅(qū)u的數(shù)目稱為頂點的入度。對于圖G=(V，E)，將它所有的有向邊反轉(zhuǎn)，得到它的換位圖(transposed graph)GT=(V，ET)，其中ET={(u，v)|(v，u)∈E}。

假設(shè)E*為有向圖G=(V，E)的傳遞和自反閉包，s，t∈V是圖中的兩個頂點。如果(s，t)∈E*，則稱頂點t是自頂點s可達，如果有一頂點序列：s0，s1......sk，s.t.(si，si+1)∈E，如果sk是自s0可達的，則這一頂點序列稱為一條路徑。如果路徑上不包含重復(fù)的頂點，則稱該路徑是一條簡單路徑，其長度為k，即邊的數(shù)目。

在有向圖中，頂點集合C滿足C∈V，如果任意兩個頂點u，v∈C，滿足頂點v都是自頂點u可達，則稱C是有向圖中的一個強連通分量(SCC)，如果有向圖任意強連通分量C*，滿足C?C*?V，則稱該C為一個最大強連通分量。

v∈W∈V、Ew={(x，y)∈E∧x，y∈W}，圖(V，Ew)中所有可達頂點v的頂點集合稱為頂點v的向前閉合(forward closure)，同理頂點的向后閉合(backward closure)指的是自頂點可達的所有頂點集合。

對于一個顯示的有向圖，在計算機中通過鄰接表或鄰接矩陣來描述。對于一個隱式圖(隱式圖指的是它有一個初始頂點和一個限定函數(shù)返回任意頂點的直接后繼)，比如說對于一個系統(tǒng)，它的有向圖描述不能直接描述，需要通過算法將其轉(zhuǎn)化為一個有向圖，文獻[2]中就提到了兩種隱式圖的描述算法，在本文中使用工具Divine，直接將系統(tǒng)轉(zhuǎn)化為有向圖。

1.3可達性關(guān)系

可達性關(guān)系的計算是SCC分解算法中的核心，主要是查找從一個給定的頂點可以到達的所有頂點，即計算其向前閉包。圖的標(biāo)準(zhǔn)廣度優(yōu)先搜索或深度優(yōu)先搜索都可以實現(xiàn)這樣的效果，其空間復(fù)雜度為O(n)，時間復(fù)雜度O(m+n)。

可達性程序是SCC分解算法的第一步，該部分的算法的并行化經(jīng)過多年研究已經(jīng)成為了一種標(biāo)準(zhǔn)技術(shù)[3-5]?？蛇_性程序的并行化技術(shù)中，一個分區(qū)函數(shù)將頂點分配給多個處理器。每個處理器負責(zé)搜索由分區(qū)函數(shù)分配給它的頂點，包含一組已訪問的頂點和一個待訪問頂點的列表。

本文描述的算法中既提到了向前可達性，也使用到向后可達性的概念。一個向后可達性程序的功能就是確定所有自給定頂點可達的頂點。

1.4中值點選擇

無論是向前可達點的搜索，還是向后可達點的搜索，都需要算法從某個指定的點開始，這個給定的點，稱之為中值點。中值點的選取對于算法的復(fù)雜度有很大的影響。如果我們選擇的中值點所向前向后可達性遍歷的頂點集合中沒有已經(jīng)被分解出來的點，那么相應(yīng)的所有頂點，可以只使用在中值點發(fā)起的單個向前可達性來鑒定。可是挑選滿足上述條件的中值點，需要使用到深度優(yōu)先搜索后順序。本文算法中是隨機選擇中值點，中值點選取的并行化仍是一個很好的研究方向。

2　算法

介紹了相關(guān)知識之后，我們接下來會首先介紹兩個基本的分布式SCC分解算法，再提出一個基于此算法的改進算法，并分析其可行性。

2.1FB算法

FB算法是SCC分布式分解的基礎(chǔ)算法，圖2給出了算法的基本步驟：首先，在圖中隨機選擇中值點，然后從中值點開始向前、向后進行遍歷，此過程將圖分成四個獨立的子圖。圖中頂點分別是：在向前遍歷區(qū)域不在向后遍歷區(qū)域、在向后遍歷區(qū)域不在向前遍歷區(qū)域、既在向前遍歷區(qū)域又在向后遍歷區(qū)域以及既不在向前遍歷區(qū)域又不在向后遍歷區(qū)域。既在向前遍歷區(qū)域又在向后遍歷區(qū)域中的點所組成的子圖就是一個SCC，不需要再進行分解。而其他三種子圖，則需要進行進一步分解。圖3中給出了該算法的偽代碼：

圖2　FB算法步驟

圖3FB算法偽代碼

算法包括中值點選取PIVOT、向前向后遍歷。向前向后兩個可達性遍歷過程有兩個參數(shù)：中值點和狀態(tài)集(頂點集合)。該算法的復(fù)雜度為O(n·(n+m))。

2.2MP-MS算法

算法MP-MS[6]是FB算法的改進版本，使用了最大前驅(qū)和最大后繼的概念。相比于FB算法，主要的不同是在圖的遍歷過程，為了計算出頂點的最大前驅(qū)和后繼(文獻[7]中給出了一個算法來計算最大前驅(qū)與后繼)，使用并行程序FWD-MAXPRED和BWDMAXSUCC替換FWD和BWD程序。除了遍歷向前向后可達性關(guān)系以外，新的程序還可以根據(jù)前驅(qū)和后繼的最大值來劃分子圖，圖4給出了其子圖劃分，并返回子圖中的頂點，得到前驅(qū)列表及后繼列表，可以被用于對劃分的子圖進行遞歸調(diào)用。圖5給出了算法的偽代碼：

圖4　使用最大前驅(qū)與最大后繼來劃分子圖

圖5MP-MS算法

2.3O-BF算法

在使用FB算法或者MP-MS算法之前，我們觀察到，給定一個有向圖，對其進行SCC分解，有很多不需要考慮的狀態(tài)點。一個SCC中的任何頂點都需要滿足至少有一個前驅(qū)和后繼，也就是說，一個沒有任何前驅(qū)或后繼的點必然不屬于SCC，基于此思考，可以在使用上述FB、MP-MS之前對圖進行約減。

在這樣的思想上，本文引入了OWCTY技術(shù)[4](單項約減消除技術(shù))來對圖進行處理，圖6是對 OWCTY技術(shù)的代碼描述。

圖6OWCTY技術(shù)

OWCTY算法有三個參數(shù)，G表示待分解的圖，F(xiàn)表示可接受狀態(tài)集，init_state表示初始狀態(tài)點，reachability(S∩F)遍歷出所有自初始狀態(tài)點可達頂點集合。elimination(S)查找出的頂點集合滿足：頂點屬于S中某個環(huán)或自S中某個環(huán)中任意頂點可達。

以圖2為例， LT和TT頂點可以被OWCTY識別，其沒有前驅(qū)或后繼將被消除，消除這樣的頂點會產(chǎn)生新的頂點，這些頂點中也會有頂點沒有前驅(qū)或后繼，遞歸使用OWCTY消除。隨著無用頂點的消除，圖的規(guī)模越來越小，圖中的平凡組件可能會成為圖中的頭或尾節(jié)點。圖2中包括三種平凡組件(Trivial components)：LT、TT以及既不是頭也不是尾的平凡組件(T)。

O-BF算法的核心思想就是將OWCTY技術(shù)與FB算法相結(jié)合，先使用OWCTY將圖中無用的頂點消除，再使用FB算法進行SCC分解。

該算法將重復(fù)使用OWCTY技術(shù)對圖進行無用點的消除，每次迭代將會得出一個OBF子圖，然后對每一個OBF子圖進行FB分解。圖7與圖8分別給出了OBF算法的偽代碼和步驟描述:

圖7OBF算法

圖8　OBF算法的兩個步驟

程序從初始頂點開始(圖中沒有直接前驅(qū)的節(jié)點)。OWCTY消除過程遍歷所有初始頂點的直接后繼，消除所有沒有前驅(qū)的頂點，圖中有叉的頂點是OWCTY消除過程不可消除的頂點。從這些點進行一次向后可達性遍歷，得到一個OBF切片(頂點集合B)。偽代碼第8行開始使用FB算法并行執(zhí)行，對OBF切片進行分解，得出一個SCC。將當(dāng)前SCC中頂點的直接后繼(不屬于該SCC中的頂點)作為新的初始頂點，遞歸調(diào)用OBF算法，最終可以在O(n·(n+m))時間內(nèi)得到所有的SCC。

3　實驗與結(jié)果

下面將在算法基礎(chǔ)上進行編程實驗，實驗環(huán)境為：機器A:8G Rom，2.60 GHz Cpu，4 Cores。機器B:6G rom、2.80 GHz、2Cores。

本文實驗中使用的系統(tǒng)(電梯調(diào)度算法、Peterson算法和Rether9_2)都來自DiVine[8]工具庫。在表2中列出其相關(guān)參數(shù)，包括：名稱、頂點與邊數(shù)目、平凡以及非平凡強連通圖的數(shù)目、使用Tarjan算法所需要的時間。

表2　系統(tǒng)參數(shù)

實驗得出表3中的結(jié)果，其算法時間開銷對比如圖9所示：

表3　實驗結(jié)果(n.a表示2個小時內(nèi)得不出結(jié)果)

圖9　算法時間開銷對比(min)

對于結(jié)果進行分析，發(fā)現(xiàn)：

(1)當(dāng)前實驗環(huán)境下，對于MP-MS算法，基于最大前驅(qū)與后繼的改進算法實際效果并不是很好，其所花費的時間開銷遠遠大于其他算法。

(2)在處理單元數(shù)目不是很多的情況下，分布式SCC基礎(chǔ)算法FB的效果并沒有串行算法Tarjan效果好。

(3)實驗結(jié)果表面，使用OWCTY技術(shù)的OBF算法對于時間開銷上的優(yōu)化非常明顯，即便是處理器數(shù)目不是很多的情況下，時間上也提高了10%以上。

最后，根據(jù)我們的實驗，改進后的OBF算法對于圖的SCCs分解在時間開銷上要優(yōu)于串行的Tarjan算法。

4　結(jié)語

對于模型檢測的狀態(tài)爆炸問題，可以使用分布式技術(shù)一定程度上緩解。而對于其全局狀態(tài)空間的劃分，可以使用相應(yīng)的算法改進效率。

本文詳細介紹了相關(guān)的分布式SCC分解算法，并對其進行優(yōu)化，實驗結(jié)果表明，優(yōu)化后的O-BF算法效果明顯，算法的效率有了顯著的提高。

本文僅使用了簡單的多線程編程來進行實驗，線程間的通信問題有欠考慮，時間開銷還有進一步優(yōu)化的空間，另外，在中值點的選取方面都有可以優(yōu)化的空間。

[1] Baier C， Katoen J P. Principles of model checking[M]. Cambridge: MIT press， 2008.

[2] Garavel H， Mateescu R， Smarandache I. Parallel state space construction for model-checking[M]. Berlin Heidelberg: Springer-Verlag， 2001: 217-234.

[3] Blom S， Calamé J R， Lisser B， et al. Distributed analysis with μCRL: a compendium of case studies[M]. Berlin Heidelberg: Springer-Verlag， 2007: 683-689.

[4] Fisler K， Fraer R， Kamhi G， et al. Is there a best symbolic cycle-detection algorithm?[M]. Berlin Heidelberg: Springer-Verlag， 2001: 420-434.

[5] Lerda F， Sisto R. Distributed-memory model checking with SPIN[M]. Berlin Heidelberg: Springer-Verlag， 1999: 22-39.

[6] Sminia T， Orzan S M. On distributed verification and verified distribution[D]. Amsterdam: Vrije Universiteit， 2004.

(責(zé)任編輯：曾晶)

Optimization and Research of Distributed Algorithm for Model Checking Space Decomposition

PAN Huaiyu，LONG Shigong*，ZHENG Han

(College of Computer Science and Technology， Guizhou University， Guiyang 550025， China)

Model Checking has many advantages in system verification: wide range of applications， high degree of automation and high speed. But its state explosion problem restricts its application. Using the distributed technology to mitigate state explosion leads to a new problem -- how to decompose the state space? Two algorithms about distributed SCC decomposition were described: FB and MP-MS algorithm. Then the OWCTY technology was applied in optimizing these two algorithms. Through the experiment， the results show that the optimization algorithm has a higher efficiency and less time cost. It has important significance to alleviating the problem of state explosion.

model checking;state explosion; OWCTY; distributed technology

A

1000-5269(2016)03-0086-05

10.15958/j.cnki.gdxbzrb.2016.03.21

2015-12-07

國家自然科學(xué)基金(61163001

潘懷宇(1991-)，男，在讀碩士，研究方向：密碼學(xué)與可信計算，Email：578943277@qq.com.

龍士工，Email：526796467@qq.com.

TP301