張莉+楊淑貞+楊浩

摘 要：隨著網(wǎng)絡(luò)式軟件復(fù)雜程度的日益增加，如何確保網(wǎng)絡(luò)式軟件功能和性能的正確性越發(fā)重要。根據(jù)網(wǎng)絡(luò)式軟件的特點(diǎn)，在RGPS需求元建模框架的指導(dǎo)下，提出RGPS服務(wù)層元模型正確性驗(yàn)證。首先用BPEL語言和WSDL語言把RGPS服務(wù)層元模型描述成BPEL模型，再用Promela語言實(shí)現(xiàn)BPEL模型的建模，最后輸入LTL公式對(duì)RGPS服務(wù)層元模型進(jìn)行安全性和活性驗(yàn)證分析。以城市交通出行系統(tǒng)為例，采用RGPS需求元模型為框架，構(gòu)建城市交通出行系統(tǒng)服務(wù)層元模型。

關(guān)鍵詞：網(wǎng)絡(luò)式軟件；BPEL；Promela；LTL公式；正確性驗(yàn)證

DOIDOI：10.11907/rjdk.162588

中圖分類號(hào)：TP306

文獻(xiàn)標(biāo)識(shí)碼：A文章編號(hào)：1672-7800（2016）012-0008-03

0 引言

隨著計(jì)算機(jī)網(wǎng)絡(luò)的迅速發(fā)展，計(jì)算機(jī)軟件也朝著網(wǎng)絡(luò)化、服務(wù)化方向轉(zhuǎn)變，網(wǎng)絡(luò)式軟件[1-3]就是在這種形勢(shì)下產(chǎn)生的一種復(fù)雜軟件系統(tǒng)。網(wǎng)絡(luò)式軟件將網(wǎng)絡(luò)資源聚合部署到網(wǎng)絡(luò)上，為用戶提供隨個(gè)人需求而變化的在線服務(wù)。RGPS需求元模型框架是一種由分層與合作問題組成的框架，它涵蓋了網(wǎng)絡(luò)式軟件描述中所需的角色、目標(biāo)、流程和服務(wù)4個(gè)基本要素，由角色層元模型、目標(biāo)層元模型、過程層元模型和服務(wù)層元模型以及各層之間相互關(guān)系組成。角色層元模型定義了需求方和需求方的社會(huì)屬性、所需要承擔(dān)的角色、所屬的組織、規(guī)則以及相互之間的關(guān)系。目標(biāo)層元模型將需求目標(biāo)進(jìn)行分類，確定各個(gè)目標(biāo)之間的分解和約束關(guān)系。過程層元模型描述需求過程的各個(gè)組成部分，包括過程的輸入、輸出、前置條件、后置條件、組合過程中子流程之間的控制結(jié)構(gòu)等。服務(wù)層元模型描述了服務(wù)信息以及它們的相互關(guān)系，用來指導(dǎo)服務(wù)鏈的構(gòu)造及其所需服務(wù)資源的管理。

模型檢測(cè)技術(shù)[4-6]是一種很重要的形式化驗(yàn)證分析技術(shù)。它最早由Clarke和Emerson于1981年提出，能通過顯式的狀態(tài)搜索或隱式不動(dòng)點(diǎn)計(jì)算來驗(yàn)證系統(tǒng)是否滿足某種屬性或者實(shí)現(xiàn)某個(gè)功能。有形枚舉的模型檢測(cè)方法通過對(duì)狀態(tài)的搜索遍歷，找到所有的可達(dá)集，再檢查可達(dá)集中是否存在錯(cuò)誤狀態(tài)。如果存在錯(cuò)誤狀態(tài)，那么說明系統(tǒng)不安全，否則說明系統(tǒng)是安全的。SPIN是一種常見的有形枚舉的模型檢測(cè)工具。

本文首先采用BPEL語言和WSDL語言把RGPS服務(wù)層元模型描述成BPEL模型，再對(duì)BPEL模型進(jìn)行Promela語言建模，最后對(duì)RGPS服務(wù)層元模型進(jìn)行驗(yàn)證分析。

1 RGPS服務(wù)層元模型的BPEL模型

服務(wù)可以分為原子服務(wù)和組合服務(wù)兩種。組合服務(wù)是原子服務(wù)按照一定的過程控制結(jié)構(gòu)組合編排而成。消息和操作是服務(wù)的兩個(gè)基本要素。消息是服務(wù)所需的數(shù)據(jù)，分為輸入消息和輸出消息。操作分為前置條件和效果。服務(wù)描述分為功能性描述和非功能性描述。功能性描述介紹服務(wù)的主要業(yè)務(wù)。非功能性描述分為質(zhì)量屬性和情境屬性，包括時(shí)間、費(fèi)用和可維護(hù)性等。

BPEL是業(yè)務(wù)流程執(zhí)行語言，用于描述業(yè)務(wù)流程的結(jié)構(gòu)，調(diào)用網(wǎng)絡(luò)服務(wù)，進(jìn)行流程中數(shù)據(jù)的定義和傳遞。WSDL是網(wǎng)絡(luò)服務(wù)描述語言，BPEL定義的流程都要通過WSDL來實(shí)現(xiàn)，并且被調(diào)用的網(wǎng)絡(luò)服務(wù)也是用WSDL描述的。

隨著城市交通系統(tǒng)的發(fā)展，城市交通系統(tǒng)網(wǎng)絡(luò)也變得愈加復(fù)雜。本文以城市交通出行系統(tǒng)為例子，采用RGPS需求元模型為框架，構(gòu)建城市交通出行系統(tǒng)服務(wù)層元模型。

圖1中，當(dāng)收到出行者的查詢動(dòng)作后，流程初始化3個(gè)并行的任務(wù)：計(jì)算出行價(jià)格、選擇車次和路線以及為出行安排日期。雖然有些處理可以并行進(jìn)行，但是3個(gè)任務(wù)之間存在相互依賴的控制和數(shù)據(jù)。具體地說，在計(jì)算最終價(jià)格時(shí)需要車次和路線信息，在全面安排實(shí)現(xiàn)計(jì)劃時(shí)需要出行日期。在完成這3個(gè)任務(wù)后就可以將出行計(jì)劃交給出行者。

用BPEL描述該服務(wù)層模型的部分代碼為：

part="TavelTypeInfo"/>

portType="tns：TavelPT"

operation="requestTavel"

inputVariable="TavelRequest">

outputVariable="TavelInfo">

operation="sendTavel"

variable="DateInfo"/>

2 BPEL模型的Promela語言建模

Promela語言一種形式化語言，實(shí)現(xiàn)了對(duì)有限狀態(tài)系統(tǒng)的建模。Promela描述的行為通過通道實(shí)現(xiàn)進(jìn)程間通信和數(shù)據(jù)交換。一般來說，Promela模型由類型、通道、變量和進(jìn)程構(gòu)成。Promela語言主要有數(shù)據(jù)類型、進(jìn)程、消息傳遞、控制流、語句類型。通過用JAVA編寫程序代碼，得到BPEL模型的Promela語言建模主程序代碼：

if （e.getSource（） == menuItembpel2）

{

final String testBpelFile =bpelfileName；

final String testWsdlFile = wsdlfileName；

final String inputStreamFile = promelafileName；

try {

TestTranslator.translator（testBpelFile，testWsdlFile，new PrintStream（inputStreamFile））；

promelafile = new File（inputStreamFile）；

editorArea.setText（editor.readFile（promelafile））；

}catch （FileNotFoundException e1） {

// TODO Auto-generated catch block

e1.printStackTrace（）；

} catch （IOException e2） {

// TODO Auto-generated catch block

e2.printStackTrace（）；

}

城市交通出行系統(tǒng)的Promela語言部分代碼為：

typedef T_BPEL_lc_basic {

byte state = BPEL_lc_basic_state_not_started；

}；

typedef T_BPEL_lc{

byte state = BPEL_lc_state_not_started；

bit fault = BPEL_lc_fault_none；

bit fault_handler = BPEL_lc_fault_handler_none；

}；

typedef T_BPEL_lnk {

bool evaluated = 0；

bool evaluation = 0；

}；

3 正確性驗(yàn)證

BPEL模型經(jīng)過Promela語言建模之后，需要在SPIN工具輸入LTL公式進(jìn)行正確性驗(yàn)證，而正確性驗(yàn)證又分為安全性驗(yàn)證和活性驗(yàn)證。

SPIN工具是由美國(guó)貝爾實(shí)驗(yàn)室開發(fā)的用來驗(yàn)證大規(guī)模復(fù)雜軟件系統(tǒng)的形式化驗(yàn)證工具。SPIN工具以Promela語言作為輸入語言，使用on-the-fly技術(shù)，可以看作一個(gè)完整的LTL模型檢測(cè)系統(tǒng)，里面有多項(xiàng)可供選擇的優(yōu)化技術(shù)。LTL公式即線性時(shí)序邏輯公式，LTL包括&&，！，―>，‖等連接符和□，◇，○等時(shí)序算子?！鮬表示p永遠(yuǎn)為真，◇p表示p在未來某一時(shí)刻為真，○p表示在下一時(shí)刻為真，pq表示p一直為真直到q為真。安全性是指壞的事情永遠(yuǎn)不會(huì)發(fā)生，活性是指好的事情最終會(huì)發(fā)生。

本文開發(fā)出了RGPS服務(wù)層元模型正確性驗(yàn)證工具，該工具用Java語言編程實(shí)現(xiàn)。用戶首先用BPEL語言把RGPS服務(wù)層元模型例子給描述出來，再通過編寫代碼實(shí)現(xiàn)BPEL語言和Promela語言之間的轉(zhuǎn)換生成Promela語言建模，接著用LTL公式描述模型的性質(zhì)，最后進(jìn)行SPIN驗(yàn)證返回檢測(cè)結(jié)果。

LTL公式！[]（p1->！p2）的意思是由初始價(jià)格得不到最終價(jià)格的情況不會(huì)發(fā)生。輸入LTL公式！[]（p1->！p2）進(jìn)行安全性驗(yàn)證得到如下結(jié)果：

Full statespace search for：

never claim –

assertion violations +（if within scope of claim）

cycle checks-（disabled by –DSAFETY）

invalid end states +（disabled by never claim）

State-vector 121 byte， depth reached 142， errors： 0

驗(yàn)證結(jié)果顯示沒有錯(cuò)誤發(fā)生，表明此公式成立。

LTL公式[]p的意思是無論什么情況下，系統(tǒng)都沒有壞的事情發(fā)生。輸入LTL公式[]p進(jìn)行安全性驗(yàn)證得到如下結(jié)果：

Full statespace search for：

never claim –

assertion violations +（if within scope of claim）

cycle checks –（disabled by –DSAFETY）

invalid end states –（disabled by never claim）

State-vector38 byte， depth reached 172， errors： 1

驗(yàn)證結(jié)果顯示有錯(cuò)誤發(fā)生，表明此公式成立。

LTL公式[]（p1&&t1-><>p2）的意思是由初始價(jià)格和乘車信息就一定能得到最終價(jià)格。輸入LTL公式[]（p1&&t1-><>p2）進(jìn)行活性驗(yàn)證得到如下結(jié)果：

Full statespace search for：

never claim –

assertion violations +（if within scope of claim）

acceptance cycles –（fairness enabled）

invalid end states +（disabled by never claim）

State-vector 55 byte， depth reached 138， errors： 0

驗(yàn)證結(jié)果顯示沒有錯(cuò)誤發(fā)生，表明此公式成立。

LTL公式[]<>p&&[]<>w的意思是在乘車信息未知的情況下能得到票價(jià)或者出行日期。輸入LTL公式[]<>p&&[]<>w進(jìn)行活性驗(yàn)證得到如下結(jié)果：

Full statespace search for：

never claim –

assertion violations +（if within scope of claim）

acceptance cycles –（fairness enabled）

invalid end states –（disabled by never claim）

State-vector 97 byte， depth reached 122， errors： 1

驗(yàn)證結(jié)果顯示有錯(cuò)誤發(fā)生，表明此公式成立。

4 結(jié)語

隨著Internet技術(shù)的發(fā)展和軟件生成運(yùn)行環(huán)境的變化，網(wǎng)絡(luò)式軟件成為基于互聯(lián)網(wǎng)環(huán)境的新生軟件形態(tài)。為了克服網(wǎng)絡(luò)式軟件復(fù)雜度過高和緩解模型檢測(cè)所引發(fā)的空間狀態(tài)爆炸問題，本文研究了基于Promela模型組合與抽象的分析方法對(duì)RGPS服務(wù)層元模型進(jìn)行正確性驗(yàn)證。RGPS服務(wù)層元模型正確性驗(yàn)證采用技術(shù)研究與工具開發(fā)相結(jié)合的方式。一方面，對(duì)核心技術(shù)進(jìn)行長(zhǎng)期系統(tǒng)深入研究，特別是實(shí)現(xiàn)BPEL/WSDL語言轉(zhuǎn)換到Promela語言， 并結(jié)合LTL公式性質(zhì)進(jìn)行安全性和活性驗(yàn)證；另一方面，將理論研究上的突破轉(zhuǎn)化到實(shí)踐開發(fā)工具中，順應(yīng)國(guó)內(nèi)外軟件驗(yàn)證需求的潮流。

參考文獻(xiàn)：

[1] 胡博，何克清，陳華峰.基于RGPS的網(wǎng)絡(luò)式軟件需求獲取與分析方法[J].微計(jì)算機(jī)信息，2010，26（2）：6-8.

[2] 趙新輝，袁開銀，吳盡昭.網(wǎng)絡(luò)式軟件非功能需求沖突消解[J].計(jì)算機(jī)工程，2012，38（18）：37-41.

[3] 張婷.網(wǎng)絡(luò)式軟件非功能需求分析方法及其應(yīng)用[J].信息與電腦，2014，06：160-161.

[4] 林惠民，張文輝.模型檢測(cè)：理論、方法與應(yīng)用[J].電子學(xué)報(bào)，2002，30（12A）：1907-1912.

[5] 駱翔宇，譚征，蘇開樂，吳立軍.一種基于認(rèn)知模型檢測(cè)的Web服務(wù)組合驗(yàn)證方法[J].計(jì)算機(jī)學(xué)報(bào)，2011，34（6）：1041-1061

[6] 文中華，黃巍，劉任任，姜云飛.模型檢測(cè)規(guī)劃中的狀態(tài)分層方法[J].軟件學(xué)報(bào)，2009，20（4）：858-869.

[7] 張曼，段振華，王小兵.BPEL流程建模中的交疊模式分析與轉(zhuǎn)換[J].軟件學(xué)報(bào)，2011，22（11）：2684-2697.

[8] 張文博，史維峰.基于BPEL和QoS的動(dòng)態(tài)Web服務(wù)組合框架研究[J].計(jì)算機(jī)技術(shù)與發(fā)展，2009，19（11）：72-75.

（責(zé)任編輯：陳福時(shí)）