多核模型檢測(cè)工具CTAV的實(shí)現(xiàn)與優(yōu)化①

趙 威

(中國(guó)科學(xué)院 軟件研究所 計(jì)算機(jī)科學(xué)國(guó)家重點(diǎn)實(shí)驗(yàn)室,北京 100190)

(中國(guó)科學(xué)院大學(xué),北京 100049)

實(shí)時(shí)系統(tǒng)是指這樣的一類計(jì)算機(jī)應(yīng)用系統(tǒng),它要求在一定時(shí)限內(nèi)及時(shí)的響應(yīng)外部事件,并在一定時(shí)限內(nèi)完成事件的處理.在這類系統(tǒng)中,確保其準(zhǔn)確性和可靠性非常重要,一旦出現(xiàn)缺陷,帶來(lái)的經(jīng)濟(jì)財(cái)產(chǎn)損失都是巨大的.實(shí)時(shí)系統(tǒng)的模型檢測(cè)[1]是確保實(shí)時(shí)系統(tǒng)的可靠性和正確性的一種重要技術(shù),它通過(guò)遍歷狀態(tài)空間尋找是否存在不滿足規(guī)約的狀態(tài)或路徑來(lái)驗(yàn)證系統(tǒng)是否正確可靠.

時(shí)間自動(dòng)機(jī)模型是實(shí)時(shí)系統(tǒng)最廣泛使用的一種數(shù)學(xué)模型,針對(duì)實(shí)時(shí)系統(tǒng)的模型檢測(cè)工具主要采取時(shí)間自動(dòng)機(jī)作為形式模型,以計(jì)算樹(shù)邏輯(Computation Tree Logic,CTL)[1]或線性時(shí)序邏輯(Linear Temporal Logic,LTL)[1]作為性質(zhì)描述語(yǔ)言.典型的代表有UPPAAL、KRONOS、RED以及CTAV等.

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

本文的主要內(nèi)容如下:研究了多種Büchi自動(dòng)機(jī)的多核空性判定算法,基于文獻(xiàn)[10–12]實(shí)現(xiàn)時(shí)間Büchi自動(dòng)機(jī)關(guān)于LTL的多核模型檢測(cè),同時(shí)對(duì)比了多種多核算法在CTAV工具下的效果,并基于符號(hào)化狀態(tài)之間的包含關(guān)系給出了一種優(yōu)化方法,并最終對(duì)比了divine的實(shí)驗(yàn)結(jié)果.

1 基本概念

1.1 時(shí)間自動(dòng)機(jī)

時(shí)間自動(dòng)機(jī)[13]就是帶有時(shí)鐘集的有限自動(dòng)機(jī).時(shí)鐘集是有限個(gè)時(shí)鐘的集合,每個(gè)時(shí)鐘都是一個(gè)取值為非負(fù)實(shí)數(shù)的變量.時(shí)間自動(dòng)機(jī)狀態(tài)之間的轉(zhuǎn)換要滿足時(shí)鐘約束才可能發(fā)生.時(shí)間自動(dòng)機(jī)的狀態(tài)可以附加上“節(jié)點(diǎn)不變量”的屬性,這也是一個(gè)時(shí)鐘約束,用來(lái)保證狀態(tài)不會(huì)保持在原地不動(dòng).

時(shí)間自動(dòng)機(jī)的形式化定義[14]是一個(gè)六元組M=

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

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

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

(4)Σ為標(biāo)號(hào)的有限集合.

時(shí)間自動(dòng)機(jī)M的遷移動(dòng)作主要包含2種,分別是延遲遷移和離散遷移.

1.2 Zone[15]

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

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

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

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

例如,一個(gè)時(shí)鐘區(qū)域x≥6∧0≤y≤3∧y≤x–1,引入絕對(duì)時(shí)鐘后可以將表達(dá)式改寫成 0–x≤–6∧0–y≤0∧y–0≤3∧y–x≤–1,用 3×3 矩陣表示,分別為:

其中INF表示無(wú)窮大.

1.3 符號(hào)化語(yǔ)義

假設(shè)D表示一個(gè)zone,Y是時(shí)鐘集合,對(duì)其延遲和重置定義如下:

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

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

時(shí)間自動(dòng)機(jī)(如圖1)的符號(hào)化狀態(tài)是(l,D),l是節(jié)點(diǎn),D是zone.初始狀態(tài)(l0,D0↑∧Inv(l0)),l0是初始節(jié)點(diǎn),D0表示所有時(shí)鐘都為0.

時(shí)間自動(dòng)機(jī)的符號(hào)化語(yǔ)義為以(l,D)為狀態(tài)的遷移系統(tǒng),遷移(l′,D′)→?a(l′′,D′′),如果有(l,g,a,Y,l1)∈E,并且D′′=((D′∧g)[Y:=0]∧Inv(l′′))↑ ∧Inv(l′′),D′′不為空.

圖1 簡(jiǎn)單的自動(dòng)機(jī)

圖1中的時(shí)間自動(dòng)機(jī)在符號(hào)化語(yǔ)義下的一個(gè)可能遷移序列如下:

其中l(wèi)oop表示自循環(huán)遷移,并且這個(gè)遷移前后的狀態(tài)不相同,這個(gè)遷移系統(tǒng)有無(wú)窮多個(gè)狀態(tài).

2 原理

2.1 模型檢測(cè)

給定時(shí)間自動(dòng)機(jī)M=(L,l0,Σ,x,I,E)和LTL公式φ,要檢驗(yàn)LTL性質(zhì)是否被時(shí)間自動(dòng)機(jī)M所滿足.在文獻(xiàn)[2]中提出了一種檢測(cè)算法,主要思路是先將公式?φ轉(zhuǎn)化為一個(gè)Büchi自動(dòng)機(jī)M?φ,然后檢驗(yàn)M與M?φ的合成M‖M?φ是否為空,這樣將LTL性質(zhì)的檢驗(yàn)轉(zhuǎn)換為對(duì)M‖M?φ的空性判定,而對(duì)此類空性判定,通過(guò)使用基于zone的符號(hào)化語(yǔ)義將M‖M?φ轉(zhuǎn)化成一個(gè)Büchi自動(dòng)機(jī),然后利用Büchi 自動(dòng)機(jī)空性檢測(cè)算法來(lái)完成.

將檢驗(yàn)LTL性質(zhì)是否被時(shí)間自動(dòng)機(jī)所滿足轉(zhuǎn)換為對(duì)Büchi自動(dòng)機(jī)空性檢測(cè)的結(jié)果,若空性檢測(cè)的結(jié)果為空,則性質(zhì)被自動(dòng)機(jī)M所滿足;反之若空性檢測(cè)的結(jié)果不為空,則性質(zhì)不被自動(dòng)機(jī)M所滿足.

2.2 符號(hào)化狀態(tài)

在符號(hào)化狀態(tài)抽象表示過(guò)程中,狀態(tài)的表示我們是采取DBM來(lái)表示的,因此狀態(tài)之間會(huì)產(chǎn)生集合的包含關(guān)系,在狀態(tài)展開(kāi)的遍歷過(guò)程中我們采取判斷狀態(tài)是否遍歷過(guò)或者已經(jīng)在被刪除狀態(tài)集合中來(lái)對(duì)其進(jìn)行后續(xù)處理,在文獻(xiàn)[4]中我們得到以下引理.

引理1.在狀態(tài)空間中如果有Sk?Sj,并且Sk可以到達(dá)接受環(huán),那么Sj也可以到達(dá).

證明:假設(shè)Sj不能到達(dá)可接受環(huán),而Sk能到達(dá),而Sk?Sj代表自動(dòng)機(jī)中各個(gè)進(jìn)程所處節(jié)點(diǎn)一樣,僅僅時(shí)間約束不同,如圖2,Sj如果不能到達(dá)可接受環(huán),那么Sk肯定不能,與條件矛盾.

引理2.在狀態(tài)空間中如果有Sk?Sj,并且Sk到Sj之間包含一個(gè)接受狀態(tài),那么Sk可以到達(dá)接受環(huán).

證明:狀態(tài)Sj是狀態(tài)Sk的超集,而狀態(tài)Sk能到達(dá)Sj,由DBM表示的時(shí)間約束是凸性的,可以將Sj分為Sk和Sj–Sk兩部分,故可得發(fā)現(xiàn)環(huán).

由引理1還可以得出以下結(jié)論,在狀態(tài)空間中如果有Sj?Sk,并且Sk不可以到達(dá)接受環(huán),那么Sj也不可以到達(dá).這個(gè)結(jié)論有助于避免不必要的狀態(tài)展開(kāi),由引理1逆否命題可得.

圖2 Sk與Sj

3 多核模型檢測(cè)工具的實(shí)現(xiàn)與優(yōu)化

3.1 算法簡(jiǎn)介

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

圖3 算法主流程

在算法展開(kāi)狀態(tài)過(guò)程中假設(shè)S表示狀態(tài)節(jié)點(diǎn),有遷移S0→S1,則S1是當(dāng)前遍歷到的狀態(tài)節(jié)點(diǎn),有如下可能:

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

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

(3)S1出現(xiàn)在Dead中,即S1的所有后繼已經(jīng)遍歷,不會(huì)出現(xiàn)滿足條件的接受環(huán),那么直接跳過(guò).

圖4 混合算法

3.2 算法優(yōu)化

基于此我們采取了相應(yīng)的改進(jìn)措施,通過(guò)文獻(xiàn)[3]應(yīng)用于LTSmin多線程算法的改進(jìn),我們將其應(yīng)用到了我們算法上,主要改進(jìn)思路有以下兩點(diǎn):

如果有遷移S1→S2,如果Get_status(S2)返回UNKNOWN,我們?cè)黾右韵屡袛?

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

(2)如果S2是Dead狀態(tài)的子集,直接由引理1得,S2后繼肯定不會(huì)出現(xiàn)環(huán),可以直接跳過(guò).

基于這兩點(diǎn),我們對(duì)算法進(jìn)行了相應(yīng)的改動(dòng),改動(dòng)偽代碼如圖5,算法及優(yōu)化全部實(shí)現(xiàn)在CTAV工具中,我們對(duì)結(jié)果進(jìn)行了對(duì)比研究,主要基于展開(kāi)狀態(tài)的變化,如表1結(jié)果顯示,在部分模型取得了不錯(cuò)的效果.

3.3 算法效果比較

在多線程算法中,單一算法在發(fā)現(xiàn)環(huán)的過(guò)程中往往在某一方面表現(xiàn)十分優(yōu)秀,而在某些例子也存在極差的表現(xiàn),在工具實(shí)現(xiàn)過(guò)程中基于Tarjan、Dijkstra算法,我們比較了這兩種多核算法的區(qū)別,Tarjan算法主要表現(xiàn)在每發(fā)現(xiàn)環(huán)的時(shí)候只pop最后的邊,而Dijkstra算法在發(fā)現(xiàn)環(huán)的時(shí)候?qū)?dāng)前圖除根節(jié)點(diǎn)全部pop,這會(huì)直接導(dǎo)致發(fā)現(xiàn)接受圖的效率問(wèn)題,為此,我們采取了混合算法,讓一部分線程跑Tarjan,一部分線程跑Dijkstra,在實(shí)驗(yàn)中,我們通過(guò)給線程加上整數(shù)標(biāo)識(shí),讓奇數(shù)線程運(yùn)行Dijkstra算法,偶數(shù)線程運(yùn)行Tarjan算法.最終表現(xiàn)結(jié)果如表2,在結(jié)果中我們發(fā)現(xiàn)混合算法表現(xiàn)良好,在各種模型下能取得相對(duì)于單一算法更佳的時(shí)間效率效果.

圖5 算法改進(jìn)

表2 混合算法效果對(duì)比結(jié)果

4 實(shí)驗(yàn)研究

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

表3 多核CTAV對(duì)比單核表現(xiàn)結(jié)果

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

表4 divine和ctav對(duì)比

5 結(jié)束語(yǔ)

通過(guò)采用基于Tarjan和dijkstra的多線程并行的模型檢測(cè)算法,我們提高了CTAV工具對(duì)CPU的利用率,以此提高了CTAV工具的時(shí)間效率,同時(shí)通過(guò)符號(hào)化狀態(tài)的包含關(guān)系我們提出了多核算法下的優(yōu)化方案,對(duì)狀態(tài)空間的約減有一定的優(yōu)化作用,同時(shí)在CTAV工具下對(duì)比了多種多核空性檢測(cè)算法的效率,并采取混合多線程算法完成了工具的開(kāi)發(fā).當(dāng)然,多核模型檢測(cè)工具的優(yōu)化仍然需要進(jìn)一步的研究,簡(jiǎn)單的利用符號(hào)化狀態(tài)的包含關(guān)系約減的優(yōu)化效果并不明顯,進(jìn)一步的優(yōu)化也是我們下一步的工作.同時(shí),最新的研究中也產(chǎn)生了很多采取分布式資源對(duì)系統(tǒng)進(jìn)行模型檢測(cè)的研究,如文獻(xiàn)[19]提出采用分布式資源對(duì)發(fā)布訂閱結(jié)構(gòu)系統(tǒng)進(jìn)行模型檢測(cè).對(duì)于如何利用分布式系統(tǒng)進(jìn)一步提高工具的效率也是我們下一步的研究方向.