基于Büchi自動機化簡的JavaMOP監(jiān)控器構造方法

葉玲玲， 錢俊彥， 查顯偉

(桂林電子科技大學 計算機與信息安全學院，廣西 桂林 541004)

隨著軟件系統(tǒng)規(guī)模和復雜性的不斷增加，驗證軟件系統(tǒng)正確性和安全性的難度也越來越大。對于大規(guī)模的軟件系統(tǒng)，傳統(tǒng)的驗證技術(如模型驗證[1]和測試[2])會出現(xiàn)狀態(tài)爆炸和難以覆蓋系統(tǒng)所有執(zhí)行分支等問題。運行時驗證[3-4]是一種輕量級的形式化驗證方法，它根據(jù)軟件系統(tǒng)的實際執(zhí)行情況來驗證系統(tǒng)的正確性，能夠為人們提供系統(tǒng)運行時行為的準確信息。運行時驗證技術通過分析系統(tǒng)的一個或多個執(zhí)行軌跡來驗證系統(tǒng)，避免了傳統(tǒng)形式化驗證技術復雜性高的問題。運行時驗證的核心部分是監(jiān)控器[3]，對系統(tǒng)進行運行時驗證就是將待驗證的系統(tǒng)置于監(jiān)控下，監(jiān)控器通過驗證系統(tǒng)的執(zhí)行軌跡是否滿足給定的屬性來判斷系統(tǒng)是否正確。

近年來，為了確保軟件系統(tǒng)的正確性，運行時驗證得到了廣泛的應用。Asadollah等[5]在多核并行軟件環(huán)境下，提出了一種基于運行時驗證的漏洞檢測模型，用于檢測系統(tǒng)故障；Incki等[6]運用運行時驗證技術來防止物聯(lián)網中的網絡攻擊。然而，對系統(tǒng)進行運行時驗證，通常會產生一些額外的驗證開銷，因此，減少運行時驗證工具的監(jiān)控開銷成為了一個非常重要的研究內容。

為了減少運行時驗證的開銷，Reger等[7]提出MARQ驗證工具，通過索引技術和對監(jiān)控對象的冗余刪除來減少運行時開銷；Reger[8]運用靜態(tài)分析去除運行時驗證不可達對象，減少需檢測的對象，從而減少監(jiān)控開銷；Chen等[9]提出了弱監(jiān)控性的定義，排除不可監(jiān)控的屬性，以減少運行時監(jiān)控開銷。這些控制運行時驗證開銷的方法，主要考慮的是找到并刪除無用的監(jiān)控對象。為了達到減少運行時監(jiān)控開銷的目的，還可以對JavaMOP[10]、TraceMatches[11]等運行時驗證工具生成監(jiān)控器代碼的過程進行優(yōu)化，進而控制監(jiān)控器在構造過程中的開銷。鑒于此，提出一種基于Büchi自動機化簡的監(jiān)控器構造方法,降低JavaMOP運行時驗證的時間和內存開銷。

1 相關知識

1.1 線性時態(tài)邏輯

線性時態(tài)邏輯(linear temporal logic，簡稱LTL)是一種與時間有關的模態(tài)時序邏輯。引入LTL公式來描述系統(tǒng)行為屬性，通過使用原子命題、析取操作符(∨)、next算子(X)、until算子(U)和否定操作符號()定義LTL公式的集合。

定義2(LTL語義) 令u=u0u1…∈Σω是一個無限狀態(tài)序列，且Σ=2P，u滿足LTL公式φ，當且僅當uφ，LTL公式的語義定義為：

utrue；

up，當且僅當p∈u；

uφ，當且僅當u/φ；

uφ1∨φ2，當且僅當uφ1或者uφ2；

uφ1∧φ2，當且僅當uφ1且uφ2；

uXφ，當且僅當ui+1φ；

uφ1Uφ2，當且僅當?k≥0,ukuk+1…φ2和?0≤i

使用這些定義能夠推導出eventually算子(F)、always算子(G)和release算子(R)：Fφ等價于trueUφ；Gφ等價于Fφ；φ1Rφ2等價于(φ1Uφ2)。

1.2 Büchi自動機

Büchi自動機是ω自動機的一種，它將有限狀態(tài)自動機擴展到無限，接受一個無限的輸入序列，可以替代和處理ω正則語言。由于Büchi自動機在布爾操作[12]下是封閉的，它常被用于基于自動機的形式化驗證方法。

定義3(Büchi自動機) Büchi自動機是一個五元組B=(Σ,Q,I,δ,F)。其中：Σ為非空有限字母表，且Σ′?2Σ；δ?Q×2Σ′×Q是遷移關系；Q為非空有限狀態(tài)集合；I?Q為初始狀態(tài)集合；F?Q為接受狀態(tài)集合。

1.3JavaMOP

JavaMOP是一種基于Java語言、支持軟件開發(fā)與分析的運行時驗證工具，它支持多種邏輯，如線性時態(tài)邏輯(LTL)、上下無關文法(CFG)、擴展正則表達式(ERE)等，并將形式化規(guī)約以邏輯插件的形式集成在JavaMOP工具中，實現(xiàn)對不同形式化規(guī)約的監(jiān)控。其中，LTL插件用于驗證軟件系統(tǒng)運行時是否滿足給定的LTL屬性。JavaMOP是目前最高效的運行時驗證工具之一，在軟件運行時驗證中，將LTL語言描述的屬性轉換成監(jiān)控器代碼插裝到待監(jiān)控的系統(tǒng)程序中，實現(xiàn)實時監(jiān)控系統(tǒng)程序的運行并返回監(jiān)控結果。JavaMOP運行時監(jiān)控軟件系統(tǒng)程序的過程如圖1所示。

圖1 JavaMOP運行時監(jiān)控軟件系統(tǒng)程序的過程

JavaMOP在驗證軟件系統(tǒng)時，根據(jù)給定的屬性規(guī)約會自動生成相應的監(jiān)控器代碼，并插裝到目標程序中進行實時監(jiān)控。JavaMOP生成監(jiān)控器基于自動機的驗證算法，對于給定的LTL屬性，通過轉換算法[13]將LTL公式轉化為Büchi自動機，再將Büchi自動機轉化為確定性有限自動機(determine finite automata，簡稱DFA)，生成監(jiān)控器的抽象表示，之后得到監(jiān)控器代碼，實現(xiàn)對軟件系統(tǒng)程序驗證的功能。

2 自動機化簡規(guī)則與算法

在生成監(jiān)控器的過程中，減小Büchi自動機的大小，能夠減少內存消耗并加快監(jiān)控器代碼的生成。為此，提出自動機化簡規(guī)則對由LTL公式轉化得到的Büchi自動機進行化簡。首先對自動機中接受語言為空的狀態(tài)進行移除操作；再將滿足合并規(guī)則的狀態(tài)進行合并化簡，使得目標Büchi自動機最小化。

規(guī)則1(移除規(guī)則) 設Büchi自動機B=(Σ,Q,I,δ,F)，對自動機中的任一狀態(tài)q，若從狀態(tài)q開始的自動機接受語言為空，則狀態(tài)q為冗余狀態(tài)可移除。

規(guī)則1即取自動機中的任意一個狀態(tài)，判斷Büchi自動機接受的語言是否為空，若接受的語言為空，則進行冗余標記，并移除操作將其刪除。移除冗余算法描述如下。

算法1RemoveRedundant(B)

輸入：Büchi自動機B=(Σ,Q,I,δ,F)；

輸出：新的Büchi自動機B′=(Σ′,Q′,I′,δ′,F′)，且有L(B′)=L(B)。

1 fors∈Qdo；

2 計算從狀態(tài)s出發(fā)的后繼狀態(tài)集合nodes(s)；

3 if nodes(s)∩F=? then//狀態(tài)s開始的自動機語言為空；

4 標記狀態(tài)s為冗余狀態(tài)；

5 移除狀態(tài)s；

6 返回Büchi自動機B′。

規(guī)則2(合并規(guī)則) 設Büchi自動機中狀態(tài)a和狀態(tài)b都有n條遷移關系，若狀態(tài)a的下一個狀態(tài)是b,且狀態(tài)a遷移到狀態(tài)b的條件也是狀態(tài)b的自旋條件，同時狀態(tài)a剩下n-1條遷移與狀態(tài)b的另外n-1遷移相同，則狀態(tài)a和狀態(tài)b可以合并。

合并規(guī)則對自動機冗余刪除后進一步化簡自動機，用于得到狀態(tài)數(shù)更少的自動機。首先將自動機中的狀態(tài)集分為2個集合S1和S2，集合S1用于存儲接受狀態(tài)，集合S2存儲除了接受狀態(tài)的自動機狀態(tài)；然后分別對集合S1和集合S2中的狀態(tài)s和s′進行判斷，是否符合合并規(guī)則；若滿足，則可將狀態(tài)s′合并到狀態(tài)s，狀態(tài)s′的環(huán)移動到狀態(tài)s。具體執(zhí)行過程如下。

算法2Merge(B)

輸入：Büchi自動機B′=(Σ′,Q′,I′,δ′,F′)；

輸出：新的Büchi自動機B″=(Σ″,Q″,I″,δ″,F″)，且有L(B″)=L(B′)。

1 fors∈Qdo；

2 ifs∈Fthen；

3S1:=S1∪s//把s加入到接受狀態(tài)集合S1中；

4 else；

5S2:=S2∪s//把s加入到非接受狀態(tài)集合S2中；

6 //對S1集合中狀態(tài)進行合并操作；

7 fors∈S1do；

8 fors′∈S1do；

9 ifs,s′滿足合并規(guī)則 then；

10 合并狀態(tài)s和狀態(tài)s′；

11 //對S2集合中狀態(tài)進行合并操作；

12 fors∈S2do；

13 fors′∈S2do；

14 ifs，s′滿足合并規(guī)則then；

15 合并狀態(tài)s和狀態(tài)s′；

16 返回Büchi自動機B″。

圖2為運用合并規(guī)則化簡自動機狀態(tài)的例子。使用一個三元組δ表示2個狀態(tài)之間的遷移關系，如δ=(s1,c,s2)表示從狀態(tài)s1遷移到狀態(tài)s2的條件是c。圖2(a)為化簡之前的自動機，它有6個狀態(tài)和13條遷移關系，其中狀態(tài)s0有3條遷移關系δ1=(s0,a,s1)，δ2=(s0,c,s2)，δ3=(s0,b,s3)。狀態(tài)s1也有3條遷移關系δ4=(s1,a,s1)，δ5=(s1,c,s2)，δ6=(s1,b,s3)。狀態(tài)s0遷移到狀態(tài)s1與狀態(tài)s1到自身的條件相同，并且剩下的2條遷移也相同，因此，狀態(tài)s0和s1滿足合并規(guī)則，可將s0與s1合并。同樣地，狀態(tài)s3和s4滿足合并規(guī)則，可以合并?；喌玫叫碌淖詣訖C如圖2(b)所示，它包含4個狀態(tài)和7條遷移關系，與化簡前相比簡單了很多。

圖2 運用合并規(guī)則化簡自動機的例子

3 實驗與分析

為了驗證自動機化簡規(guī)則的可行性，用Java語言實現(xiàn)了基于自動機的監(jiān)控器構造過程，并與JavaMOP中原有構造運行時監(jiān)控器的方法進行比較。為了使2種監(jiān)控器構造方法的實驗數(shù)據(jù)具有可比性和公平性，采用相同的測試用例，所有實驗在相同的環(huán)境下進行。實驗運行環(huán)境的配置如下：處理器為Inter (R) Core (TM) i5-4690 CPU@3.5 GHz和內存為8 GiB的臺式電腦，電腦配備的操作系統(tǒng)為Ubuntu 14.04，同時配置了Sun Java SE 8環(huán)境。使用DaCapo[14]數(shù)據(jù)集，選取其中4個測試屬性作為實驗的測試對象，分別為：

HasNext：對于每個迭代器對象，要求在執(zhí)行函數(shù)next()前調用函數(shù)hasnext()，并且hasnext()的返回值為true；

SafeSyncColl：若一個集合是同步的，則它的迭代器也應是同步訪問的；

UnSafeIterator：在使用迭代器接口迭代集合元素時不能更新集合元素；

UnSafeMapIterator：在集合上對映射的鍵值迭代時，Map無法進行更新操作。

表1為2種監(jiān)控器構造方法的性能比較。從表1可看出，在內存開銷方面，化簡Büchi自動機能夠減少運行時監(jiān)控器在構造過程中的內存消耗；在時間開銷上，簡化的Büchi自動機加速了生成監(jiān)控器的過程，從而節(jié)省了構造監(jiān)控器代碼的時間，降低了整個監(jiān)控器構造的時間開銷。對于測試的屬性HasNext，化簡操作前JavaMop時間和內存開銷分別為92.88 s和629.71 MiB，本方法時間和內存開銷分別為89.92 s和612.23 MiB，在時間和內存開銷分別降低了3.19%和2.78%。對于屬性UnSafeIterator，本方法時間和內存開銷分別降低4.93%和5.32%，比屬性HasNext性能提升更多，這是因為屬性UnSafeIterator操作更加復雜，經過化簡操作后移除和約減的狀態(tài)和遷移關系更多，因此，性能提升也相對更多。

表1 2種監(jiān)控器構造方法的性能比較

4 結束語

對于運行時驗證中基于自動機理論構造監(jiān)控器的方法，通過化簡Büchi自動機來減小運行時驗證在監(jiān)控器構造過程中的時間和內存開銷，能夠提高監(jiān)控器生成的效率和運行時驗證的性能。針對運行時驗證工具JavaMOP中構造監(jiān)控器的方法進行研究實驗，實驗結果表明，本方法在提升運行時監(jiān)控性能上有一定的效果。今后研究監(jiān)控器代碼生成后對程序進行實時監(jiān)控過程中監(jiān)控算法的優(yōu)化，提高監(jiān)控算法效率，以進一步降低運行時驗證的時間和內存開銷。