RGPS服務層元模型正確性驗證

張莉+楊淑貞+楊浩

摘 要：隨著網(wǎng)絡式軟件復雜程度的日益增加，如何確保網(wǎng)絡式軟件功能和性能的正確性越發(fā)重要。根據(jù)網(wǎng)絡式軟件的特點，在RGPS需求元建?？蚣艿闹笇拢岢鯮GPS服務層元模型正確性驗證。首先用BPEL語言和WSDL語言把RGPS服務層元模型描述成BPEL模型，再用Promela語言實現(xiàn)BPEL模型的建模，最后輸入LTL公式對RGPS服務層元模型進行安全性和活性驗證分析。以城市交通出行系統(tǒng)為例，采用RGPS需求元模型為框架，構建城市交通出行系統(tǒng)服務層元模型。

關鍵詞：網(wǎng)絡式軟件；BPEL；Promela；LTL公式；正確性驗證

DOIDOI：10.11907/rjdk.162588

中圖分類號：TP306

文獻標識碼：A文章編號：1672-7800（2016）012-0008-03

0 引言

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

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

本文首先采用BPEL語言和WSDL語言把RGPS服務層元模型描述成BPEL模型，再對BPEL模型進行Promela語言建模，最后對RGPS服務層元模型進行驗證分析。

1 RGPS服務層元模型的BPEL模型

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

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

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

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

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

part="TavelTypeInfo"/>

portType="tns：TavelPT"

operation="requestTavel"

inputVariable="TavelRequest">

outputVariable="TavelInfo">

operation="sendTavel"

variable="DateInfo"/>

2 BPEL模型的Promela語言建模

Promela語言一種形式化語言，實現(xiàn)了對有限狀態(tài)系統(tǒng)的建模。Promela描述的行為通過通道實現(xiàn)進程間通信和數(shù)據(jù)交換。一般來說，Promela模型由類型、通道、變量和進程構成。Promela語言主要有數(shù)據(jù)類型、進程、消息傳遞、控制流、語句類型。通過用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 正確性驗證

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

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

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

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

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

驗證結果顯示沒有錯誤發(fā)生，表明此公式成立。

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

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

驗證結果顯示有錯誤發(fā)生，表明此公式成立。

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

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

驗證結果顯示沒有錯誤發(fā)生，表明此公式成立。

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

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

驗證結果顯示有錯誤發(fā)生，表明此公式成立。

4 結語

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

參考文獻：

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

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

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

[4] 林惠民，張文輝.模型檢測：理論、方法與應用[J].電子學報，2002，30（12A）：1907-1912.

[5] 駱翔宇，譚征，蘇開樂，吳立軍.一種基于認知模型檢測的Web服務組合驗證方法[J].計算機學報，2011，34（6）：1041-1061

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

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

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

（責任編輯：陳福時）