實時模型檢測精確加速窗口的計算原理及算法

王國卿 莊 雷 和孟佯 宋 玉 馬 嶺

(鄭州大學信息工程學院 鄭州 450001)

實時模型檢測中，時間自動機可以為實時系統(tǒng)的時間行為進行建模[1].使用時鐘描述帶有時鐘約束的狀態(tài)遷移，為實時系統(tǒng)的模型檢測提供了理論基礎[2]，其廣泛應用于輪詢控制系統(tǒng)、鐵路互鎖系統(tǒng)等領域.基于時間自動機的模型檢測算法，由于引入了時鐘變量，控制程序和外界環(huán)境通常使用不同的時間度量，可達性分析算法會產生大量狀態(tài)片段[3-4]，導致狀態(tài)空間急劇增大，檢測時間大幅增長.

加速技術是一種約減方法，可以用來解決由時間度量不同造成的片段問題.文獻[5]將加速技術應用到線性目標檢測中，可以有效地提高檢測性能；文獻[6]以隱式Markov模型作為改進框架，對推理模型進行了加速；文獻[7]提出了一種新的計算最壞情況執(zhí)行時間(worst case execution time， WCET)的算法，以時間自動機為模型，使用抽象技術加速了WCET的分析效率；文獻[8]基于貝葉斯分類器確定了加速模型，通過分析異質群體的行為趨勢，表明加速技術在可靠性評估中能有效提高分析精度；文獻[9]介紹了大規(guī)模分布式環(huán)境中實現(xiàn)目標函數優(yōu)化的迭代機學習算法，通過平衡性能和效率，使加速效果顯著提高；文獻[10]利用2個可滿足性問題求解器驗證在線模型，加速模型檢測對復雜行為的處理.

在加速技術的基礎上，國內外研究人員設計了很多種優(yōu)化技術來約減可達性分析所需的存儲空間，以解決或者緩解狀態(tài)空間爆炸問題.文獻[11]對時間自動機的時鐘采用基于時鐘帶(zone)的抽象來區(qū)分最大上、下界，以獲得對可達性驗證的完整性.通過此類優(yōu)化算法，可以有效化簡差分矩陣，這將極大地增加實時模型檢測工具UPPAAL的可擴展性.文獻[12]也研究了時間自動機的可達性問題，通過構建時鐘帶抽象的搜索樹，來模擬自動機狀態(tài)空間上的底層關系.從有效性的角度考慮，該方法避免了最大上下界方法產生非凸集的潛在可能，使算法更加完備.文獻[11-12]采用了時鐘帶抽象來近似實際可達時鐘值，是一種粗粒度方法.時鐘帶抽象基于符號化方法，根據時間自動機的時鐘約束來設置最大上下界抽象的參數.這一類方法對解決可達性問題是健全和完備的，但由于高度的粗粒度抽象，使抽象模型對時間自動機的其他性質無法準確驗證.

對于通信協(xié)議驗證[13]、物聯(lián)網服務建模[14]等實際問題，精確加速技術是一種更為有效的方法.精確加速技術是一種細粒度的抽象方法，在考慮前向可達性分析的同時，能夠分析其他性質的變化及影響.文獻[3]利用UPPAAL驗證樂高機器人系統(tǒng)時，發(fā)現(xiàn)了片段問題并進行簡單描述，提出可進一步研究的設想；文獻[15]將近似技術運用到實時系統(tǒng)模型的安全性和連通性檢測中，可有效控制回路導致重復控制的情況；文獻[16]提出一種實時性質語言L?S來檢測可達性中的拒絕狀態(tài)，同時對模型檢測的安全性和邊界活性進行了約減.以上文獻所提到的問題和方法，促使精確加速的概念提出，為進一步深入研究提供了可能.

在實時模型檢測中精確加速方面的研究工作較有代表性的包括文獻[17-22].

文獻[17]介紹了一種對時間自動機子集的語法調整方法.通過向時間自動機添加1個附加環(huán)，能夠加速前向符號可達性分析，可有效解決片段問題，對樂高機器人系統(tǒng)出現(xiàn)的問題加速效果明顯.但該文獻對可加速環(huán)窗口的說明不夠深入，沒有說明窗口大小的計算和進一步約減的辦法.文獻[18]提出一種基于駐留環(huán)實現(xiàn)精確加速的方法，其入口邊界條件由可加速環(huán)窗口大小決定.由于駐留環(huán)的長度固定，其構造的自動機模型更簡單，能提高精確加速的速度并降低精確加速的時間和空間開銷.該文獻同樣對可加速環(huán)窗口的大小默認為已知，未提及其計算方法.文獻[19]通過分析加速過程中的主要參數，提出一種模型檢測精確加速的判斷方法，推導出了精確加速是否需要的判斷條件.該方法可在片段數量較少或片段不滿足一定條件時使用，避免添加的附加環(huán)降低驗證速度.以上工作依賴于特定條件，在實際的實時系統(tǒng)中使用較少，與壓縮可加速環(huán)規(guī)模相比存在一定不足，且對可加速環(huán)窗口的概念亦未明確.文獻[20]針對時間自動機規(guī)模較大的問題，在識別可加速環(huán)的方法中引入拓撲排序的思想，提出了一種識別時間自動機中可加速環(huán)的方法.通過簡化時間自動機的規(guī)模，提高了識別時間自動機中可加速環(huán)的效率.盡管該方法與本文類似，都對時間自動機的規(guī)模進行了簡化，但其簡化的是非可加速環(huán)部分，本文在此基礎上對可加速環(huán)進行了進一步約減.文獻[21]提出了一種利用模型檢測技術來提高資源利用率的開發(fā)方法，在設計開發(fā)階段，使用了精確加速技術，極大地改進了符號模型檢測處理調度系統(tǒng)的能力；文獻[22]針對網絡物理系統(tǒng)的可調度問題，借助精確加速技術來建模高級規(guī)范和驗證框架，從而將高級規(guī)范自動轉換為正式模型.文獻[21-22]主要將精確加速技術的思想應用于系統(tǒng)資源調度問題的建模，但并未對原有的精確加速理論進行完善.

精確加速的關鍵技術是可加速環(huán)窗口的計算，向時間自動機添加的附加環(huán)和駐留環(huán)的參數，都取決于可加速環(huán)窗口的大小.上述與精確加速相關的各文獻中，給出的實例較為簡單，其中可加速環(huán)窗口的計算均為人工推演所得，尚未見到有文獻提出窗口的計算方法，可加速環(huán)窗口的計算成為精確加速中亟待解決的問題.

本文系統(tǒng)地給出了可加速環(huán)窗口的定義，并結合實例對窗口計算原理進行分析，根據已有的識別時間自動機中可加速環(huán)的方法[20]，提出了一種精確加速中可加速環(huán)窗口的計算算法.算法根據窗口計算原理，獲取影響窗口大小的有效數據，并對其他無用數據和節(jié)點進行約減，壓縮了可加速環(huán)的規(guī)模，提高了計算效率，為精確加速技術的后續(xù)實現(xiàn)提供了支持，同時為研發(fā)精確加速自動檢測程序奠定了基礎.

1 基礎知識

1.1 時間自動機

為了更清晰地說明時間自動機的實值時鐘，首先定義包含所有時鐘變量的時鐘約束集T(C).假設時鐘變量集為C，時鐘約束τ的定義為

τc?n|τ1∧τ2,

其中c∈C，n∈N，?表示二元關系{<,≤,=,≥,>}中的一種.時鐘約束集T(C)是時鐘約束τ的集合.

時鐘解釋v是從C到R+∪{0}的1個映射，R+為正實數集，即為時鐘變量集C中的每個時鐘變量賦值.對于時鐘變量集C的子集X，X0表示X的所有時鐘變量c賦值為0(時鐘復位)，而對集合C-X的時鐘變量沒有影響.

定義1.時間自動機[23].時間自動機定義為1個六元組(C,L,l0,A,I,E).其中C是時鐘變量集，L是有窮的狀態(tài)位置集合，l0∈L是起始位置，A是有窮的動作事件集合，I是使每一個狀態(tài)位置l∈L都有1個時鐘約束的映射，E?L×A×T(C)×2C×L是邊界的規(guī)則轉換集合.1個規(guī)則轉換(l,a,τ,λ,l′)表示：當狀態(tài)位置l的時鐘滿足時鐘約束τ，則系統(tǒng)可以完成動作事件a從狀態(tài)位置l轉移到狀態(tài)位置l′，并完成λ中的全部時鐘復位.

圖1是時間自動機定義示例，時間自動機M表示對實時系統(tǒng)中控制程序和外部環(huán)境的簡易抽象建模.狀態(tài)位置l1，l2，l3組成的環(huán)表示對控制程序的建模，稱之為控制環(huán)，時鐘為x；對外部環(huán)境的建模由時鐘y所體現(xiàn)，每次轉換到狀態(tài)位置l2時檢驗y，若滿足y≥LARGE，則跳出控制環(huán).

Fig. 1 Timed automaton M圖1 時間自動機M

1.2 前向符號可達性分析

前向符號可達性分析算法是實時模型檢測工具UPPAAL的核心之一.模型檢測引擎運用on-the-fly算法策略，從起始位置開始進行前向搜索，判斷某個符號狀態(tài)空間是否可達.對于每一個尚未搜索的符號狀態(tài)，需要根據其時鐘和動作計算出后繼狀態(tài)，并與已搜索的符號狀態(tài)作比較.若已經出現(xiàn)，則舍棄；若沒有出現(xiàn)，則將該后繼狀態(tài)添加到已搜索的符號狀態(tài)列表中.

為了進一步說明前向符號可達性分析過程，以圖1時間自動機M為例，表1給出了時間自動機M從起始位置開始進行前向符號搜索，執(zhí)行1次控制環(huán)后得到的符號狀態(tài)，表格結果由UPPAAL模擬器得到.表1中，符號狀態(tài)6與符號狀態(tài)3雖然狀態(tài)位置都是l2，但是由于二者的時鐘帶不同，所以是兩種不同的符號狀態(tài)，需要進一步前向搜索符號狀態(tài)6.符號狀態(tài)5與符號狀態(tài)2亦同理.由此可知，每執(zhí)行一次控制環(huán)，總能得到新的符號狀態(tài).

Table 1 Symbolic States Result from Forward Symbolic Exploration by Timed Automaton M表1 時間自動機M前向符號搜索得到的符號狀態(tài)

由于閾值LARGE通常較大，而時鐘y的增長較為緩慢，當驗證l4的可達性時，時間自動機M需要執(zhí)行若干次控制環(huán)才能使時鐘y得到有效地增長，而執(zhí)行次數的多少取決于LARGE的值.LARGE值越大，執(zhí)行的次數越多.正是由于建模中出現(xiàn)的不同時鐘，時間自動機在符號模型檢測時，運用時鐘帶抽象技術[11-12]，狀態(tài)空間會出現(xiàn)大量不必要的時鐘帶片段，形成前向符號搜索片段問題.

1.3 可加速環(huán)

與數學中的環(huán)(ring)不同，時間自動機中的環(huán)(cycle)可以簡單理解成一組邊及其所經過位置的序列，而序列的起始和終結位置是同一位置.可加速環(huán)是一類定義較為嚴格的環(huán)，環(huán)中的時鐘約束(包括狀態(tài)位置的時鐘約束、邊界的時鐘約束和時鐘復位)只能包含1個時鐘.具體定義為:

定義2.可加速環(huán)[17].給定1個時間自動機M=(C,L,l0,A,I,E)，設Ecyc=(e0,e1,…,en-1)∈En且x∈C，則可加速環(huán)定義為二元組(Ecyc,x)，滿足的條件為：

1)Ecyc是1個環(huán)；

2) 對于Ecyc中出現(xiàn)的所有狀態(tài)位置l，其時鐘約束I(l)為空或者是{x≤c}的形式；

3) 設(l,a,τ,λ,l′)∈Ecyc，其邊界時鐘約束τ為空或者是{x≥c}的形式，時鐘復位λ為空或者只含有x；

4)x必須在Ecyc的重置位置src(e0)的全部入邊上復位.

這里的時鐘x命名為環(huán)時鐘，時鐘約束I(l)命名為位置不變式，時鐘約束τ命名為邊界約束.重置位置src(e0)表示可加速環(huán)外部時鐘的檢測位置，且該位置的出邊為e0；若環(huán)中某個狀態(tài)位置的入邊為ei，則該位置的出邊為ei+1，其中i∈[0,n-2].

圖1中時間自動機M的狀態(tài)位置l1，l2，l3組成的控制環(huán)就是1個可加速環(huán)，環(huán)時鐘為x，重置位置為l2.各個狀態(tài)位置的位置不變式及環(huán)內各條邊的邊界約束都滿足可加速環(huán)的時鐘約束形式，在l2的唯一入邊，環(huán)時鐘x復位為0.

2 可加速環(huán)窗口

每個可加速環(huán)都有1個窗口，它的含義是指自動機執(zhí)行1次可加速環(huán)，環(huán)內時鐘增加大小的區(qū)間.

1)D∈[a,b]；

2) 對任意實數d∈[a,b]，都可以在合法時鐘約束下調整TRACE(Ecyc)中的每個時延Dm，使D為d.

定義中總時延的含義，即為環(huán)內時鐘的增加量，可以根據定義理解為：時間自動機從重置位置開始，執(zhí)行1次可加速環(huán)回到重置位置時外部時鐘的增加量.窗口即環(huán)內時鐘增量區(qū)間.

定理1.設時間自動機M中的1個可加速環(huán)為(Ecyc,x)，環(huán)內各節(jié)點集合Lcyc={li|li=src(ei)且0≤i≤n-1}，li=src(ei)表示li節(jié)點位置是邊界ei的起始節(jié)點.對任意節(jié)點li，若外部時鐘為y，則第2次回到該節(jié)點時，時鐘帶y-x的增量區(qū)間[a′,b′]等于環(huán)內時鐘增量區(qū)間，而不必考慮是否已從重置位置進入了可加速環(huán).區(qū)間[a′,b′]是可加速環(huán)(Ecyc,x)的窗口.

若尚未從重置位置進入可加速環(huán)，根據對定義3的分析，外部時鐘y的增量區(qū)間與環(huán)內時鐘增量區(qū)間存在的偏差δ主要取決于進入可加速環(huán)前的時鐘數據.而由于沒有進入可加速環(huán)，環(huán)時鐘x和外部時鐘y是一樣自然增長的，均可看作全局時鐘，節(jié)點li的時鐘帶y-x可以完全去除偏差δ.偏差δ一旦去除，節(jié)點li就等同于提前進入可加速環(huán).以此為起點再回到這個節(jié)點時，時鐘帶y-x表示的就是外部時鐘在環(huán)內的凈增長，時鐘帶y-x的增量區(qū)間與環(huán)內時鐘增量區(qū)間等價，即為窗口.

綜合上述2種情況可知定理1成立.

證畢.

3 精確加速窗口的計算原理及算法

3.1 計算原理

根據可加速環(huán)的定義，窗口計算的是環(huán)內時鐘增量，需要觀察到達環(huán)內同一狀態(tài)位置執(zhí)行可加速環(huán)前后的時鐘變化.因此，可加速環(huán)窗口的計算可以從前向符號搜索得到的符號狀態(tài)入手.仍以圖1為例，根據時間自動機的語義，具體分析精確加速的計算原理，總結可加速環(huán)窗口的一般計算方法.

時間自動機M在起始位置l0時，環(huán)時鐘x和外部時鐘y初值為0；

M轉移到狀態(tài)位置l1，x至少增長到大于3才會轉移，而l1的位置不變式要求x≤5，因此到達l1時，3

M轉移到狀態(tài)位置l2，邊界約束為x≥3，同時x時鐘復位，l2的位置不變式為x≤2；到達l2時，x的變化范圍取決于時鐘復位和位置不變式，0≤x≤2；y的增長區(qū)間Δy取決于邊界約束和上一位置x的范圍以及位置不變式，邊界約束x≥3和上一位置3

M轉移到狀態(tài)位置l3，x時鐘復位，l3的位置不變式為x≤4，因此到達l3時，0≤x≤4；因為沒有邊界約束，而上一位置0≤x≤2，所以Δy≥0，由位置不變式知Δy≤4，又有上一位置3

M轉移到狀態(tài)位置l1，邊界約束為x≥1，l1的位置不變式為x≤5；到達l1時，因為沒有時鐘復位，此時x的變化范圍取決于邊界約束和位置不變式，1≤x≤5；對于y，邊界約束x≥1和上一位置0

M轉移到狀態(tài)位置l2，邊界約束為x≥3，同時x時鐘復位，l2的位置不變式為x≤2，到達l2時，0≤x≤2；邊界約束x≥3和上一位置1≤x≤5說明Δy≥2，位置不變式x≤2說明Δy≤2，故Δy=2，又有上一位置4

M再次執(zhí)行可加速環(huán)的分析過程與之前相類似，環(huán)時鐘x和外部時鐘y的變化主要取決于位置不變式、邊界約束、時鐘復位3個因素.對于環(huán)時鐘x，若存在時鐘復位，則x的變化范圍取決于時鐘復位和位置不變式，否則其變化范圍取決于邊界約束和位置不變式；對于外部時鐘y，主要考察Δy的變化范圍，其下界取決于邊界約束和上一位置x的范圍，其上界取決于位置不變式.經分析，可加速環(huán)內的x與Δy的取值范圍是始終不變的.總結上述分析過程，表2給出了時間自動機M執(zhí)行2次可加速環(huán)得到的符號狀態(tài).

Table 2 Symbolic States Result from Executing Acceleratable Cycle Twice by Timed Automaton M表2 時間自動機M執(zhí)行2次可加速環(huán)得到的符號狀態(tài)

通過對比表2和表1的數據發(fā)現(xiàn)，分析結果的前6個狀態(tài)與UPPAAL模擬器得到的結果是一致的，說明分析過程合乎規(guī)范.

根據可加速環(huán)窗口的定義，選取重置位置l2的2個符號狀態(tài)3，6的時鐘帶y計算窗口，從3

根據定理1，更快計算窗口的方法是選取符號狀態(tài)2、5，直接計算時鐘帶y-x的增量區(qū)間.從y-x=0到3

3.2 計算算法

根據對窗口計算原理的分析，窗口的計算取決于位置不變式、邊界約束、時鐘復位3個因素.為了使算法的描述更簡便，設cnL和cnE分別表示位置不變式和邊界約束中的常量，定義其自然數的提取規(guī)則為：

1) 當I(l)=?時，cnL(I(l))=∞；當I(l)={x≤c}時，cnL(I(l))=c；

2) 當τ=?時，cnE(τ)=0；當τ={x≥c}時，cnE(τ)=c.

文獻[20]給出了識別時間自動機中可加速環(huán)的方法，對圖1中的時間自動機M使用文獻給出的方法處理后，得到如圖2所示的可加速環(huán)(Ecyc,x).

Fig. 2 Acceleratable cycle (Ecyc,x)圖2 可加速環(huán)(Ecyc,x)

可加速環(huán)窗口的計算，可以選擇環(huán)中任意入邊有環(huán)時鐘復位的節(jié)點作為起始，結合可加速環(huán)的定義和精確加速的原理分析，對識別出的可加速環(huán)進行進一步精準壓縮，減少環(huán)中節(jié)點數量，提高計算速度.精確加速中可加速環(huán)窗口的計算算法為：

Step1. 對于時間自動機M，使用識別時間自動機可加速環(huán)算法[20]，輸出M中所有可加速環(huán).

Step2. 選取1個未處理的可加速環(huán)，選擇環(huán)中任意入邊有環(huán)時鐘復位的節(jié)點作為起始，檢測其出邊是否有環(huán)時鐘復位.若有則記錄這一節(jié)點，若無則不記錄，然后轉移到下一節(jié)點繼續(xù)檢測，直到回到起始節(jié)點.

Step3. 若記錄的節(jié)點個數與該可加速環(huán)節(jié)點個數相同，則可加速環(huán)無需壓縮，計算窗口使用原環(huán)，轉Step6，否則執(zhí)行Step4.

Step4. 將所記錄的節(jié)點按照記錄順序連接成1個新環(huán)，各節(jié)點的位置不變式與原環(huán)一致，新環(huán)所有邊均含有環(huán)時鐘復位，各邊邊界約束的計算執(zhí)行Step5.此時得到節(jié)點壓縮后的新可加速環(huán)，計算窗口使用新環(huán).

Step5. 求新環(huán)各邊的邊界約束.不妨設所求邊的起始節(jié)點為A，A在新環(huán)中其入邊的起始節(jié)點為B.首先在原環(huán)中找出一條從B到A的轉移路徑，然后計算出轉移路徑中除節(jié)點B以外各節(jié)點出邊cnE(τ)值較大的，其邊界約束作為所求邊的邊界約束.

Step6. 計算可加速環(huán)窗口[a,b].a為各邊cnE(τ)之和，b為各節(jié)點cnL(I(l))之和.

Step7. 若仍有未處理的可加速環(huán)，轉Step2，否則算法結束.

偽代碼表示為：

算法1.計算可加速環(huán)(Ecyc,x)的窗口[a,b].

輸入：可加速環(huán)(Ecyc,x)；

輸出：窗口邊界a和b.

Ecyc=(e0,e1,…,en-1)，且對于每一個ei有ei=(li,ai,τi,λi,li+1)；

① functionWindowComputation(Ecyc,x)

②reset←0;

③KEY[0,1,…,n]←0;

④ fori←0 ton-1 do

⑤ ifλi≠? then

⑥reset←reset+1;

⑦KEY[reset]←i;

⑧ end if

⑨ end for

⑩A[1,2,…,reset]←0;

若可加速環(huán)節(jié)點數量為n，則算法1的Step2～Step3的時間復雜度為O(n)，算法1的Step4～Step5的時間復雜度為O(n)，算法1的Step6的時間復雜度最差為O(n)；考慮到算法1的Step1調用文獻[20]識別時間自動機可加速環(huán)算法的時間復雜度為O(n2)，因此整個算法的時間復雜度為O(n2).

因為可加速環(huán)的定義要求時鐘x必須在重置位置的全部入邊上復位，所以至少有λn-1非空，reset至少為1，算法的后續(xù)計算依托于reset值；而可加速環(huán)的定義又嚴格要求了位置不變式、邊界約束、時鐘復位的出現(xiàn)形式，因此該算法必然有解.

定理2.設時間自動機M中的1個可加速環(huán)為(Ecyc,x)，環(huán)內各節(jié)點集合Lcyc={li|li=src(ei)且0≤i≤n-1}.采用可加速環(huán)節(jié)點壓縮算法生成的新可加速環(huán)，其可達性與原可加速環(huán)(Ecyc,x)等價.

證畢.

現(xiàn)利用所提出的算法計算圖2可加速環(huán)(Ecyc,x)的窗口[a,b]：

因為時鐘x在各邊上時鐘復位2次，所以reset=2，需要記錄的節(jié)點有l(wèi)1，l2，所構造的新環(huán)比原環(huán)減少1個節(jié)點；原環(huán)被分為2部分，一部分是l2及其出邊，剩余的是另一部分；新環(huán)各邊均包含時鐘x復位，邊界約束τ依次為空和x≥3(即A[1]=max{0}=0，A[2]=max{1,3}=3)，位置不變式I(l)依次為x≤2和x≤5(即B[1]=cnL(I(l2))=2，B[2]=cnL(I(l1))=5).此時，節(jié)點壓縮后的新可加速環(huán)構造完成，如圖3所示：

Fig. 3 New acceleratable cycle after node compression in Fig.2圖3 圖2中節(jié)點壓縮后的可加速環(huán)

計算a為各邊cnE(τ)之和，a=A[1]+A[2]=3；b為各節(jié)點cnL(I(l))之和，b=B[1]+B[2]=7.所以可加速環(huán)的窗口為[3,7]，與之前的分析結果一致.

4 實驗結果

通過與物聯(lián)網科研團隊的交流及合作，精確加速技術成功已應用于物聯(lián)網網關安全系統(tǒng)的建模及驗證中[24].圖4展示了物聯(lián)網網關安全系統(tǒng)的核心部分——輪詢模塊的時間自動機模型.對于輪詢模塊，通過同步通道開啟輪詢，并由類型狀態(tài)控制輪詢邏輯的終端是感知終端還是執(zhí)行終端，使用不同的流程進行處理.物聯(lián)網網關安全系統(tǒng)的核心技術是基于時間標簽的AES密碼算法[25]，通過在密鑰擴展階段引入時間標簽，使輪密鑰可隨時間的變化進行動態(tài)更新，進而實現(xiàn)密文的變化，有效地保證機密信息的安全性.由于引入了時間標簽，使得系統(tǒng)產生了可加速環(huán)，精確加速技術的應用可有效提升驗證效率.

Fig. 4 The polling module model of Internet of things gateway security system圖4 物聯(lián)網網關安全系統(tǒng)的輪詢模塊模型

對物聯(lián)網網關安全系統(tǒng)使用3.2節(jié)算法進行分析，首先識別出系統(tǒng)中若干個可加速環(huán)，以其中1個可加速環(huán)為例，如圖5所示：

Fig. 5 An acceleratable cycle in IoT gatewaysecurity system圖5 物聯(lián)網網關安全系統(tǒng)中識別出的1個可加速環(huán)

然后對可加速環(huán)進行處理，構造節(jié)點壓縮后的新環(huán)，所有邊均含有環(huán)時鐘復位.新環(huán)如圖6所示：

Fig. 6 New acceleratable cycle after node compression in Fig.5圖6 圖5中可加速環(huán)節(jié)點壓縮后得到的新環(huán)

最后進行可加速環(huán)窗口的計算，僅需遍歷各新環(huán)的位置不變式和邊界約束即可.計算cnE(τ)之和為窗口下限，計算cnL(I(l))之和為窗口上限，因此可加速環(huán)窗口為[6,10].結果經過UPPAAL模擬器驗證無誤.

對物聯(lián)網網關安全系統(tǒng)中的所有可加速環(huán)使用3.2節(jié)算法進行節(jié)點壓縮處理，再次驗證系統(tǒng)的機密性、可用性、真實性、頑健性、完整性、新鮮性等性質，實驗結果如表3所示:

Table 3 Experimental Results表3 實驗結果對比

Fig. 7 Timed automaton M′圖7 時間自動機M′

對于未處理系統(tǒng)，首先需要執(zhí)行節(jié)點壓縮算法，然后再驗證有關安全性質，執(zhí)行壓縮算法所需消耗的時空資源如表4所示:

Table 4 The TM Resources of Compressed Algorithm表4 執(zhí)行壓縮算法所需消耗的時空資源

Table 4 The TM Resources of Compressed Algorithm表4 執(zhí)行壓縮算法所需消耗的時空資源

Execution Time∕sMemory∕KB0.27721272

實驗結果表明，節(jié)點壓縮后的物聯(lián)網網關安全系統(tǒng)模型驗證時間(含節(jié)點壓縮算法時間)平均減少了8.04%，內存消耗(含節(jié)點壓縮算法內存)平均減少了26.87%，且精簡后的時間自動機模型沒有影響到相關性質的驗證.

此外，所提出的算法還可以快速檢索出模型中的死鎖問題，以圖7時間自動機M′為例.

對時間自動機M′使用3.2節(jié)的算法進行分析，首先可以識別出4個可加速環(huán)，如圖8所示.各個環(huán)中的位置不變式、邊界約束、時鐘復位均可為空.

Fig. 8 All acceleratable cycles identified in timed automaton M′圖8 時間自動機M′中識別出的所有可加速環(huán)

對每一個可加速環(huán)進行處理，構造節(jié)點壓縮后的新環(huán)，其嚴格滿足可加速環(huán)定義，且所有邊均含有環(huán)時鐘復位.4個可加速環(huán)壓縮后的新可加速環(huán)如圖9所示.

需要注意的是對于新可加速環(huán)3，l14→l13的遷移是無法執(zhí)行的.因為l14的位置不變式x≤7與邊界約束x≥8相互矛盾，此時環(huán)進入死鎖狀態(tài).還原到時間自動機M′中，死鎖狀態(tài)同樣存在.相比于原自動機模型，壓縮后的新環(huán)更容易發(fā)現(xiàn)死鎖狀態(tài)的存在.舍棄掉存在死鎖的可加速環(huán)，時間自動機M′實際只有3個可以執(zhí)行的可加速環(huán)(即可加速環(huán)1，2，4).

最后，可加速環(huán)窗口的計算，僅需遍歷各新環(huán)的位置不變式和邊界約束即可.計算cnE(τ)值之和為窗口下限，計算cnL(I(l))值之和為窗口上限.容易得到可加速環(huán)1，2，4的窗口分別為[7,18]，[6,16]，[13,24].經過UPPAAL模擬器的驗證可知，所得結果正確無誤.

通過該實例可知，包含節(jié)點狀態(tài)多的環(huán)，其窗口不一定比節(jié)點狀態(tài)少的環(huán)大，如可加速環(huán)1和2；只要1個環(huán)滿足可加速環(huán)定義，就可以進一步壓縮成1個所有邊均含有環(huán)時鐘復位的新可加速環(huán)，而不論其是否存在死鎖，如可加速環(huán)3；1個可加速環(huán)存在死鎖，并不能說明整個時間自動機進入死鎖，可能有其他路徑可以遷移，如可加速環(huán)3和4.

Fig. 9 New acceleratable cycles after node compression in timed automaton M′圖9 時間自動機M′中可加速環(huán)節(jié)點壓縮后得到的新可加速環(huán)

5 總結與展望

通過對精確加速技術核心——可加速環(huán)的分析，闡釋了其關鍵技術可加速環(huán)窗口計算的必要性，而目前均為人工推演，缺少嚴格的數學推導；運用識別時間自動機中可加速環(huán)的方法，提出了一種精確加速中可加速環(huán)窗口的計算方法，并結合具體實例進行了分析.主要工作有：

1) 提出一種精確加速窗口的計算方法，算法壓縮了可加速環(huán)的節(jié)點規(guī)模，使計算模型更為簡單，窗口的計算效率得到了提高，同時能夠發(fā)現(xiàn)模型死鎖等問題；

2) 結合物聯(lián)網網關安全系統(tǒng)模型等實例，從時空損耗的角度對系統(tǒng)的性質進行驗證，實驗結果表明了算法的高效性.

在對復雜實時系統(tǒng)進行建模時，可能會出現(xiàn)多個可加速環(huán)疊加在同一位置的情況.運用附加環(huán)技術進行精確加速，所添加的位置會由于可加速環(huán)數量的增加而成倍增長，進而導致內存不足無法進行模型檢測；運用駐留環(huán)技術進行精確加速，多個可加速環(huán)的疊加使得駐留環(huán)入口條件不統(tǒng)一，而對于某一個駐留環(huán)，仍需執(zhí)行其對應的可加速環(huán)a(b-a)次，多個可加速環(huán)窗口的差異會使時間消耗大幅增加.如何解決復雜實時模型中的精確加速，是下一步需要重點研究的工作.另外，利用算法壓縮可加速環(huán)節(jié)點的思想，嘗試將原自動機模型整體精簡，在保證其原有性質的同時快速檢測死鎖等問題；綜合應用窗口計算、添加附加環(huán)和駐留環(huán)等方法，并結合實際問題將動作遷移、緊急通道等其他條件考慮在內，嘗試搭建簡單的精確加速自動檢測平臺，也是下一步研究的主要工作.