摘要：本文結(jié)合作者課題內(nèi)容，介紹了一種運(yùn)行時(shí)驗(yàn)證技術(shù)中的監(jiān)控器構(gòu)造方法。該方法完整涵蓋了從性質(zhì)規(guī)約到監(jiān)控器模型再到監(jiān)控程序的全過(guò)程，過(guò)程中使用了相關(guān)開(kāi)源的第三方軟件使得該方法的自動(dòng)化程度較高。同時(shí)由于該監(jiān)控器的構(gòu)造是基于三值語(yǔ)義，使得該監(jiān)控器在一定意義上具有預(yù)測(cè)性。

關(guān)鍵詞：運(yùn)行時(shí)驗(yàn)證；監(jiān)控器模型；監(jiān)控程序；三值語(yǔ)義

中圖分類(lèi)號(hào)：TP311.52 文獻(xiàn)標(biāo)識(shí)碼：A 文章編號(hào)：1007-9599 （2012） 20-0000-02

1 引言

運(yùn)行時(shí)驗(yàn)證[1]是一種新興的輕量級(jí)程序驗(yàn)證技術(shù)。在運(yùn)行時(shí)驗(yàn)證中，通常從系統(tǒng)需求中產(chǎn)生監(jiān)控器，監(jiān)控器通過(guò)觀測(cè)程序的執(zhí)行來(lái)檢查程序運(yùn)行過(guò)程是否滿(mǎn)足系統(tǒng)需求，是傳統(tǒng)的軟件驗(yàn)證和確認(rèn)技術(shù)，比如測(cè)試[2]和模型驗(yàn)證[3]的有效補(bǔ)充。它不但可以有效的檢測(cè)系統(tǒng)運(yùn)行中的異常行為，而且也使得在檢測(cè)到正確性背離時(shí)有效地修復(fù)系統(tǒng)成為可能。

本文結(jié)合作者課題中的相關(guān)工作，介紹了一種運(yùn)行時(shí)驗(yàn)證監(jiān)控器構(gòu)造方法，該方法結(jié)合LTL3 Tools監(jiān)控器模型生成工具以及JavaMOP軟件開(kāi)發(fā)工具支持和分析框架，其完整的流程圖如圖1所示。

論文的組織如下：第二節(jié)結(jié)合案例介紹如何使用LTL3 Tools工具生成監(jiān)控器模型即FSM（finite-state machine， 有限狀態(tài)機(jī)），第三節(jié)結(jié)合案例介紹如何將監(jiān)控器模型經(jīng)過(guò)相應(yīng)處理后，通過(guò)JavaMOP生成成為監(jiān)控程序。最后進(jìn)行總結(jié)。

2 監(jiān)控模型的生成

在運(yùn)行時(shí)驗(yàn)證領(lǐng)域，LTL[4]（Linear Temporal Logic，線(xiàn)性時(shí)序邏輯）被廣泛的應(yīng)用，相應(yīng)的監(jiān)控性質(zhì)要通過(guò)LTL公式進(jìn)行描述。LTL公式的預(yù)測(cè)語(yǔ)義，也稱(chēng)三值語(yǔ)義[5]（簡(jiǎn)稱(chēng)LTL3）。相較典型的已經(jīng)被定義而且使用于運(yùn)行時(shí)驗(yàn)證工具的有窮軌跡上的兩值語(yǔ)義（true/1）監(jiān)控器，基于三值語(yǔ)義的監(jiān)控器非常適合于運(yùn)行時(shí)驗(yàn)證。一方面，三值語(yǔ)義的公平性使得監(jiān)控器的裁決始終是正確的，另一方面，三值語(yǔ)義的預(yù)測(cè)性使得監(jiān)控器有發(fā)現(xiàn)一條無(wú)窮運(yùn)行軌跡的最小好[6]（壞）前綴的能力，即監(jiān)控器能盡可能早的作出裁決，因此在一定意義上具有預(yù)測(cè)性。所以本文的監(jiān)控器構(gòu)造也將使用三值語(yǔ)義。三值語(yǔ)義監(jiān)控器的理論構(gòu)造過(guò)程請(qǐng)參照文獻(xiàn)[7]。

LTL3 Tools是一個(gè)將給定LTL公式φ轉(zhuǎn)換為FSM（finite-state machine， 有限狀態(tài)機(jī)）表示Mφ的工具集。該工具集為免費(fèi)使用，在網(wǎng)上可以下載。FSM可以看作是一個(gè)基于三值語(yǔ)義的監(jiān)控器模型，輸入有窮字u，它會(huì)判斷出是否公式成立。

這里結(jié)合一個(gè)案例，進(jìn)行介紹：

對(duì)一個(gè)軟件監(jiān)測(cè)以下需求：直到init后才進(jìn)行spawn，即只有初始化以后才能調(diào)用spawn操作。對(duì)應(yīng)的LTL規(guī)約為： ！spawn U init

通過(guò)ltl2mon（該程序?yàn)長(zhǎng)TL3 Tools輸入規(guī)約的入口）程序輸入以下命令：$./ltl2mon \"（！ spawn） U init\" | dot -Tps > graph.ps得到對(duì)應(yīng)的FSM格式的監(jiān)控器。得到監(jiān)控器自動(dòng)機(jī)的圖形化表示為：

其中，黃色是起始狀態(tài)，綠色是安全狀態(tài)，紅色是不安全狀態(tài)。

生成監(jiān)控器的結(jié)果也可以通過(guò)如下命令 $ ./ltl2mon \"（！ spawn） U init\" -itest.fsm > test.txt輸出到txt文檔中，形成一個(gè)文本格式的自動(dòng)機(jī)描述如圖3所示：

3 監(jiān)控程序的實(shí)現(xiàn)

我們的最終目的是對(duì)定義的LTL規(guī)約，生成相應(yīng)的監(jiān)控程序。這里我們將使用到JavaMOP，它是一個(gè)基于Java的面向?qū)ο缶幊蹋∕OP）軟件開(kāi)發(fā)工具支持和分析框架，它支持將FSM等邏輯轉(zhuǎn)化為Java程序的監(jiān)控器，支持面向方面編程的編織模式，是一個(gè)自動(dòng)化程度較高的運(yùn)行時(shí)驗(yàn)證框架。JavaMOP有相應(yīng)的邏輯處理層，用于處理各種邏輯，將其轉(zhuǎn)換成Java語(yǔ)言的表達(dá)方式，并且有相應(yīng)的處理層根據(jù)目標(biāo)Java文件輸出相應(yīng)面向方面的監(jiān)控器表達(dá)。

在之前的案例中得到監(jiān)控器模型的基礎(chǔ)上，通過(guò)JavaMOP生成監(jiān)控程序的過(guò)程如下。

1）對(duì)test.txt中描述的的監(jiān)控器，去除重復(fù)和空的遷移條件，例如”label=”，得到簡(jiǎn)化的自動(dòng)機(jī)。以“l(fā)abel”對(duì)應(yīng)的字母表為監(jiān)控事件，依據(jù)test.txt簡(jiǎn)化的自動(dòng)機(jī)，監(jiān)控目的為監(jiān)測(cè)unsafe的狀態(tài)，通過(guò)轉(zhuǎn)換可以得到的mop文件（這是JavaMOP的輸入文件，并不是一個(gè)可運(yùn)行的程序）。我們開(kāi)發(fā)了一個(gè)工具進(jìn)行轉(zhuǎn)換，其中根據(jù)需要可以適當(dāng)?shù)倪M(jìn)行人工修改，這個(gè)過(guò)程完全通過(guò)手動(dòng)完成也是可以的。

2）按如下命令javamop test.mop執(zhí)行，得到對(duì)應(yīng)的面向方面文件TestMonitorAspect.aj。

由于作者課題中所考慮的領(lǐng)域基本上都是由C或C++實(shí)現(xiàn)，因此沒(méi)有使用JavaMOP的植入功能，即在相應(yīng)節(jié)點(diǎn)中插裝一些程序段用于獲取監(jiān)控所關(guān)注的系統(tǒng)信息，而主要利用其生成監(jiān)控程序的功能，這使得作者課題中還為了獲取相應(yīng)的程序信息做了大量的相關(guān)工作。如果針對(duì)的是由Java實(shí)現(xiàn)的程序，直接利用JavaMOP的植入功能將使從目標(biāo)程序中獲取信息環(huán)節(jié)的工作可以由程序自動(dòng)完成。作者主要使用其中生成的監(jiān)控器代碼，它位于TestMonitor類(lèi)中，是一個(gè)監(jiān)控器類(lèi)，完成自動(dòng)機(jī)的功能。圖4是案例中最終生成的監(jiān)控程序中的一段實(shí)現(xiàn)監(jiān)控器監(jiān)控過(guò)程（即根據(jù)觀察到的事件發(fā)生遷移）的代碼，其中利用數(shù)組表示不同事件在不同狀態(tài)時(shí)發(fā)生的遷移。

圖4.案例監(jiān)控程序中實(shí)現(xiàn)監(jiān)控器監(jiān)控過(guò)程的代碼

4 總結(jié)和下一步工作

本文結(jié)合作者課題中相關(guān)內(nèi)容，介紹了了一種運(yùn)行時(shí)驗(yàn)證監(jiān)控器的構(gòu)造方法，該方法結(jié)合使用了開(kāi)源的第三方軟件LTL3 Tools和JavaMOP，使得其自動(dòng)化程度較高。

在下一步工作中作者將結(jié)合其他課題的工作將該方法整理成一個(gè)類(lèi)似于已經(jīng)成熟應(yīng)用的運(yùn)行時(shí)驗(yàn)證工具集Java-MaC[8]一樣的工具，只通過(guò)輸入相應(yīng)的監(jiān)控性質(zhì)就能完全自動(dòng)的生成相應(yīng)的監(jiān)控器程序。

參考文獻(xiàn)：

[1]S. Colin， L.Mariani. Run-Time Verification， chapter 18.[J].In LNCS，2005， 3472：525～555.

[2]J.Peleska.Test automation for safety-critical systems： Industrial application and future developments.[C].In FME’96： Third International symposium of Formal Methods Europe.In LNCS，1996，1051：39～59.

[3]E.M.Clarke， O.Grumberg， D.A.Peled， Model Checking.[J].In LNCS，2006， 1346：54～56.

[4]F.Kroger.The temporal logic of programs.[M].NewYork，USA：Springer-Verlag New York，1987：132～143.

[5]M. Geilen， “On the construction of monitors for temporal logic properties. ” Electr. Notes Theor. Comput. Sci.， vol. 55， no. 2， 2001

[6]Bauer，A.， Leucher，M.， Schallhart，C.Runtime verification for LTL and PTLTL.[C].Technical Report TUM-I0724，TU München，2007

[7]隋平.基于三值語(yǔ)義的軟件運(yùn)行時(shí)驗(yàn)證方法.[D].國(guó)防科技大學(xué)碩士學(xué)位論文，2010：12～15.

[8]M. Kim， S. Kannan， I. Lee， O. Sokolsky， M. Viswanathan.Java-MaC： a runtime assurance approach for Java programs.[J].Formal Methods in Systems Design， March 2004，24（2）：129～155.

[作者簡(jiǎn)介]

張可迪（1988-），男，在讀碩士，主要研究領(lǐng)域?yàn)檐浖臏y(cè)試與驗(yàn)證；董威（1976-），男，博士，教授，主要研究領(lǐng)域?yàn)楦呖尚跑浖こ?，高可信軟件技術(shù)。