， ，,2，

(1.鄭州大學(xué) 信息工程學(xué)院， 鄭州 450001; 2.吉首大學(xué) 數(shù)學(xué)與計算機科學(xué)學(xué)院，湖南 吉首 416000)

基于時間自動機的模型檢測是一種經(jīng)典的自動驗證技術(shù)，它具備成熟的理論基礎(chǔ)并廣泛應(yīng)用于安全認(rèn)證協(xié)議、控制系統(tǒng)等領(lǐng)域。在實時系統(tǒng)中，由于控制程序和外界環(huán)境經(jīng)常使用不同的時間度量，當(dāng)以時間自動機為基礎(chǔ)，運用符號模型檢測技術(shù)進行可達性分析與驗證時[1]，驗證速度會因為狀態(tài)空間的片段化問題明顯下降[2]，導(dǎo)致模型檢測時間和空間增加，甚至無法完成檢測。

加速技術(shù)主要用來解決由于時間度量不同造成的片段問題。文獻[3]結(jié)果表明加速技術(shù)應(yīng)用在合并擴展中可以提高分析的精確性；文獻[4]介紹了利用硬件設(shè)備實現(xiàn)模型檢測加速的方法；文獻[5]利用兩個SAT求解器作為驗證引擎，對在線模型檢測進行了加速；文獻[6]和[7]分別向可加速環(huán)添加了一個附加環(huán)和駐留環(huán)，構(gòu)造了加速自動機模型，從而實現(xiàn)了加速。這些方法在大多數(shù)情況下能夠有效加速前向符號可達性分析過程，而且不改變時間自動機原有的可達性。

上述加速方法對于時鐘帶片段數(shù)量非常多的系統(tǒng)模型具有很好的加速效果，而對于片段數(shù)量較少，或者片段之間的關(guān)系不滿足一定條件時，加速效果不明顯，甚至?xí)档万炞C速度。

本文對基于附加環(huán)的精確加速技術(shù)進行分析，用加速效益和加速代價來衡量附加環(huán)的加速效果。通過分析加速過程中的主要參數(shù)，推導(dǎo)出了附加環(huán)加速能否有效的判斷條件。

1 基本知識

1.1 時間自動機

定義1(時間自動機) 假設(shè)M=(Loc,l0,X,A,I,E)是一個六元組的時間自動機，其中Loc是有窮控制位置的集合；l0∈Loc是初始位置；X是時鐘集；A是有窮動作的集合，包括協(xié)同動作和內(nèi)部動作；Loc→Φ(X)是一個映射，I為每個控制位置分配一個不變式；E?Loc×A×Φ(X)×2X×Loc是有窮邊的集合。一條邊(l,a,φ,λ,l′)表示一個遷移。如果位置l的時鐘取值滿足時鐘約束φ，那么系統(tǒng)可以通過動作a從位置l遷移到另一個位置l′，同時把λ∈X中的所有時鐘復(fù)位。

圖1是由控制程序和外部環(huán)境組成的時間自動機的抽象模型，L3是模型的初始位置。由位置L0、L1、L2組成的控制環(huán)對控制程序進行循環(huán)執(zhí)行，z是外界環(huán)境時鐘。當(dāng)時間自動機處在控制環(huán)的位置L0時，就會檢查時鐘z是否滿足z≥LARGE，從而決定是否跳出控制環(huán)而到達位置L4。

圖1 時間自動機P的抽象模型

1.2 前向符號可達性分析及片段問題

實時模型檢測工具UPPAAL的模型檢測引擎從初始狀態(tài)開始[8-9]，對可達的符號狀態(tài)空間進行前向搜索，判斷某個給定的狀態(tài)是否可達。對每個還未被搜索的符號狀態(tài)，計算出它的后繼狀態(tài)(時延或動作引起的)，并且與已經(jīng)搜索過的狀態(tài)進行比較，如果某個后繼狀態(tài)已經(jīng)出現(xiàn)過，就忽略它。相反，如果一個后繼狀態(tài)沒有出現(xiàn)過，就把它保存到待檢測狀態(tài)列表，以便進一步搜索[10]。

為了說明前向符號搜索過程，考慮圖1中的時間自動機P,表1給出了從初始狀態(tài)開始，通過前向符號搜索執(zhí)行兩次控制環(huán)得到的符號狀態(tài)。當(dāng)搜索到第5個符號狀態(tài)時，其控制位置與第2個符號狀態(tài)的控制位置相同，但由于它的時鐘帶并不包含在第2個符號狀態(tài)的時鐘帶中，因此，根據(jù)模型檢測可達性分析算法，應(yīng)該對這個狀態(tài)進一步搜索。同樣，對于第8個符號狀態(tài)也應(yīng)該進一步搜索。

表1 前向符號狀態(tài)搜索中時間自動機P得到的部分符號狀態(tài)

圖2是在前向符號狀態(tài)搜索過程中時間自動機P在控制位置L0產(chǎn)生的時鐘帶，Di為第i次到達位置L0時的時鐘帶。可以看出在這個過程中出現(xiàn)了嚴(yán)重的片段問題，這是由于閾值LARGE較大，而時鐘z的增長又比較緩慢。為了判斷控制位置L4是否可達，時間自動機必須多次執(zhí)行L0、L1、L2組成的環(huán)，才能使時鐘z得到足夠的增長。由于模型中出現(xiàn)了不同的時間度量，時間自動機在前向符號搜索進行模型檢測時，狀態(tài)空間會分裂成大量的時鐘帶片段，導(dǎo)致片段問題。

圖2 時間自動機P在控制位置L0的時鐘帶

1.3 精確加速技術(shù)

研究工作者已經(jīng)提出了多種精確加速方法，包括基于附加環(huán)和基于駐留環(huán)的精確加速方法，其關(guān)鍵技術(shù)在于為時間自動機的可加速環(huán)添加一個附加環(huán)，構(gòu)造加速模型，從而實現(xiàn)加速[6]。這些方法不會改變時間自動機的可達性，可以有效加速前向搜索可達性分析，從而解決片段問題。

定義2(加速自動機) 假設(shè)M=(Loc,l0,X,A,I,E)是一個時間自動機，A(M,l,x,B)= (Loc∪{l′},l0,X,A,I′,E∪{e1,e2})(假設(shè)l′?Loc)是M的一個加速自動機，其中，l∈Loc；常量B∈N，B=[a/(b-a)]*a；x∈X且(Ec,x)是一個可加速環(huán)；[a,b]是加速窗口；z是可加速環(huán)以外的時鐘；I′=I∪{(l′,true)}；e1=(l,τ,x≥0,{x},l′)；e2=(l′,τ,z≥B,{x},l)。

根據(jù)可加速環(huán)的定義可知，圖1中時間自動機P的控制環(huán)是一個可加速環(huán)，可以計算出它的加速窗口是[4,6]。根據(jù)定義2向時間自動機P添加一個駐留環(huán)，構(gòu)造基于駐留環(huán)的加速自動機PA，其中x=y，可以計算出B=8。與圖1相比，在圖3中僅添加一個新位置L5。

圖3 時間自動機P的加速自動機PA

2 有效精確加速的判斷條件

2.1 關(guān)鍵參數(shù)

在精確加速技術(shù)中，有幾個關(guān)鍵的參數(shù)：加速窗口[a,b]、實際加速點B和閾值LARGE。

(1) 加速窗口[a,b]

每個可加速環(huán)都有一個加速窗口，它是指執(zhí)行一次可加速環(huán)時鐘值增加大小的區(qū)間，可以根據(jù)時間自動機的語法計算出來。只要窗口上界a嚴(yán)格小于窗口下界b，可加速環(huán)就會產(chǎn)生連續(xù)的時鐘帶[7]。圖2中可加速環(huán)的加速窗口是[4, 6]，并且在z=8之后時鐘帶開始連續(xù)。

(2) 實際加速點B

根據(jù)文獻[11]，精確加速的實際加速位置(圖2中的B點)是由加速窗口決定的，其值為[a/(b-a)]*a。圖2中的時鐘帶在z=8時開始連續(xù)，也就是說實際加速點B=8。

(3) 閾值LARGE

閾值LARGE是一個常數(shù)，通常把它作為跳出控制環(huán)的條件。正是因為LARGE的存在，使得模型中出現(xiàn)了不同的時間度量，導(dǎo)致可達性分析算法對控制環(huán)進行多次重復(fù)搜索。對于可加速環(huán)，若LARGE足夠大(105以上)，則附加環(huán)有明顯的加速效果。下文中將LARGE簡記為L。

2.2 加速效果及加速代價分析

附加環(huán)的加速效益用加速效果和加速代價兩個標(biāo)準(zhǔn)來衡量。

定義3(加速量及加速效果) 在一個含有可加速環(huán)的時間自動機中，[a,b]是加速窗口。添加附加環(huán)之前，為了達到閾值LARGE，可加速環(huán)需要運行m1次，m1是滿足不等式n0+m1*a≥LARGE的最小值，其中，n0是環(huán)境時鐘z執(zhí)行可加速環(huán)之前的最大值。添加附加環(huán)之后，在滿足附加環(huán)的入邊條件之前，需要運行可加速環(huán)m2次，m2是滿足不等式m2*a≥B的最小值。

加速量是指添加附加環(huán)之后減少的可加速環(huán)運行次數(shù)，用Nacc表示，其值為m1-m2。加速效果是指添加附加環(huán)之后節(jié)省的運行時間，也就是運行Nacc次可加速環(huán)需要的時間，用T+表示。

定理1 假設(shè)M是一個時間自動機，Ec是M的一個可加速環(huán)，加速窗口是[a,b]且a

證明 根據(jù)定義3，由不等式n0+m1*a≥LARGE可得，m1=[(L-n0)/a]=(L-n0)/a+γ1，其中0≤γ1<1。由不等式m2*a≥B可得，m2=[B/a]=B/a+γ2，其中0≤γ1<1。因此，m1-m2=(L-n0-B)/a+γ1-γ2。由0≤γ1、γ2<1可知，-1<γ1-γ2<1。由此可得，加速量Nacc=m1-m2存在最小值Nacc=(L-n0-B)/a-1。

推論1 假設(shè)M是一個時間自動機，存在窗口為[a,b]的可加速環(huán)，且a

加速量和加速效果說明精確加速技術(shù)能夠減少可加速環(huán)的運行次數(shù)，節(jié)省可達性分析的時間，但是由于引入了附加環(huán)，可達性分析算法在每次運行到加速位置時都要對附加環(huán)的入邊條件進行判斷，直到條件滿足，即到達實際加速點B，這一過程增加了運算量和運行時間。

定義4(加速代價) 假設(shè)M是一個時間自動機，Ec是M中的一個可加速環(huán)，加速窗口是[a,b]且a

2.3 有效加速的判斷條件

利用上述定義和定理，分析精確加速技術(shù)有效加速的條件。用符號t表示搜索一個節(jié)點所需的時間，即單位時間，len表示可加速環(huán)的長度，即控制位置的個數(shù)。則加速效果T+的計算公式為：

T+=Nacc*t*len

(1)

根據(jù)加速代價的定義，在到達實際加速點之前，可達性分析算法在每次到達加速位置時都要判斷附加環(huán)的入邊條件是否成立，而這個判斷時間就是單位處理時間t，根據(jù)定義4可知判斷入邊條件的次數(shù)為m2，則加速代價T-的計算公式為：

T-=m2·t

(2)

定理2 假設(shè)M是一個時間自動機，Ec是一個可加速環(huán)，加速窗口是[a,b]且a

證明 附加環(huán)能夠有效加速前向可達性分析的條件是加速效果遠(yuǎn)遠(yuǎn)大于加速代價，也就是：T+>>T-，即Nacc*t*len>>m2*t，也即Nacc*len>>m2(t>0)。把Nacc和m2的值代入上式得

[(L-n0-B)/a-1]*len>>B/a+γ2

由于(L-B)/a-1>(L-n0-B)/a-1，B/a+γ2>B/a，所以[(L-B)/a-1]*len>>B/a，即：

B<

至此，得出了精確加速是否有效的判斷條件：

B<

從這個判斷條件可以看出，當(dāng)可加速環(huán)的長度和加速窗口一定時，如果LARGE的值足夠大，精確加速的效益就很明顯。根據(jù)定理2，在識別出可加速環(huán)后，首先判斷可加速環(huán)是否滿足有效加速的條件，若不滿足條件，則說明加速效果不理想，不用添加附加環(huán)；若滿足條件，則說明可加速環(huán)能夠進行有效加速，可以添加附加環(huán)。

2.4 實例驗證

對圖1中的時間自動機P進行分析，這里設(shè)定LARGE的值為300 000。

由位置L0、L1、L2組成的可加速環(huán)窗口為[4, 6]，B=8，len*(L-a)/(len+1)≈225 000，可以看出B<

對圖4中的時間自動機P進行分析。LARGE值仍為300 000，由L0、L1、L2組成的可加速環(huán)窗口為[6 000,7 100]，B=[a/(b-a)]*a=36 000，len*(L-a)/(len+1)=3*(300 000-6 000)/(3+1)=220 500，可以看出B并不是遠(yuǎn)遠(yuǎn)小于len*(L-a)/(len+1)，因此加速條件不成立。根據(jù)定理2可以判斷時間自動機P添加附加環(huán)之后加速效果不明顯，無需構(gòu)造加速模型。

圖4 時間自動機P

利用模型驗證工具UPPAAL，分別對時間自動機P和P′的可達性質(zhì)E<>P.L4和E<>P.L4進行驗證，表2給出了這兩個自動機添加附加環(huán)前后所消耗的時間和空間對比。從表中數(shù)據(jù)可以看出，時間自動機P在添加附加環(huán)之后加速效益明顯，但降低了驗證速度。這個結(jié)果與定理2中的判斷條件分析結(jié)果一致。

表2 驗證可達性運行時的數(shù)據(jù)

3 結(jié) 語

本文通過對精確加速技術(shù)進行分析，利用加速效果和加速代價衡量附加環(huán)的加速效益，推導(dǎo)出了精確加速技術(shù)能夠有效加速可達性分析的條件，根據(jù)這個加速條件可以判斷是否有必要添加附加環(huán)。下一步的工作是對可達性分析算法進行改進以取得更好的加速效果，并對自動添加附加環(huán)構(gòu)造加速模型進一步研究。

參考文獻:

[1] Bouyer P, Markey N, Sankur O.Automata, Languages, and Programming [M].Berlin: Springer Berlin Heidelberg, 2012: 128-140.

[2] Pelánek R.Reduction and Abstraction Techniques for Model Checking [D].Brno：Masaryk University, 2006.

[3] Leroux J, Sutre G.Accelerated Data-flow Analysis[C]//Static Analysis.Belin: Springer Berlin Heidelberg, 2007: 184-199.

[4] Barnat J, Bauch P, Brim L, et al.Employing Multiple CUDA Devices to Accelerate LTL Model Checking [C]//2010 IEEE 16th International Conference on Parallel and Distributed Systems (ICPADS).Berlin: IEEE, 2010: 259-266.

[5] Qanadilo M, Samara S, Zhao Y.Accelerating Online Model Checking [C]//2013 Sixth Latin-American Symposium on Dependable Computing (LADC).Berlin: IEEE, 2013: 40-47.

[6] 尹傳龍, 宋偉, 莊雷.識別時間自動機中可加速環(huán)的方法[J].計算機工程與設(shè)計, 2010, 31(23): 181-183.

[7] 尹傳龍, 莊雷, 王從銀.實時模型檢測中基于駐留環(huán)的精確加速[J].電子學(xué)報, 2011, 39(3): 489-493.

[8] Cicirelli F, Furfaro A, Nigro L.Model Checking Time-dependent System Specifications Using Time Stream Petri Nets and UPPAAL [J].Applied Mathematics and Computation, 2012, 218(16): 8160-8186.

[9] Fehnker A, Van Glabbeek R, H?fner P, et al.Automated Analysis of AODV Using UPPAAL[C]//Tools and

Algorithms for the Construction and Analysis of Systems.Berlin: Springer Berlin Heidelberg, 2012: 173-187.

[10] 張松年, 莊雷, 杜娟.時間自動機可達性分析算法的改進[J].計算機工程與科學(xué), 2007, 29(10): 44-46.

[11] Hendriks M, Larsen K G.Exact Acceleration of Real Time Model Checking [J].Electronic Notes in Theoretical Computer Science, 2002, 65(6): 120-139.