軟件運(yùn)行時(shí)驗(yàn)證加速中的多目標(biāo)約束模型研究

劉彥斌,葉 飛，王毅剛

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

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

?

【信息科學(xué)與控制工程】

軟件運(yùn)行時(shí)驗(yàn)證加速中的多目標(biāo)約束模型研究

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

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

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

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

運(yùn)行時(shí)驗(yàn)證；多目標(biāo)約束；監(jiān)控器；監(jiān)控開(kāi)銷；運(yùn)行時(shí)監(jiān)控

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

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

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

1 研究現(xiàn)狀

當(dāng)前針對(duì)軟件運(yùn)行時(shí)驗(yàn)證加速的研究主要包括以下幾類：

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

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

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

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

但上述研究單純考慮如何減小運(yùn)行時(shí)驗(yàn)證開(kāi)銷，沒(méi)有把軟件運(yùn)行時(shí)驗(yàn)證加速歸結(jié)為多目標(biāo)優(yōu)化問(wèn)題。

2 多目標(biāo)決策基本原理

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

(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)為目標(biāo)函數(shù)，p維向量(f1(x),f2(x),…,fp(x))所在空間稱為目標(biāo)空間；X是決策空間上的可行集。多目標(biāo)決策過(guò)程就是求解得到近似的非劣解集的過(guò)程。

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

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

3 多目標(biāo)約束分析

3.1 性質(zhì)違背檢測(cè)能力

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

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

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

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

3.2 監(jiān)控開(kāi)銷評(píng)估

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

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

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

其次，一般說(shuō)來(lái)，采用過(guò)去時(shí)間LTL或者M(jìn)TL書(shū)寫(xiě)的公式比采用將來(lái)時(shí)間的公式更容易表達(dá)安全性需求。由于這些公式僅僅涉及過(guò)去，它們的值在軌跡中的任何狀態(tài)中通常或者為T(mén)rue或者為False，而不像將來(lái)時(shí)間公式那樣，需要在“未來(lái)”進(jìn)行判定。從而這些過(guò)去時(shí)間書(shū)寫(xiě)的性質(zhì)規(guī)約更適于基于邏輯的監(jiān)測(cè)。因此，在監(jiān)測(cè)需求規(guī)約生成中盡可能采用過(guò)去時(shí)間算子進(jìn)行性質(zhì)表達(dá)。

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

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

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

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

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

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

3.4 診斷支持能力

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

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

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

4 多目標(biāo)約束模型的構(gòu)建

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

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

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

本項(xiàng)目所說(shuō)的可加速監(jiān)控器既包括單個(gè)可加速監(jiān)控器，也包括可加速監(jiān)控器組，是對(duì)兩者的統(tǒng)稱。軟件運(yùn)行時(shí)驗(yàn)證加速過(guò)程需要在減小監(jiān)控開(kāi)銷、提高驗(yàn)證精度和改善診斷支持能力多個(gè)互相制約的目標(biāo)間進(jìn)行權(quán)衡，對(duì)可加速監(jiān)控器的判定過(guò)程定義如下。

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

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

5 實(shí)驗(yàn)驗(yàn)證

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

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

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

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

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

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

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

6 結(jié)束語(yǔ)

本文從多目標(biāo)優(yōu)化角度研究軟件運(yùn)行時(shí)驗(yàn)證的加速問(wèn)題，通過(guò)量化運(yùn)行時(shí)驗(yàn)證的多目標(biāo)約束，構(gòu)建了可加速監(jiān)控器的判定方程，作為運(yùn)行時(shí)驗(yàn)證加速的多目標(biāo)約束模型。實(shí)驗(yàn)表明：該模型的求解結(jié)果能夠?yàn)閷?shí)施軟件運(yùn)行時(shí)驗(yàn)證加速提供量化依據(jù)。下一步，我們將繼續(xù)優(yōu)化本文所構(gòu)建的多目標(biāo)約束模型并改進(jìn)對(duì)該模型求解的啟發(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]周佳.支持故障恢復(fù)的多目標(biāo)約束路由算法研究[D].北京：解放軍信息工程大學(xué),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)化問(wèn)題的無(wú)參數(shù)填充函數(shù)算法[J].重慶理工大學(xué)學(xué)報(bào)(自然科學(xué))，2013(5)：132-136.

(責(zé)任編輯 楊繼森)

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

河北省自然科學(xué)基金項(xiàng)目(F2014506017)

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

10.11809/scbgxb2016.10.016

劉彥斌,葉飛，王毅剛.軟件運(yùn)行時(shí)驗(yàn)證加速中的多目標(biāo)約束模型研究[J].兵器裝備工程學(xué)報(bào)，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