多目標約束下軟件運行時驗證加速技術框架

劉彥斌,王毅剛，葉　飛

(1.中國電子科技集團公司第十三研究所，石家莊　050051；2.中國人民解放軍軍械工程學院，石家莊　050003)

?

多目標約束下軟件運行時驗證加速技術框架

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

(1.中國電子科技集團公司第十三研究所，石家莊050051；2.中國人民解放軍軍械工程學院，石家莊050003)

軟件運行時驗證是一種近年來逐步興起的通過監(jiān)控程序運行來檢驗其是否滿足給定性質的輕量級驗證技術。由于復雜性質的運行時驗證中常產生高額的時間開銷，阻礙了該技術在部署后系統(tǒng)中的應用。在深入剖析國內外研究現(xiàn)狀及存在問題基礎上，從改善部署后軟件運行時驗證效率的角度出發(fā)，綜合考慮性質違背檢測能力、診斷支持能力等潛在開銷優(yōu)化制約因素，提出多目標約束下的軟件運行時驗證加速技術框架。該框架包括構建多目標約束模型、可加速監(jiān)控器判定、加速控制技術研究以及原型工具開發(fā)等內容，并具體闡述了框架所涉及的關鍵技術方案。本研究將為解決運行時驗證中的開銷問題提供關鍵技術支撐，為運行時驗證技術在部署后系統(tǒng)中的工程化應用奠定基礎。

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

本文引用格式：劉彥斌,王毅剛，葉飛.多目標約束下軟件運行時驗證加速技術框架[J].兵器裝備工程學報，2016(8):88-92.

運行時驗證(Runtime Verification)是一種近10多年來逐步興起的針對程序具體運行的輕量級驗證技術。它把形式化驗證技術和系統(tǒng)的實際運行結合起來，通過監(jiān)控程序運行并檢驗其是否滿足給定性質實現(xiàn)對系統(tǒng)的驗證。典型的實現(xiàn)方式是：在靜態(tài)階段，根據(jù)性質規(guī)約轉換生成監(jiān)控器(Monitor)，并插樁程序使之能夠在運行中向監(jiān)控器發(fā)送相關事件；在動態(tài)運行階段，監(jiān)控器處理這些事件序列并決定是否滿足性質規(guī)約。由于運行時驗證針對的對象僅僅是系統(tǒng)運行中的單個或者少數(shù)執(zhí)行軌跡，不需要針對整個系統(tǒng)模型，從而避免了狀態(tài)空間爆炸問題。而且，監(jiān)控器能夠被集成為被驗證系統(tǒng)的一部分，不但可以用來檢測軟件運行中的錯誤，也可在檢測到性質違背時及時采取措施(如，執(zhí)行修復代碼等)，從而提供額外的系統(tǒng)運行階段安全保障。

伴隨軟件運行時驗證技術的發(fā)展,在常規(guī)的狀態(tài)性質、時序性質，以及并發(fā)程序涉及的并發(fā)性質[17]之外，人們希望通過運行時驗證技術來驗證更為復雜的系統(tǒng)屬性。比如，參數(shù)化性質，這類性質往往要求特定類型的所有對象或數(shù)據(jù)結構的所有實例都滿足或不滿足。在面向對象程序中，經常會要求其動態(tài)實例化后產生的所有對象都滿足某個特定時序性質；在并發(fā)程序中,要求所有動態(tài)創(chuàng)建的進程都滿足某個性質[15]。對參數(shù)化性質等復雜性質的運行時驗證也是當前的研究熱點。

但是，參數(shù)化性質等較為復雜性質的在線運行時驗證中，由于需要維持大量的監(jiān)控器實例并處理程序實體中生成的大量事件，經常產生高額的開銷(Overhead)。研究表明，對于當前具有代表性的運行時驗證工具JavaMOP[9]和Tracematches[8]，所產生的平均開銷分別為41%和112%，一些復雜性質產生的開銷能達到程序執(zhí)行時間的970%[18]，如此高的開銷，是用戶所不能容忍的。尤其對于部署后的實際用戶使用環(huán)境中的程序而言，用戶所能容忍的開銷更低。根據(jù)Bodden等[8]的調查結果，工業(yè)界普遍所能接受的開銷應當在5%以內。開銷問題阻礙了運行時驗證技術在實踐中被廣泛用于軟件部署后環(huán)境，而大部分僅僅停留在軟件測試過程中使用。如何減小軟件運行時驗證開銷，已成為當前亟待解決的難點問題。

本文在深入剖析國內外研究現(xiàn)狀及存在問題基礎上，從改善部署后軟件運行時驗證效率的角度出發(fā)，綜合考慮性質違背檢測能力、診斷支持能力等潛在開銷優(yōu)化制約因素，提出多目標約束下的軟件運行時驗證加速技術框架。通過開展多目標約束模型構建、可加速監(jiān)控器判定、加速控制等關鍵技術研究以及相關支持工具研制，實現(xiàn)運行時驗證加速目的。該研究將為解決運行時驗證中的開銷問題提供關鍵技術支撐，為運行時驗證技術在部署后系統(tǒng)中的工程化應用奠定基礎。

1　國內外研究現(xiàn)狀

近年來，軟件運行時驗證技術在國際上備受關注，包括美國國家航空航天局AMES研究中心、伊利諾伊大學香檳分校、賓夕法尼亞大學、慕尼黑工業(yè)大學、IBM Haifa研究中心等在內的許多國際研究機構正持續(xù)開展運行時驗證理論與方法研究。研究方向包括性質規(guī)約與在線檢驗算法[2-4]、軌跡生成方法[5]、運行時執(zhí)行(Runtime Enforcement)與反饋[6]等。開發(fā)的代表性的運行時驗證工具包括： JavaMaC[7]、Tracematches[8]、MOP[9-10]、RuleR[11]、JPaX[12]、QVM[13]等。國內，國防科技大學、北京大學等單位也開展了相應的研究。例如，董威等[14-16]研究了主動監(jiān)控理論及預測監(jiān)控器的生成方法。針對軟件運行時驗證加速的研究主要包括以下幾類：

1) 聯(lián)合靜態(tài)分析減小開銷。通過靜態(tài)分析可減少從程序中提取事件所需的插樁點數(shù)量。Dwyer 等[19]利用靜態(tài)分析來移除Typestate性質監(jiān)控中不必要的插樁。Bodden等[20-22]探索了許多輕量級的代碼靜態(tài)分析方法，通過識別可安全移除的插樁點減小開銷。Purandare 等[23]優(yōu)化了程序中性質相關的循環(huán)結構，通過僅僅監(jiān)控有限次數(shù)的循環(huán)減小開銷。

2) 基于取樣的開銷優(yōu)化方法。該類技術通過對性質或者事件取樣減小開銷。Diep等[24]提出了基于格的取樣技術減小路徑性質監(jiān)控中的開銷。Bonakdarpour等[25]提出了時間觸發(fā)的運行時驗證概念，監(jiān)控器周期性地取樣程序狀態(tài)評估性質是否成立。Navabpour等[26]研究了啟發(fā)式算法求解給定取樣周期內需要被緩沖的最小數(shù)量的關鍵事件，以便時間-觸發(fā)的監(jiān)控器能夠成功重構兩個連續(xù)取樣時間內的程序狀態(tài)。Goodloe等[27]從語言層面提供了基于取樣的監(jiān)控機制。Arnold等[13]構建了被稱為質量虛擬機(QVM)的特殊運行時環(huán)境，采用了性質指導的取樣和對象為中心的取樣策略。

3) 基于多用戶協(xié)同的開銷分解方法。Bodden 等[8]提出了多用戶協(xié)同的運行時驗證技術。該技術通過將運行時驗證任務分配給多個用戶，每個用戶僅僅執(zhí)行部分插樁的程序，從而減小每個用戶所承擔的開銷。該技術源自Liblit等[28]所提出的基于統(tǒng)計方法的協(xié)同bug診斷思想，利用源自多用戶的大量程序執(zhí)行軌跡的信息組合進行失效的隔離。

通過直接或者間接減小插樁點和監(jiān)控器數(shù)量減小開銷，是運行時驗證中開銷優(yōu)化的基本思路，如圖1所示。雖然現(xiàn)有研究在開銷優(yōu)化方面取得了一定的成果， 可以有效減小插樁點數(shù)量(如聯(lián)合靜態(tài)分析、事件取樣)和減小監(jiān)控器數(shù)量(如性質取樣)。但當前研究尚存在許多不足之處：首先，已有研究沒有充分考慮開銷優(yōu)化中的潛在制約因素，沒有充分考慮開銷優(yōu)化對診斷支持能力的潛在影響，在優(yōu)化過程中可能會損害系統(tǒng)正常功能。其次，難以滿足工程界的“有界開銷”需求。當前研究主要集中于“盡可能減小開銷”，從技術本質而言，所產生的開銷仍然是“無界的(Unbounded)”。而目前工程中更關注的是如何使得在各種條件下開銷都能滿足要求，即“有界(Bounded)的”開銷。盡管有學者[29]初步探索了控制方法產生有界開銷，但適用范圍尚很有限。

圖1　開銷優(yōu)化示意圖

2　運行時驗證加速技術框架

針對當前研究中存在的上述問題，本研究從改善部署后軟件運行時驗證效率的角度出發(fā)，不僅將開銷作為優(yōu)化目標，還同時考慮開銷優(yōu)化對驗證結果準確性以及診斷支持能力的影響。把軟件運行時驗證的優(yōu)化歸結為多目標優(yōu)化問題，以減小監(jiān)控開銷、提高驗證精度、改善診斷支持能力為優(yōu)化目標，構建了多目標約束下的軟件運行時驗證加速技術框架。所構建的框架如圖2所示，主要包括軟件運行時驗證中的多目標約束建模、可加速監(jiān)控器判定技術、加速控制技術、工具原型開發(fā)及應用試驗等內容。

圖2　技術框架示意圖

1) 軟件運行時驗證中的多目標約束建模

在軟件運行時驗證中，由于性質驗證和診斷所需信息源常常重疊，優(yōu)化監(jiān)控開銷不僅影響性質違背檢測能力，而且能夠影響診斷所需信息的收集。軟件運行時驗證加速過程需要在減小監(jiān)控開銷、提高驗證精度和改善診斷支持能力多個互相制約的目標間進行權衡。

該技術以實驗分析方法為基礎，識別運行時驗證優(yōu)化過程中多目標間的內在依賴關系，抽取出細粒度的影響變量，量化多目標約束，構造開銷量化模型、性質違背檢測能力評估模型和診斷支持能力評估模型，進而建立多目標約束模型，作為軟件運行時驗證加速的分析依據(jù)。

2) 多目標約束下的可加速監(jiān)控器判定

在實施運行時驗證加速之前，需要首先判定出哪些監(jiān)控器是“可加速”的，即判定出哪些監(jiān)控器在運行中不再必要、哪些可以進行動態(tài)調整，且滿足多目標約束。對于參數(shù)化性質等復雜性質而言，由于監(jiān)控器數(shù)量龐大，存在動態(tài)性、不確定性等特征，且監(jiān)控開銷、驗證精度和診斷支持能力之間常常發(fā)生沖突，滿足多目標約束的可加速監(jiān)控器的判定是非常困難的。

該技術將探索基于多目標模型求解的可加速監(jiān)控器判定技術。利用性質的語義結構分析和從程序運行中獲得的執(zhí)行軌跡等監(jiān)控信息，研究啟發(fā)式算法進行監(jiān)控器“可加速”判定。將利用程序執(zhí)行軌跡等監(jiān)控信息，一方面結合統(tǒng)計分析和機器學習技術，構建被驗證系統(tǒng)的統(tǒng)計模型，挖掘不同監(jiān)控器之間的潛在聯(lián)系，判定某監(jiān)控器是否必要；另一方面用來迭代確定多目標模型中的相關參數(shù)值。該技術能夠識別出滿足多目標約束的可加速監(jiān)控器以及相應的加速操作方式，作為實施軟件運行時驗證加速的輸入。

3) 軟件運行時驗證的加速控制技術

為滿足工程界對“有界(Bounded)開銷”的需求，該技術將研究運行時驗證的加速控制技術，利用反饋控制機理，動態(tài)調整監(jiān)控器，將開銷控制在用戶可接受范圍之內；同時，在加速過程中，必須滿足多目標約束，不能影響驗證精度。由于傳統(tǒng)的比例-積分-微分(PID)控制、監(jiān)督控制等理論不能直接應用在非線性離散系統(tǒng)中，將針對被驗證系統(tǒng)的特點，研究相應的加速控制實施機制和算法。所研究的自適應加速控制算法，能夠在軟件運行過程中，以可加速監(jiān)控器及相應的加速操作方式為輸入，利用系統(tǒng)當前實際開銷和目標閾值間的誤差進行反饋控制，自適應地對監(jiān)控器進行增量式在線動態(tài)調整(例如，臨時關閉某監(jiān)控器)，避免監(jiān)控開銷超出用戶所能接受的水平。

4) 在上述研究基礎上，研制支持工具原型并進行應用試驗

基于以上研究成果，設計實現(xiàn)相應的支持工具原型，支持多目標約束模型構建、可加速監(jiān)控器判定以及加速控制技術的實現(xiàn)，并在具體案例中進行應用試驗。進而，根據(jù)實際效果和應用反饋進一步改進所研究的模型與方法。

3　多目標約束模型

本文將監(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))所在空間是目標空間。

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

(1)

Cmul就是本文所構建的多目標約束模型，它的具體推導過程將在別的文獻中具體闡述。利用性質的語義結構分析和從程序運行中獲得的執(zhí)行軌跡等監(jiān)控信息，已構建了啟發(fā)式算法對該多目標約束方程Cmul進行求解。

4　實驗與驗證

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

所開展實驗的具體步驟及技術路線如圖3所示。主要包括數(shù)據(jù)準備、多目標約束模型構建、程序執(zhí)行軌跡統(tǒng)計分析、可加速監(jiān)控器判定、加速控制算法和驗證精度補償?shù)戎饕襟E。

1) 數(shù)據(jù)準備。首先，采用受控實驗方法獲取某衛(wèi)星模型控制系統(tǒng)運行時驗證相關實驗數(shù)據(jù)。選取了CommandSuccess、SAFEFILEWRITE等各類不同類型的性質作為待驗證性質。例如，該衛(wèi)星系統(tǒng)期望行為應滿足CommandSuccess性質：每個Command(i,n,t1)事件應當最終跟隨Suceess(i,n,t2)事件，在期間不能有Fail(i,n,t3)事件發(fā)生。該命令成功(CS,command success)性質可以用LTL進行表達。在實驗環(huán)境下，收集其加速前完整的程序執(zhí)行軌跡信息，共生成500個軌跡，每個軌跡包含400個命令，平均軌跡長度是2 000個事件。此外，還收集了監(jiān)控開銷、驗證精度、診斷支持能力相關的實驗數(shù)據(jù)。

2) 多目標約束模型構建及求解。根據(jù)所收集實驗數(shù)據(jù)，結合定性評估和定量分析方法，建立初步的開銷度量函數(shù)、性質違背檢測能力評價函數(shù)和診斷支持能力評價函數(shù)，通過考察三者之間的內在依賴關系，得到多目標約束模型Cmul的具體參數(shù)。由于各個目標之間相互存在沖突，采用了啟發(fā)式迭代算法對多目標模型求解，得到決策空間上的最優(yōu)解M′，并將M′中的監(jiān)控器轉換插入目標軟件，從而對其進行運行時監(jiān)控。

圖3　實驗步驟及技術路線示意圖

3) 結合統(tǒng)計分析和機器學習方法，對目標系統(tǒng)運行中獲得的執(zhí)行軌跡等監(jiān)控信息進行統(tǒng)計分析，構建目標系統(tǒng)的統(tǒng)計模型。由于在隱馬爾可夫模型中，根據(jù)可觀察狀態(tài)能夠確定系統(tǒng)的隱含狀態(tài)。從系統(tǒng)完整的執(zhí)行軌跡中學習并構建了隱馬爾科夫統(tǒng)計模型(HMM)，并利用該模型來彌補加速過程中可能造成的監(jiān)控事件缺失。

4) 應用控制理論，將加速控制問題轉化為對非線性系統(tǒng)設計一個最優(yōu)控制器的問題。改進并聯(lián)合面向離散時間系統(tǒng)的PID控制器和面向離散事件系統(tǒng)的監(jiān)督控制理論，設計滿足約束的控制器。在此基礎上，設計了自適應加速控制算法，使之能夠根據(jù)開銷量化模型進行開銷預測，實現(xiàn)費用感知的加速控制。

通過對比加速前后的實驗數(shù)據(jù)，結果表明，在加速前平均開銷為51%，加速之后在滿足驗證精度、診斷支持能力前提下平均開銷減小為28%，通過加速控制算法臨時關閉某些監(jiān)控器可將平均開銷控制在10%以內。

5　結束語

通過深入剖析國內外研究現(xiàn)狀及存在問題，本文提出多目標約束下的軟件運行時驗證加速技術框架。與現(xiàn)有運行時驗證開銷優(yōu)化方法相比，其特色和創(chuàng)新之處主要在于：① 從多目標優(yōu)化角度研究軟件運行時驗證的加速技術，通過建立多目標優(yōu)化模型優(yōu)化調整“監(jiān)控器”，提高系統(tǒng)性能；② 融合控制理論、機器學習等多學科技術，實現(xiàn)軟件運行時驗證加速。初步實驗結果表明，本文所提方法能夠在滿足多目標約束前提下有效減小驗證開銷，實現(xiàn)驗證加速目的。下一步將在本文研究基礎上，進一步開展對比實驗改進框架中的各項關鍵技術。

[1]張獻,董威,齊治昌.基于AOP的運行時驗證中的沖突檢測[J].軟件學報,2011(6).

[2]BAUER A,LEUCKER M,SCHALLHART C.The good,the bad,and the ugly—but how ugly is ugly?[C]//Proceedings of the 7th International Workshop on Runtime Verification (RV’07).2007:126-138.

[3]BAUER A,LEUCKER M,SCHALLHART C.Comparing LTL Semantics for Runtime Verification[J].Journal of Logic and Computation,2010,20(3):651-674.

[4]MEREDITH P O.Efficient monitoring of parametric context-free patterns[J].Automated Software Engineering,2010.17(2):149-180.

[5]SEYSTER J,DIXIT K,HUANG X,et al.Aspect-oriented instrumentation with GCC[C]//Proceedings of the 1st International Conference on Runtime Verification.LNCS,2010:405-420.

[6]FALCONE Y,FEMANDEZ J C,MOUNIER L.What can you verify and enforce at runtime?[Z].Software Tools for Technology Transfer,Special Section on Runtime Verification,2011.

[7]KIM M.Java-MaC:A run-time assurance approach for Java programs[J].Formal Methods in System Design,2004,24(2):129-155.

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

[9]CHEN F,GOSU G.MOP:An efficient and generic runtime verification framework[J].Acm Sigplan Notices,2007,42(10):569-588.

[10]MEREDITH P,JIN D,GRIFFITH D,et al.An overview of the MOP runtime verification framework[Z].Software Tools for Technology Transfer.Special Section on Runtime Verification,2011.

[11]BARRINGER H,RYDEHEARD D,HAVELUND K.Rule Systems for Run-time Monitoring:from EAGLE to RULER[J].Journal of Logic and Computation,2010,20(3):675-706.

[12]HAVELUND K,ROSU G.An overview of the runtime verification tool Java PathExplorer[J].Formal Methods in System Design,2004,24(2):189-215.

[13]ARNOLD M,VECHEV M,YAHAV E.QVM:An Efficient Runtime for Detecting Defects in Deployed Systems[J].ACM Trans Softw Eng Methodol,2011,21(1):1-35.

[14]WEI D,MARTIN L,SCHALLHART C.Impartial anticipation in runtime verification[C]//Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis,Springer-Verlag,2008.

[15]趙常智，董威，隋平，等.面向參數(shù)化LTL的預測監(jiān)控器構造技術[J].軟件學報,2010(2):318-334.

[16]ZHAO C Z,JI W D, SUI P,et al.Software Active Online Monitoring Under Anticipatory Semantics[C]//1st International Workshop on Software Health Management 2009:Pasadena,California,USA.

[17]QADEER S,TASIRAN S.Runtime verification of concurrency-specific correctness criteria[Z].Software Tools for Technology Transfer,Special Section on Runtime Verification,2011.

[18]BODDEN E,HENDREN L,LHOTAK O.A staged static program analysis to improve the performance of runtime monitoring[C]//European Conference on Object-Oriented Programming,2007:525-549.

[19]DWYER M,PURANDARE R.Residual dynamic typestate analysis.In:Int’l[C]//Conf on Aut Soft Eng，2007:124-133.

[20]ERIC B,LAURIE H.A staged static program analysis to improve the performance of runtime monitoring[Z].2007.

[21]BODDEN E.Efficient hybrid typestate analysis by determining continuation-equivalent states[C]//Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering，ACM:Cape Town,South Africa.2010.

[22]BODDEN E,LAM P,HENDREN L.Finding programming errors earlier by evaluating runtime monitors ahead-of-time[C]//Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering，ACM:Atlanta,Georgia.2008:36-47.

[23]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，ACM:Reno/Tahoe,Nevada,USA.2010:270-285.

[24]DIEP M M,DWYER M B,ELBAUM S.Lattice-Based Sampling for Path Property Monitoring[J].ACM Trans Softw Eng Methodol,2011,21(1):1-43.

[25]BONAKDARPOUR B,NAVABPOUR S,FISCHMEISTER S.Sampling-based runtime verification[C]//Proceedings of the 17th international conference on Formal methods，Springer-Verlag:Limerick,Ireland.2011:88-102.

[26]NAVABPOUR S,WU W W C,BONAKDARPOUR B,et al.Efficient techniques for near-optimal instrumentation in time-triggered runtime verification[C]//Runtime Verication,2011.

[27]PIKE L.Copilot:a hard real-time runtime monitor[C]//Proceedings of the First international conference on Runtime verification,Springer-Verlag:St.Julians,Malta.2010:345-359.

[28]JIN G.Instrumentation and sampling strategies for cooperative concurrency bug isolation[C]//Proceedings of the ACM international conference on Object oriented programming systems languages and applications,Reno/Tahoe,Nevada,USA.2010:241-255.

[29]CALLANAN S.Software monitoring with bounded overhead[C]//Parallel and Distributed Processing,IPDPS 2008.

[30]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,Springer-Verlag:St.Julians,Malta.2010:36-50.

[31]JIN D.Garbage collection for monitoring parametric properties[C]//Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation.San Jose,California,USA.2011:415-424.

(責任編輯楊繼森)

Runtime Verification Speeding up Based on Multi-Objective Constraint

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

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

Runtime verification is a relatively new lightweight formal verification method which is concerned with dynamic monitoring and analysis of system executions with respect to precisely specified properties. Runtime verification of complicated properties that involve many system variables imposes high overhead, which makes it is hard to apply this method in the context of deployed systems. This paper considered all the latent constraints including the efficiency of property violation detection and fault diagnosis. It involved the key technology at the topic of speeding up for runtime verification on the condition of multi-objective constraint. It mainly includes: to construct a model of multi-objective constraint, to resolve the problem of how to recognize the involved monitor for speeding up by constructing heuristic algorithm to get the answer for multi-objective model on the basis of monitoring statistics information of verified systems before speeding up, using control theory, to implement runtime verification speeding up by constructing self-adaptive speeding up control algorithm. This research will provide key technologies for resolving the overhead problem of runtime verification. And it can also provide a basis for applying the runtime verification method for actual deployed systems.

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

2016-02-29；

216-03-26

河北省自然科學基金項目“多目標約束下的軟件運行時驗證加速技術研究”(F2014506017)

劉彥斌(1978—)，男，博士，高級工程師，主要從事可信軟件研究；王毅剛(1975—)，男，博士；葉飛(1979—)，男，博士。

10.11809/scbgxb2016.08.020

format:LIU Yan-bin, WANG Yi-gang, YE Fei.Runtime Verification Speeding up Based on Multi-Objective Constraint[J].Journal of Ordnance Equipment Engineering,2016(8):88-92.

TP311

A

2096-2304(2016)08-0088-06

【信息科學與控制工程】