廖慧芬，詹 芹

LIAO Hui-fen，ZHAN Qin

（九江學(xué)院 信息科學(xué)與技術(shù)學(xué)院，九江 330005）

1 JPF工作原理和體系結(jié)構(gòu)

JPF的基本工作原理是從被檢測對象中篩選出少量的狀態(tài)等價(jià)于原系統(tǒng)，然后交給JVM檢測，再對不符合系統(tǒng)性質(zhì)的檢測結(jié)果，JPF可以用不同的方式顯示錯(cuò)誤路徑及性質(zhì)違例。JPF有三種不同的輸出方式：分別是JPF報(bào)告系統(tǒng)（Reporting System）、JPF日志和應(yīng)用輸出。

JPF中的整個(gè)設(shè)計(jì)重點(diǎn)基本是JVM和Search對象，JVM的功能相當(dāng)于狀態(tài)生成器，在執(zhí)行過程中，首先JVM生成模型檢測使用的程序狀態(tài)，同時(shí)JVM中的三個(gè)重要的方法：Forward（）表示下一個(gè)狀態(tài)、Backtrack（）存儲回溯棧中的上一個(gè)狀態(tài)和RestoreState（）存儲一個(gè)任意狀態(tài)，控制程序狀態(tài)；Search的功能相當(dāng)于是JVM的驅(qū)動，篩選出供JVM處理的狀態(tài)，告訴JPF虛擬機(jī)在狀態(tài)空間中是前進(jìn)還是后退，同時(shí)具有性質(zhì)驗(yàn)證器的功能。

2 JPF的關(guān)鍵技術(shù)

在檢測過程中，JAVA程序狀態(tài)一般包括三部分，分別是對象的動態(tài)變量、類的靜態(tài)變量和每個(gè)線程的信息。由此可見，JAVA程序的狀態(tài)數(shù)量一般都是很大，在解決嚴(yán)重的狀態(tài)爆炸問題方面，JPF使用了啟發(fā)式路徑選擇生成器、on-the-fly偏序規(guī)約、主機(jī)VM執(zhí)行、狀態(tài)抽象、靜態(tài)分析、對稱規(guī)約和符號執(zhí)行等一系列的解決方案。

偏序規(guī)約（Partial Order Reduction）方法是利用行為的獨(dú)立性（Independence）來減少并行系統(tǒng)模型檢測中的狀態(tài)空間爆炸問題。因此，在算法中只需要考慮其中的一種狀態(tài)而忽略另一種狀態(tài)，狀態(tài)S通過這種方式可以轉(zhuǎn)換成比較小的另一個(gè)狀態(tài)S'，在執(zhí)行狀態(tài)空間遍歷時(shí)，只需要選擇合適并具有代表性的狀態(tài)集代替全部狀態(tài)集，從而達(dá)到減少狀態(tài)數(shù)量。

圖1 系統(tǒng)狀態(tài)轉(zhuǎn)移圖

近年來，在模型檢測中經(jīng)常用對稱（Symmetry）方法來避免狀態(tài)爆炸問題，對稱方法主要是利用了系統(tǒng)中的對稱結(jié)構(gòu)來進(jìn)行狀態(tài)精簡的。在JPF中，把對稱方法和偏序規(guī)約技術(shù)結(jié)合形成對稱規(guī)約技術(shù)，它的基本思想是，在模型檢測過程中對系統(tǒng)中需要進(jìn)行性質(zhì)驗(yàn)證的狀態(tài)形成等價(jià)狀態(tài)，只需要檢測這些等價(jià)狀態(tài)中的一個(gè)就可以了。假設(shè)一個(gè)并行系統(tǒng)中，行為集A={xi,yi,zi,ni}，狀態(tài)集S={Ni,Ti,Ci}。形成的完整系統(tǒng)狀態(tài)轉(zhuǎn)移如圖1所示。注意到，圖1中存在明顯的對稱關(guān)系，使用對稱規(guī)約可以得到如圖2所示的新的狀態(tài)轉(zhuǎn)移圖。同時(shí)，行為y、z是獨(dú)立的，可以使用偏序規(guī)約對系統(tǒng)作進(jìn)一步的狀態(tài)精簡，從而得到與原系統(tǒng)等價(jià)的狀態(tài)較少的狀態(tài)空間，如圖3所示。

圖2 對稱規(guī)約后的狀態(tài)轉(zhuǎn)移圖圖

圖3 偏序規(guī)約后的狀態(tài)轉(zhuǎn)移圖

3 基于JPF的Eclipse模型檢測平臺實(shí)現(xiàn)

JPF不僅可以實(shí)現(xiàn)對Java程序的模型檢測功能，它還提供了很強(qiáng)的程序擴(kuò)展功能。本文使用JPF的Eclipse的PDE來進(jìn)行JPF插件的開發(fā)，使用PDE提供工程向?qū)В陆ㄒ粋€(gè)Eclipse Plug-in項(xiàng)目。

3.1 分析插件要實(shí)現(xiàn)的功能，標(biāo)識需要進(jìn)行添加的擴(kuò)展點(diǎn)

plugin.xml是插件和Eclipse內(nèi)核的接口，它提供的擴(kuò)展點(diǎn)非常多，常見的擴(kuò)展點(diǎn)有透視圖（perspectives）、視圖（views）、編輯器（editors）、首選項(xiàng)（preferencePages）、幫助（toc）和上下文幫助（context）。需要為每個(gè)class關(guān)聯(lián)一個(gè)配置文件（后綴為.cjp），通過讀取cjp文件的配置信息，使用JPF來檢測目標(biāo)class文件。首先在工具欄中設(shè)計(jì)一個(gè)按鈕來啟動插件的配置對話框，用于配置和管理被檢測類的配置文件，然后還需要專門的面板來并顯示檢測的結(jié)果。

3.2 根據(jù)擴(kuò)展點(diǎn)的規(guī)范來實(shí)現(xiàn)這些擴(kuò)展

新建一個(gè)類MyJpfButtonAction，實(shí)現(xiàn)接口IWorkbenchWindowActionDelegate，然后在run（）方法中添加實(shí)現(xiàn)打開配置對話框的代碼。

然后，需要定義兩個(gè)視圖，一個(gè)用于管理配置需要驗(yàn)證的文件，另一個(gè)用來顯示驗(yàn)證的結(jié)果。作為view的擴(kuò)展，它必須繼承ViewPart類，將它們分別命名為OutputView和TopicView。讓他們重載父類的createPartControl（）方法，來設(shè)計(jì)各自的面板內(nèi)容。在OutputView中，設(shè)計(jì)一個(gè)列表來顯示線程選擇信息，當(dāng)用戶點(diǎn)擊某個(gè)線程時(shí)，在右邊顯示線程檢測的詳細(xì)信息，為了實(shí)現(xiàn)此功能，讓OutputView類實(shí)現(xiàn)JFace的一個(gè)視圖UI接口ISelectionChangedListener。

添加一個(gè)右鍵菜單項(xiàng)，新建兩個(gè)類JavaClass LaunchAction和RunJpfAction，實(shí)現(xiàn)接口IObjectActionDelegate。在JavaClassLaunchAction的run（）方法中使用IProject和IFile來為class文件創(chuàng)建配置文件，并初始化配置文件的內(nèi)容。在RunJpfAction的run（）方法中調(diào)用JPF來完成指定文件的檢測工作。

圖4 配置面板

3.3 編輯plugin.xml文件

PDE為插件清單文件plugin.xml提供了專門的插件清單編輯器。PDE中的插件編輯器為多頁編輯器，其中包括概述、依賴項(xiàng)、運(yùn)行時(shí)、擴(kuò)展、擴(kuò)展點(diǎn)、編譯、MANIFEST.MF、plugin. xml和build.properties等，可在每個(gè)配置頁面中為其定制相關(guān)的屬性。為每一個(gè)擴(kuò)展點(diǎn)添加一個(gè)＜extension＞節(jié)點(diǎn)，然后在子節(jié)點(diǎn)中配置擴(kuò)展點(diǎn)的id、實(shí)現(xiàn)類的路徑、名稱、圖標(biāo)、標(biāo)簽文字等擴(kuò)展點(diǎn)屬性。

調(diào)用JPF來執(zhí)行檢測功能，需要設(shè)計(jì)一個(gè)專門的類來完成此項(xiàng)工作。新建一個(gè)類VerifyJob，繼承Eclipse的核心類Job，該類包含4個(gè)主要屬性：IFile變量來存儲配置文件信息，Config變量來自JPF的配置類，布爾型變量step指示是否單步執(zhí)行，PrintStream變量用于輸出。根據(jù)默認(rèn)的配置文件和用戶自定義的配置文件，生成JPF的Config對象，然后在VerifyJob的run（）方法中使用Config對象構(gòu)造一個(gè)JPF對象，最后執(zhí)行JPF的run（）方法。自定義一個(gè)監(jiān)聽器，用于檢測并輸出JPF的檢測結(jié)果，然后通過調(diào)用JPF的addSearchListener（）和addVMListener（）方法，將該監(jiān)聽器添加到當(dāng)前的JPF對象中去。

3.4 插件測試、打包與發(fā)布

PDE提供了很方面的測試、調(diào)試手段。每添加一次代碼，就可以通過在插件項(xiàng)目上點(diǎn)擊鼠標(biāo)右鍵，選擇”Run As Eclipse Application”來測試新插件的功能效果。當(dāng)然，最終的測試，需要將打包發(fā)行后的插件安裝到Eclipse中來觀察插件的工作情況。

插件項(xiàng)目在打包時(shí)，僅將src源文件對應(yīng)的編譯文件打成一個(gè)jar包。其它文件如xml、圖像文件等都需要手工復(fù)制到打包目錄下?？墒褂肊clipse導(dǎo)出功能，或Ant來打包插件。

Eclipse還可以通過新建一個(gè)Update Site項(xiàng)目的方法，將新的插件以網(wǎng)頁的形式發(fā)布出去。利用建立Update Site項(xiàng)目向?qū)?，最終會形成一個(gè)web目錄，該目錄下包含了你要發(fā)布的plugins和features文件夾，另外還有一個(gè)site.xml文件和一個(gè)index.html文件。site.xml中定義了改更新站點(diǎn)可以提供的插件的下載路徑，這樣用戶可以通過Eclipse的UpdateManager來在線安裝插件。

4 實(shí)例應(yīng)用分析

為測試JPF的死鎖檢測功能，首先創(chuàng)建一個(gè)存在死鎖問題的Java類Deadlock，該類實(shí)現(xiàn)Runnable接口，在mian（）函數(shù)中啟動兩個(gè)Deadlock對象，并用synchronized控制對象本身的訪問。考慮這樣一種情況：1）線程T1在對象t1上同步，然后調(diào)用對象t2的foo方法，允許被搶先執(zhí)行。2）另一個(gè)線程T2開始執(zhí)行，在對性t2上同步。3）T2獲得t2，繼續(xù)執(zhí)行，企圖獲得t1，調(diào)用t1的foo方法。但獲取失敗，因?yàn)門1占有t1。于是，T2阻塞，等待T1釋放t1。4）輪到T1繼續(xù)執(zhí)行，T1試圖獲得t2，但不能成功，因?yàn)閠2已經(jīng)被T2占有了。至此，T1和T2都被阻塞，程序死鎖。配置JPF，實(shí)現(xiàn)死鎖檢測。

在運(yùn)行Deadlock類后，由于配置了NotDeadlockedProperty屬性，JPF可以很快發(fā)現(xiàn)程序中的死鎖問題，并輸出導(dǎo)致死鎖的程序執(zhí)行路徑。JPF的出現(xiàn)，為Java程序模型檢測注入了新的力量，它在許多方面都得到了實(shí)際應(yīng)用，包括航天軟件的研制、實(shí)時(shí)系統(tǒng)驗(yàn)證和網(wǎng)絡(luò)協(xié)議驗(yàn)證[等。Eclipse是Java程序員比較常用的一種Java編輯工具，利用JPF在其基礎(chǔ)上開發(fā)一款Java模型檢測工具是非常有意義的，可以使得程序員在編寫程序的同時(shí)檢測程序代碼的邏輯正確性。

[1]楊明遠(yuǎn),羅貴明.一種大規(guī)模并行程序模型的檢測方法[J].計(jì)算機(jī)工程,2008,34,（13）：72-74.

[2]鐘誠,唐春艷.運(yùn)用類復(fù)制變異和JPF技術(shù)生成類間測試用例[J].小型微型計(jì)算機(jī)系統(tǒng),2009,30,（8）.