劉彥斌,葉 飛，王毅剛

(1.中國電子科技集團公司第十三研究所，石家莊 050051；

2.中國人民解放軍軍械工程學院，石家莊 050003)

?

【信息科學與控制工程】

軟件運行時驗證加速中的多目標約束模型研究

劉彥斌1,葉 飛2，王毅剛2

(1.中國電子科技集團公司第十三研究所，石家莊 050051；

2.中國人民解放軍軍械工程學院，石家莊 050003)

由于復雜性質的運行時驗證中常產生高額時間開銷，影響了該技術在系統(tǒng)部署后的應用；減小驗證開銷提高驗證效率已成為亟待解決的難點問題；通過識別運行時驗證優(yōu)化過程中多目標約束間的內在依賴關系，定義并構建了可加速監(jiān)控器的判定方程，作為驗證加速中的多目標約束模型；實驗表明：該模型的求解結果能夠用來判定可加速監(jiān)控器，為實施軟件運行時驗證加速提供量化依據(jù)。

運行時驗證；多目標約束；監(jiān)控器；監(jiān)控開銷；運行時監(jiān)控

運行時驗證(Runtime Verification)是一種近10多年來逐步興起的針對程序具體運行的輕量級驗證技術[1]。它把形式化驗證技術和系統(tǒng)的實際運行結合起來，通過監(jiān)控程序運行并檢驗其是否滿足給定性質實現(xiàn)對系統(tǒng)的驗證。由于運行時驗證針對的對象僅僅是系統(tǒng)運行中的單個或者少數(shù)執(zhí)行軌跡，不需針對整個系統(tǒng)模型，避免了狀態(tài)空間爆炸。但是，參數(shù)化性質等較為復雜性質的在線運行時驗證中，由于需要維持大量的監(jiān)控器實例并處理程序實體中生成的大量事件，經常產生高額的時間開銷。研究表明：當前具有代表性的運行時驗證工具JavaMOP[2]和Tracematches[3]所產生的平均開銷分別為41%和112%，如此高的開銷，是用戶所不能容忍的。開銷問題阻礙了運行時驗證技術在實踐中廣泛用于軟件部署后環(huán)境。減小軟件運行時驗證開銷，已成為當前亟待解決的難點問題。

由于性質驗證和診斷所需信息源可能部分重疊，在開銷優(yōu)化過程中不僅影響系統(tǒng)驗證結果的準確性，而且可能影響診斷所需信息的收集，即對診斷支持能力造成潛在不良影響。因此，把軟件運行時驗證加速歸結為多目標優(yōu)化問題，不僅需要將開銷做為優(yōu)化目標，還需考慮開銷優(yōu)化對驗證結果準確性以及診斷支持能力的影響。軟件運行時驗證加速過程需要在減小監(jiān)控開銷、提高驗證精度和改善診斷支持能力多個互相制約的目標間進行權衡。建立多目標約束模型，并基于該模型確定優(yōu)化對象，是實施軟件運行時驗證加速首先需要解決的問題。

本文通過識別運行時驗證優(yōu)化過程中多目標約束間的內在依賴關系，通過量化分析運行時驗證加速中的多目標約束，包括性質違背檢測能力、監(jiān)控開銷評估、診斷支持能力以及監(jiān)控器優(yōu)化的正確性，在此基礎上構建了可加速監(jiān)控器的判定方程，作為運行時驗證加速的多目標約束模型。該多目標約束模型的求解結果可判定“可加速”的監(jiān)控器，為實施軟件運行時驗證加速提供依據(jù)。

1 研究現(xiàn)狀

當前針對軟件運行時驗證加速的研究主要包括以下幾類：

1) 聯(lián)合靜態(tài)分析減小開銷。Bodden等[4]探索了許多輕量級的代碼靜態(tài)分析方法，通過識別可安全移除的插樁點減小開銷。Purandare 等[5]優(yōu)化了程序中性質相關的循環(huán)結構，通過僅僅監(jiān)控有限次數(shù)的循環(huán)減小開銷。

2) 基于周期性取樣的開銷優(yōu)化方法。Bonakdarpour等[6]提出了時間觸發(fā)的運行時驗證概念，監(jiān)控器周期性地程序狀態(tài)取樣來評估性質是否成立。Navabpour等[7]研究了采用啟發(fā)式算法求解給定取樣周期內需要被緩沖的最小數(shù)量的關鍵事件，以便時間-觸發(fā)的監(jiān)控器能夠成功重構兩個連續(xù)取樣時間內的程序狀態(tài)[8]，優(yōu)化取樣周期最小化所需外存儲器，以便監(jiān)控器能夠正確地恢復程序狀態(tài)變化序列。

3) 基于控制理論的解決方案[9]。針對CPS系統(tǒng)，提出新的基于控制理論的軟件監(jiān)控解決方案來協(xié)調可預測性以及內存利用率。

4) 基于并行運行監(jiān)控器減小開銷[10]。例如，通過在GPU中運行監(jiān)控器實現(xiàn)監(jiān)控和功能進程的分離，并行監(jiān)控并驗證程序。針對基于的系統(tǒng)，通過將不同組件運行在不同的計算機核中，減小運行時驗證開銷[11]。

但上述研究單純考慮如何減小運行時驗證開銷，沒有把軟件運行時驗證加速歸結為多目標優(yōu)化問題。

2 多目標決策基本原理

多目標決策與單目標決策不同，其最顯著特點是目標之間的不可公度性和目標產生的矛盾性。因此，單目標決策問題具有最優(yōu)解，多目標決策問題通常無法找到最優(yōu)解。多目標決策中，一般不存在所有目標函數(shù)共同的極大值點，通常求取其非劣解或最優(yōu)解[12]。多目標決策的標準形式是:

(VOP) max[f1(x),f2(x),…,fp(x)]

s.t.x∈X

其中，X=(x1,x2,…xn)T是n維向量，x所在的空間叫決策空間；f1(x),f2(x),…,fn(x)為目標函數(shù)，p維向量(f1(x),f2(x),…,fp(x))所在空間稱為目標空間；X是決策空間上的可行集。多目標決策過程就是求解得到近似的非劣解集的過程。

本文將監(jiān)控器標識為m，所對應的監(jiān)控器集合m=(m1,m2,…,mn)T是N維向量,m所在的空間是決策空間。m對應的目標函數(shù)分別標識為f1(m)，f2(m)和f3(m)，其中：f1(m)為性質違背檢測能力評估函數(shù);f2(m)為監(jiān)控開銷量化評估函數(shù);f3(m)為診斷支持能力評估函數(shù)。

三維向量(f1(m)，f2(m)和f3(m))所在空間是目標空間。針對具體的軟件系統(tǒng)，需要在多目標約束下求解得到決策空間上的最優(yōu)解M，將M中的監(jiān)控器轉換插入目標軟件，對其進行運行時監(jiān)控。

3 多目標約束分析

3.1 性質違背檢測能力

從運行時驗證角度而言，并非程序執(zhí)行中所有的性質都能夠被監(jiān)測。LamportL最早將反應式系統(tǒng)的性質分為安全性和活性兩大類[13]，簡單而言，安全性意味著“一些壞的事情在程序執(zhí)行期間從來不會發(fā)生”，而活性意味著“一些好的事情將最終發(fā)生”。

由于運行監(jiān)測器僅僅能夠觀察有限的執(zhí)行步驟，而活性需要通過無限序列行為決定，通常是不可監(jiān)測的。對于反應式系統(tǒng)而言，只有把活性轉換成有限時間區(qū)間的行為(如系統(tǒng)必須在固定的時間限制內響應請求)才能進行監(jiān)測，而安全性質一般是可以監(jiān)測的。但是，安全性質未必都是可監(jiān)測的性質(如圖靈機停機問題的安全關閉，是安全性質，但由于不可判定，從而是不可監(jiān)測的性質)。因此，可以得出結論，可監(jiān)測的性質是安全性質的真子集[14]。

對于σ∈Sw，用pref(σ)作為σ的所有有限前綴的集合，則可監(jiān)測的性質可以定義如下：

由于監(jiān)測器能夠監(jiān)測的僅僅是安全性質的子集，因此只有那些能夠被監(jiān)測器在有限軌跡內識別的性質才能作為監(jiān)測需求規(guī)約。同時，在可監(jiān)測的性質當中，并非所有性質都是需要進行監(jiān)測的。為減少監(jiān)測對系統(tǒng)帶來的額外開銷，如占用系統(tǒng)資源，影響軟件執(zhí)行時間等，應盡可能減少被監(jiān)測的性質數(shù)量。

3.2 監(jiān)控開銷評估

本文中的開銷是指時間開銷，是對在運行時驗證中由于監(jiān)控程序需要額外執(zhí)行的時間的度量。如果最初程序執(zhí)行時間為R，插樁后伴有監(jiān)控的程序執(zhí)行時間為R+K，則監(jiān)控開銷是K/R。

監(jiān)控開銷量化評估函數(shù)f2(m)=K/R,其中，K=y(x1,x2,…,xK),K的大小和多個因素相關，是被監(jiān)控變量的數(shù)量、位置、監(jiān)控需求描述語言、驗證算法等因素的函數(shù)。通過盡可能減小被監(jiān)測的性質及變量的數(shù)量，并對監(jiān)控需求描述語言中邏輯算子的形式和數(shù)量進行限制等途徑，可以減小監(jiān)控開銷。

首先，為減少被監(jiān)控變量的數(shù)量，選取監(jiān)測需求規(guī)約，需要遵循以下原則：選取“可監(jiān)測的”性質；選取那些“可疑的”無法通過常規(guī)軟件測試進行確認的性質進行監(jiān)測；根據(jù)失效引起的危害程度，優(yōu)先選取“嚴酷度”高的性質進行監(jiān)測；根據(jù)目標軟件特點及對開銷的容忍程度，選取被監(jiān)測的性質數(shù)目。

其次，一般說來，采用過去時間LTL或者MTL書寫的公式比采用將來時間的公式更容易表達安全性需求。由于這些公式僅僅涉及過去，它們的值在軌跡中的任何狀態(tài)中通?；蛘邽門rue或者為False，而不像將來時間公式那樣，需要在“未來”進行判定。從而這些過去時間書寫的性質規(guī)約更適于基于邏輯的監(jiān)測。因此，在監(jiān)測需求規(guī)約生成中盡可能采用過去時間算子進行性質表達。

第三，由于在監(jiān)測中，每個算子都將占用額外的內存，為了盡可能縮小監(jiān)測開銷，需要簡化給定邏輯中算子的數(shù)量。利用算子之間的等價關系，可以對算子進行簡化。例如，對于過去時間LTL，采用監(jiān)測算子{↑,↓,[ )s}可表達所有的標準過去時間LTL算子φ|◆φ|φ|φSsψ|φSwψ。從而，可把采用標準過去算子生成的公式轉化為采用監(jiān)測算子{↑,↓,[ )s}表示的性質規(guī)約，減小驗證開銷。

3.3 監(jiān)控器優(yōu)化的正確性

程序可看作由許多在不同的狀態(tài)下具有不同取值的程序變量組成，所有程序變量的某一次取值稱之為系統(tǒng)的一個狀態(tài)，從而，一個典型的程序執(zhí)行模型可看作是一個又一個狀態(tài)所組成的序列：

定義2：執(zhí)行：程序執(zhí)行是一個無限狀態(tài)序列σ=s0,s1, …，si∈S，S是狀態(tài)的集合；程序執(zhí)行軌跡π[i，j]表示π從狀態(tài)si到狀態(tài)sj的子序列si,si+1,…,sj。

軟件行為是執(zhí)行的集合，軟件性質(Property)是期望的軟件行為的描述，即執(zhí)行中那些(無限)狀態(tài)序列所滿足的性質。性質反映了狀態(tài)內部和狀態(tài)之間的關系，回答了狀態(tài)的什么關系導致軟件可接受的外部行為(即軟件需求)的問題。

定義3：監(jiān)控器優(yōu)化的正確性：對于性質?和未優(yōu)化的監(jiān)控器M，符合下列條件時稱M被正確優(yōu)化：對于每個軌跡π，監(jiān)控器M觀察得到π′，且|π′|≤|π|；M觀察到π發(fā)生性質違背時，M′都能報告π′發(fā)生性質違背。

3.4 診斷支持能力

根據(jù)GJB3385—98，術語“診斷”是指檢測故障和隔離故障的過程。它的實質是從征兆出發(fā)，通過信息的處理，正確地確定故障原因、類型和位置。由于軟件故障具有隨機性，軟件故障狀態(tài)隨著程序執(zhí)行的結束而消失并且難以進行重現(xiàn)，等到系統(tǒng)失效發(fā)生后，再去進行故障診斷常?！盀闀r已晚”，常常很難斷定失效究竟是軟件故障還是硬件故障，從而需要根據(jù)故障監(jiān)測信息進行故障診斷。同時，為減小軟件運行監(jiān)測給系統(tǒng)帶來的開銷，監(jiān)測能夠從軟件運行中提取的信息需盡可能的少。也就是說，軟件運行監(jiān)測必須“精確”地捕獲能夠作為征兆的故障信息。

由于部署后應用系統(tǒng)中的軟件一般經過了大量的軟件測試，包括靜態(tài)測試、動態(tài)測試等。殘留的軟件故障最可能的是邏輯和時序約束方面的故障以及和硬件接口的輸入/輸出故障，因為這些故障和真實運行環(huán)境有關，只有在某些特殊情況下才可能出現(xiàn)，常規(guī)的軟件測試難以發(fā)現(xiàn)。因此，需要對這些方面的特性進行監(jiān)測，主要包括功能特性、時序性質以及時間約束。主要采用LTL和MTL，根據(jù)這幾方面特性，提取監(jiān)測需求公式；并在系統(tǒng)運行期間運行驗證這些公式是否發(fā)生性質違背，發(fā)生性質違背時的故障體現(xiàn)為上述3個方面，發(fā)現(xiàn)性質違背時能夠用來揭示故障原因的軟件運行狀態(tài)被稱作診斷信息D。

定義4：監(jiān)控器優(yōu)化中的診斷信息保持：對于性質?，未優(yōu)化的監(jiān)控器M，M觀察到的軌跡為π，診斷信息為D；對于優(yōu)化過的監(jiān)控器M′，如果監(jiān)控器M′觀察得到的每個軌跡π′，都滿足D∩π=D∩π′，則稱優(yōu)化后的監(jiān)控器保持了診斷信息,此時診斷支持能力評估函數(shù)f3(M)=f3(M′)。

4 多目標約束模型的構建

在實施運行時驗證加速之前，需要首先判定出哪些監(jiān)控器是“可加速”的，即判定出哪些監(jiān)控器在運行中不再必要、哪些可以進行動態(tài)調整，且滿足多目標約束。因此，需要構建可加速監(jiān)控器的判定方程。

定義5：單個可加速監(jiān)控器：對于某監(jiān)控器m而言,如存在對其優(yōu)化后的監(jiān)控器m′，滿足下列條件：性質違背檢測能力評估函數(shù)f1(m)=f1(m′)，監(jiān)控開銷量化評估函數(shù)f2(m)>f2(m′),診斷支持能力評估函數(shù)f3(m)=f3(m′)，則稱m為可加速監(jiān)控器m，加速后的監(jiān)控器為m′。

定義6：可加速監(jiān)控器組：對于監(jiān)控器M=(m1,m2,…,mn)，如果M中存在監(jiān)控器組L=(mi,mj,…,mk)，使得對L優(yōu)化后的監(jiān)控器，滿足下列條件：性質違背檢測能力評估函數(shù)f1(L)≤f1(L′)，監(jiān)控開銷量化評估函數(shù)f2(L)>f2(L′)，診斷支持能力評估函數(shù)f3(L)≤f3(L′)，則稱L為可加速監(jiān)控器組。

本項目所說的可加速監(jiān)控器既包括單個可加速監(jiān)控器，也包括可加速監(jiān)控器組，是對兩者的統(tǒng)稱。軟件運行時驗證加速過程需要在減小監(jiān)控開銷、提高驗證精度和改善診斷支持能力多個互相制約的目標間進行權衡，對可加速監(jiān)控器的判定過程定義如下。

定義7：可加速監(jiān)控器的判定：對監(jiān)控器M=(m1,m2,…,mn)中的可加速監(jiān)控器進行判定的過程，就是求解下列約束方程Cmul得到監(jiān)控器M′的過程：

利用性質的語義結構分析和從程序運行中獲得的執(zhí)行軌跡等監(jiān)控信息，已構建了啟發(fā)式算法對該多目標約束方程Cmul進行求解。實驗表明，該方程的求解結果能夠有效判定出哪些監(jiān)控器是“可加速”的，為實施軟件運行時驗證加速提供量化依據(jù)。

5 實驗驗證

為了驗證上述模型，采用某衛(wèi)星控制系統(tǒng)作為案例開展實驗。該衛(wèi)星載有多種執(zhí)行各種任務的設備(如照相機、溫度傳感器等)，地面人員通過操作指令可對衛(wèi)星進行控制。衛(wèi)星上發(fā)生的每個重要事件都被記錄在日志中并傳回給地面，地面日志模塊接受并存儲這些事件。我們將通過這些數(shù)據(jù)對軟件進行運行時驗證。

在實驗環(huán)境下，采用受控實驗方法收集其加速前完整的程序執(zhí)行軌跡信息，共生成500個軌跡，每個軌跡包含400個命令，平均軌跡長度是2 000個事件。此外，還收集了監(jiān)控開銷、驗證精度、診斷支持能力相關的實驗數(shù)據(jù)。

在驗證加速前，選取了CommandSuccess等各類不同類型的性質作為待驗證性質，系統(tǒng)中總共包含12個監(jiān)控器M=(m1,m2,…,m12)。例如，該衛(wèi)星系統(tǒng)期望行為應滿足命令成功(CommandSuccess)性質：每個Command(i,n,t1)事件應當最終跟隨Suceess(i,n,t2)事件，在期間不能有Fail(i,n,t3)事件發(fā)生。該性質可以用LTL表達如下：

□(Command(i,n,_)?Fail(i,n,_)USuccsee(i,n,_))

其中，□含義是“always”,U含義是”until”。

根據(jù)所收集實驗數(shù)據(jù)，結合定性評估和定量分析方法，得到了多目標約束模型Cmul的具體參數(shù)。接著，通過啟發(fā)式迭代算法對多目標模型求解，判定出性質L=(m2,m8,m10,m11)為可加速監(jiān)控器組，其中m2在運行中不再必要，m8、m11可進行動態(tài)調整，m10可改為以某時間間隔取樣驗證模式，且滿足多目標約束。根據(jù)該結果，將優(yōu)化后的監(jiān)控器轉換插入目標軟件實施運行時驗證。

通過對比加速前后的實驗數(shù)據(jù)，結果表明，所構建模型的求解結果能夠作為實施軟件運行時驗證加速的依據(jù)。在加速前平均開銷為51%，加速之后在滿足驗證精度、診斷支持能力前提下平均開銷減小為28%。

6 結束語

本文從多目標優(yōu)化角度研究軟件運行時驗證的加速問題，通過量化運行時驗證的多目標約束，構建了可加速監(jiān)控器的判定方程，作為運行時驗證加速的多目標約束模型。實驗表明：該模型的求解結果能夠為實施軟件運行時驗證加速提供量化依據(jù)。下一步，我們將繼續(xù)優(yōu)化本文所構建的多目標約束模型并改進對該模型求解的啟發(fā)式算法。

[1] FALCONE Y,FERNANDEZ J C,MOUNIER L.What can you verify and enforce at runtime[J].International Journal on Software Tools for Technology Transfer,2012,14(3):349-382.

[2] BODDEN E.Collaborative Runtime Verification with Tracematches[J].Journal of Logic and Computation,2010,20(3):707-723.

[3] CHEN F,ROSU G.MOP:An Efficient and Generic Runtime Verification Framework[J].Acm Sigplan Notices,2007,42(10):569-588.

[4] BODDEN E.Efficient Hybrid Typestate Analysis by Determining Continuation-Equivalent States[C]//Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering,2010.

[5] PURANDARE R,DWYER M B,ELBAUM S.Monitor Optimization Via Stutter-equivalent Loop Transformation[C]//Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications,2010.

[6] BONAKDARPOUR B,NAVABPOUR S,FISCHMEISTER S.Sampling-based Runtime Verification[C]//Proceedings of the 17th International Conference on Formal Methods，2011.

[7] NAVABPOUR S,WU C W W,BONAKDARPOUR B,et al.Efficient Techniques for Near-Optimal Instrumentation in Time-Triggered Runtime Verification[C]//Runtime Verification.Springer Berlin Heidelberg,2011:208-222.[8] BONAKDARPOUR B,NAVABPOUR S,FISCHMEISTER S.Form Methods Syst Des,2013,43:29.

[9] MEDHAT R,BONAKDARPOUR B,KUMAR D,et al.Runtime Monitoring of Cyber-Physical Systems Under Timing and Memory Constraints[J].ACM Transactions on Embedded Computing Systems (TECS),2015,14(4):79.

[10]BERKOVICH S,BONAKDARPOUR B,FISCHMEISTER S.GPU-based Runtime Verification[J].IEEE International Parallel & Distributed Processing Symposium (IPDPS),2013(5).

[11]NAVABPOUR S,BONAKDARPOUR B,FISCHMEISTER S.Time-Triggered Runtime Verification of Component-Based Multi-core Systems[C]//Runtime Verification，2015:153-168.

[12]周佳.支持故障恢復的多目標約束路由算法研究[D].北京：解放軍信息工程大學,2010.

[13]DWYER M B,PURANDARE R,PERSON S.Runtime Verification in Context:can Optimizing Error Detection Improve Fault Diagnosis[C]//Proceedings of the First International Conference on Runtime Verification,2010.

[14]VISWANATHAN M,KANNAN S,LEE I.Foundations for the Run-time Analysis of Software Systems[J].2000.

[15]冉慧，宋雪. 求解約束優(yōu)化問題的無參數(shù)填充函數(shù)算法[J].重慶理工大學學報(自然科學)，2013(5)：132-136.

(責任編輯 楊繼森)

Research on Modeling for Multi-Objective Constraint Among Speeding up Runtime Verification

LIU Yan-bin1, YE Fei2, WANG Yi-gang2

(1.The No. 13rdResearch Institute of China Electronics Technology Group Corporation, Shijiazhuang 050051, China; 2.Ordnance Engineering College of PLA, Shijiazhuang 050003, China)

Runtime verification of complicated properties imposed high overhead, which influences us to apply this method in the context of deployed systems. By identifying inherent dependencies among multi-objective constraint of runtime verification, a decision equation was constructed to decide that which is optimizable monitor, and this decision equation can be considered as a multi-objective constrained model for speeding up runtime verification. Experimental results show that this model is capable of deciding that the optimizable monitor and provides a quantitative basis for speeding up runtime verification.

runtime verification; multi-objective constraint; monitor; monitoring overhead; runtime monitoring

2016-03-12；

2016-05-15

河北省自然科學基金項目(F2014506017)

劉彥斌(1978—)，男，博士，主要從事可信軟件研究。

10.11809/scbgxb2016.10.016

劉彥斌,葉飛，王毅剛.軟件運行時驗證加速中的多目標約束模型研究[J].兵器裝備工程學報，2016(10):80-83.

format:LIU Yan-bin,YE Fei,WANG Yi-gang.Research on Modeling for Multi-Objective Constraint Among Speeding up Runtime Verification[J].Journal of Ordnance Equipment Engineering,2016(10):80-83.

TP311

A

2096-2304(2016)10-0080-05