多核模型檢測工具CTAV的實現與優化①

趙 威

(中國科學院 軟件研究所 計算機科學國家重點實驗室,北京 100190)

(中國科學院大學,北京 100049)

實時系統是指這樣的一類計算機應用系統,它要求在一定時限內及時的響應外部事件,并在一定時限內完成事件的處理.在這類系統中,確保其準確性和可靠性非常重要,一旦出現缺陷,帶來的經濟財產損失都是巨大的.實時系統的模型檢測[1]是確保實時系統的可靠性和正確性的一種重要技術,它通過遍歷狀態空間尋找是否存在不滿足規約的狀態或路徑來驗證系統是否正確可靠.

時間自動機模型是實時系統最廣泛使用的一種數學模型,針對實時系統的模型檢測工具主要采取時間自動機作為形式模型,以計算樹邏輯(Computation Tree Logic,CTL)[1]或線性時序邏輯(Linear Temporal Logic,LTL)[1]作為性質描述語言.典型的代表有UPPAAL、KRONOS、RED以及CTAV等.

CTAV[2]是中科院軟件所在2009年實現的一個關于時間自動機的符號化模型檢測工具,在關于時間自動機的模型檢測中它是第一個針對線性時序邏輯LTL的模型檢測工具,它先將時間自動機關于LTL的模型檢測化歸為時間Büchi自動機的空性檢測,然后文獻[2]中證明了時間Büchi自動機的空性檢測可通過zone抽象化歸為Büchi自動機的空性檢測,這樣就可以利用Büchi自動機的空性檢測算法來完成時間自動機關于LTL的模型檢測.基于這一方法,文獻[3]最早實現了時間自動機關于LTL的符號化模型檢測,這里符號化的含義是指模型檢測使用的是時間自動機的基于zone的符號化語義.文獻[2]中使用的Büchi自動機的空性檢測算法是單線程的.2013年,文獻[4–7]在其多核模型檢測工具LTSmin的基礎上利用文獻[2]中的方法實現了時間自動機關于LTL的多核模型檢測工具LTSmin+opaal,使得驗證效率有了較大的提高.與此同時捷克人在他們的多核模型檢測工具DIVINE3.0[8,9]中也實現了時間自動機關于LTL的多核模型檢測.本文我們將在文獻[10–12]中給出的關于Büchi自動機的多核模型檢測算法的基礎上在CTAV工具中實現時間Büchi自動機關于LTL的多核模型檢測,與LTSmin+opaal和DIVINE3.0相比,在系統描述語言方面,我們工具支持比時間自動機表達能力更強的時間Büchi自動機,其它兩個只支持時間自動機模型,這一點對證明活性性質至關重要,在性質描述語言方面,由于CTAV本身可以支持LTL的實時擴展MTL0,∞(Metric Temporal Logic)[3],所以我們的工具將能比其它兩個工具支持更多的性質驗證.

本文的主要內容如下:研究了多種Büchi自動機的多核空性判定算法,基于文獻[10–12]實現時間Büchi自動機關于LTL的多核模型檢測,同時對比了多種多核算法在CTAV工具下的效果,并基于符號化狀態之間的包含關系給出了一種優化方法,并最終對比了divine的實驗結果.

1 基本概念

1.1 時間自動機

時間自動機[13]就是帶有時鐘集的有限自動機.時鐘集是有限個時鐘的集合,每個時鐘都是一個取值為非負實數的變量.時間自動機狀態之間的轉換要滿足時鐘約束才可能發生.時間自動機的狀態可以附加上“節點不變量”的屬性,這也是一個時鐘約束,用來保證狀態不會保持在原地不動.

時間自動機的形式化定義[14]是一個六元組M=

(1)X為時鐘變量的有限集合,C(X)為X上時鐘約束的集合,其定義為:

其中,x∈X,～ ∈{<,≤,==,＞,≥},c是非負整數.

(2)L是節點的非空有限集合,l0∈L是初始節點.

(4)Σ為標號的有限集合.

時間自動機M的遷移動作主要包含2種,分別是延遲遷移和離散遷移.

1.2 Zone[15]

假設X為時鐘變量的有限集合,Φ(X)為時鐘變量集合X上擴展時鐘約束的集合,擴展時鐘約束的語法定義如下:

式中:x,yX,～{<,≤,＞,≥},c是非負整數.對于時鐘賦值u,u滿足擴展的時鐘約束的充分必要條件是在賦值u下為真.

Zone通常用DBM(Difference Bound Matrices)[16]來表示.

DBM是一個矩陣,矩陣中的每一個元素是一組時鐘的兩兩差值.其定義了一個值為0的絕對時鐘,對于DBMD中的元素Dij表示其中的第i行第j列,它表示zone中時鐘變量i和時鐘變量j形成的時鐘約束.

例如,一個時鐘區域x≥6∧0≤y≤3∧y≤x–1,引入絕對時鐘后可以將表達式改寫成 0–x≤–6∧0–y≤0∧y–0≤3∧y–x≤–1,用 3×3 矩陣表示,分別為:

其中INF表示無窮大.

1.3 符號化語義

假設D表示一個zone,Y是時鐘集合,對其延遲和重置定義如下:

D↑={u+d|u∈D,d∈R≥0},表示 zone的延遲定義;

r(D)={u[Y:=0]|u∈D},表示zone的重置.

時間自動機(如圖1)的符號化狀態是(l,D),l是節點,D是zone.初始狀態(l0,D0↑∧Inv(l0)),l0是初始節點,D0表示所有時鐘都為0.

時間自動機的符號化語義為以(l,D)為狀態的遷移系統,遷移(l′,D′)→?a(l′′,D′′),如果有(l,g,a,Y,l1)∈E,并且D′′=((D′∧g)[Y:=0]∧Inv(l′′))↑ ∧Inv(l′′),D′′不為空.

圖1 簡單的自動機

圖1中的時間自動機在符號化語義下的一個可能遷移序列如下:

其中loop表示自循環遷移,并且這個遷移前后的狀態不相同,這個遷移系統有無窮多個狀態.

2 原理

2.1 模型檢測

給定時間自動機M=(L,l0,Σ,x,I,E)和LTL公式φ,要檢驗LTL性質是否被時間自動機M所滿足.在文獻[2]中提出了一種檢測算法,主要思路是先將公式?φ轉化為一個Büchi自動機M?φ,然后檢驗M與M?φ的合成M‖M?φ是否為空,這樣將LTL性質的檢驗轉換為對M‖M?φ的空性判定,而對此類空性判定,通過使用基于zone的符號化語義將M‖M?φ轉化成一個Büchi自動機,然后利用Büchi 自動機空性檢測算法來完成.

將檢驗LTL性質是否被時間自動機所滿足轉換為對Büchi自動機空性檢測的結果,若空性檢測的結果為空,則性質被自動機M所滿足;反之若空性檢測的結果不為空,則性質不被自動機M所滿足.

2.2 符號化狀態

在符號化狀態抽象表示過程中,狀態的表示我們是采取DBM來表示的,因此狀態之間會產生集合的包含關系,在狀態展開的遍歷過程中我們采取判斷狀態是否遍歷過或者已經在被刪除狀態集合中來對其進行后續處理,在文獻[4]中我們得到以下引理.

引理1.在狀態空間中如果有Sk?Sj,并且Sk可以到達接受環,那么Sj也可以到達.

證明:假設Sj不能到達可接受環,而Sk能到達,而Sk?Sj代表自動機中各個進程所處節點一樣,僅僅時間約束不同,如圖2,Sj如果不能到達可接受環,那么Sk肯定不能,與條件矛盾.

引理2.在狀態空間中如果有Sk?Sj,并且Sk到Sj之間包含一個接受狀態,那么Sk可以到達接受環.

證明:狀態Sj是狀態Sk的超集,而狀態Sk能到達Sj,由DBM表示的時間約束是凸性的,可以將Sj分為Sk和Sj–Sk兩部分,故可得發現環.

由引理1還可以得出以下結論,在狀態空間中如果有Sj?Sk,并且Sk不可以到達接受環,那么Sj也不可以到達.這個結論有助于避免不必要的狀態展開,由引理1逆否命題可得.

圖2 Sk與Sj

3 多核模型檢測工具的實現與優化

3.1 算法簡介

文獻[10]中提出了一種基于Tarjan[17]和Dijkstra[18]算法而形成的多核并行空性檢測算法,并且實現在SPOT庫中,這個算法的主要思路如下:采用共享的終止條件stop和一個并查集結構使得多個線程可以共享狀態遍歷結果,而狀態展開過程就是一個深度優先遍歷過程,在這個過程中的每一步會首先找出狀態節點是處在未遍歷狀態、已經遍歷或者已經遍歷完全的狀態.從初始狀態開始,把遍歷序號依次賦值給展開狀態,其中當前圖的所有狀態的序號都不為0.如果當前狀態的所有后繼都已經被遍歷過,并且仍然不滿足接受條件,則說明該狀態和其后續狀態不在接受路徑中,將它們的遍歷序號賦值為0,表示已經從當前圖中刪除,放入被刪除狀態中.在找到一條接受路徑或者完全展開全部狀態后停止.算法偽代碼如圖3和圖4.

圖3 算法主流程

在算法展開狀態過程中假設S表示狀態節點,有遷移S0→S1,則S1是當前遍歷到的狀態節點,有如下可能:

(1)S1沒有遍歷,返回UNKNOWN(表示未遍歷),將其放入深度優先棧dfs中,同時加入hash表中,其中dfs表示存儲遍歷過程中狀態的棧,其每個元素由<當前狀態,當前遷移的接收條件,標識符,當前狀態未遍歷的后繼＞這樣的四元組構成,hash表存儲所有狀態并給予唯一的標識符,Dead表示刪除狀態集合,即已遍歷完全無法滿足接受條件的狀態集合,Livenum存儲活著的（不屬于Dead集合的）狀態.

(2)S1出現在了Livenum表中,即出現在當前圖,說明發現了環,這樣我們需要判斷該環是否滿足接受條件,如果滿足則賦值stop=1,標記終止符為1表示結束算法,當前線程直接返回,其它線程收到stop=1,也立即返回,表示找到了路徑,性質不滿足.

(3)S1出現在Dead中,即S1的所有后繼已經遍歷,不會出現滿足條件的接受環,那么直接跳過.

圖4 混合算法

3.2 算法優化

基于此我們采取了相應的改進措施,通過文獻[3]應用于LTSmin多線程算法的改進,我們將其應用到了我們算法上,主要改進思路有以下兩點:

如果有遷移S1→S2,如果Get_status(S2)返回UNKNOWN,我們增加以下判斷:

(1)如果S2是已遍歷而且非死亡狀態中的狀態的超集,即存在S3屬于livenum,并且S3包含于S2,則我們可以將其作為發現一個環,以此判斷找到了環,進行是否包含接受條件的判斷.

(2)如果S2是Dead狀態的子集,直接由引理1得,S2后繼肯定不會出現環,可以直接跳過.

基于這兩點,我們對算法進行了相應的改動,改動偽代碼如圖5,算法及優化全部實現在CTAV工具中,我們對結果進行了對比研究,主要基于展開狀態的變化,如表1結果顯示,在部分模型取得了不錯的效果.

3.3 算法效果比較

在多線程算法中,單一算法在發現環的過程中往往在某一方面表現十分優秀,而在某些例子也存在極差的表現,在工具實現過程中基于Tarjan、Dijkstra算法,我們比較了這兩種多核算法的區別,Tarjan算法主要表現在每發現環的時候只pop最后的邊,而Dijkstra算法在發現環的時候將當前圖除根節點全部pop,這會直接導致發現接受圖的效率問題,為此,我們采取了混合算法,讓一部分線程跑Tarjan,一部分線程跑Dijkstra,在實驗中,我們通過給線程加上整數標識,讓奇數線程運行Dijkstra算法,偶數線程運行Tarjan算法.最終表現結果如表2,在結果中我們發現混合算法表現良好,在各種模型下能取得相對于單一算法更佳的時間效率效果.

圖5 算法改進

表2 混合算法效果對比結果

4 實驗研究

最終我們完成了多核模型檢測工具的開發和優化,如表3顯示train-gate模型下性質“[](“trans(0).Appr”→<＞(“trains(0).Cross”))”為例線程數量和模型復雜化后時間效率的提升變化,表中“原”代表原單核工具,后續數字表示新工具采取的線程數量.實驗效果顯示多核模型檢測工具的效果提升是顯著的,基本與線程數量成線性相關,當然由于機器核數的影響,在達到峰值即機器支持的線程核數后有所下降.

表3 多核CTAV對比單核表現結果

同時,我們對比了divine工具和我們工具在4線程下的時間效率,在部分模型中取得了更好的效果,如表4.

表4 divine和ctav對比

5 結束語

通過采用基于Tarjan和dijkstra的多線程并行的模型檢測算法,我們提高了CTAV工具對CPU的利用率,以此提高了CTAV工具的時間效率,同時通過符號化狀態的包含關系我們提出了多核算法下的優化方案,對狀態空間的約減有一定的優化作用,同時在CTAV工具下對比了多種多核空性檢測算法的效率,并采取混合多線程算法完成了工具的開發.當然,多核模型檢測工具的優化仍然需要進一步的研究,簡單的利用符號化狀態的包含關系約減的優化效果并不明顯,進一步的優化也是我們下一步的工作.同時,最新的研究中也產生了很多采取分布式資源對系統進行模型檢測的研究,如文獻[19]提出采用分布式資源對發布訂閱結構系統進行模型檢測.對于如何利用分布式系統進一步提高工具的效率也是我們下一步的研究方向.