一種FTCSP的服務組合時間建模與分析方法

，，

(新疆電子研究所股份有限公司，烏魯木齊 830013)

引 言

進程代數(shù)作為一種形式化建模語言，具有以自然的方式對并發(fā)和組合系統(tǒng)進行建模的優(yōu)勢，已得到廣泛關注研究[1-4]。而如何擴展進程代數(shù)使其支持服務組合不確定性時間信息的表達和推理，對于增強進程代數(shù)功能、豐富服務組合形式化建模理論具有重要意義[5]。本文基于可能性理論[6]提出了一種擴展模糊時間的通信順序進程(Fuzzy Time Communication Sequential Processes，F(xiàn)TCSP)，并以FTCSP為基礎，提出了一種支持服務組合不確定時間建模與分析的方法，給出了有利于服務組合模糊時間的分析算法。最后以地下空間環(huán)境信息實時發(fā)布系統(tǒng)為例(Undergroundspace Environment Information Real-time publishing System， UEIRS)，給出了服務組合不確定時間建模與分析的具體過程，驗證了該方法的有效性。

1 服務組合及其進程代數(shù)的建模方法

面向服務的體系結構(Service Oriented Architecture，SOA)將系統(tǒng)所有的功能都定義為獨立的服務，由于單個的服務功能單一，不能提供完整的解決方案，為了實現(xiàn)更加復雜的業(yè)務邏輯，可以組合較小的、易于執(zhí)行的輕量級服務來創(chuàng)建隨需而變的服務。服務組合問題的本質(zhì)就是解決內(nèi)部各個服務之間的協(xié)作。為了實現(xiàn)服務組合的正確性、服務的連接性、服務質(zhì)量的可滿足性等應用需求，需要在系統(tǒng)設計開發(fā)階段對服務組合建模，提高軟件系統(tǒng)的安全性與可靠性。

形式化方法基于形式化理論和模型對服務組合進行描述和推理，是保證服務組合系統(tǒng)正確性及提高安全性和可靠性的重要手段。因此，利用形式化方法(如進程代數(shù)、Petri網(wǎng)、自動機理論等)來描述和驗證服務組合，成為服務組合建模方法的研究熱點。進程代數(shù)適合描述并發(fā)和組合系統(tǒng)，而服務組合的一個顯著特點就是服務之間的并發(fā)和組合，因此，本文專注于進程代數(shù)在服務組合建模中的應用。通過分析總結基于進程代數(shù)的服務組合形式化相關研究，見參考文獻[3]，得到如圖1所示的建模流程。建模主要分為開發(fā)設計和反向運行測試兩個階段。圖1中編號①和②的含義解釋如下:

圖1 基于進程代數(shù)的服務組合形式化建模流程

①開發(fā)設計階段:首先對服務組合抽象流程及其規(guī)約基于進程代數(shù)進行形式化建模，利用進程代數(shù)知識推理及驗證工具對服務組合抽象流程進行功能驗證，如死鎖和活性檢查；然后在進程代數(shù)各個算子與服務組合執(zhí)行語言之間建立映射關系，基于可信模型自動生成程序代碼框架，協(xié)助服務組合系統(tǒng)的具體開發(fā)實現(xiàn)。

②反向運行測試階段:建立正在運行的服務組合業(yè)務流程到進程代數(shù)的映射，借助進程代數(shù)推理性質(zhì)和工具驗證其功能和非功能屬性，達到分析、測試服務組合的目的。

本文在此原則的基礎上展開，首先定義了FTCSP的語義及語法，然后提出了服務組合時間建模與分析方法，最后對該方法進行了評估驗證，得出結論。

2 FTCSP的語義及語法定義

本節(jié)針對現(xiàn)有的進程代數(shù)在系統(tǒng)不確定時間問題建模上力不從心，對TCSP進行了擴展，并依據(jù)Zadeh在1978年提出的可能性理論[6]作為處理不確定信息的一種方法，采用梯形模糊時間區(qū)間表示不確定性時間[7-8]，最終定義了支持不確定時間建模的FTCSP 的進程代數(shù)定義如下：

P::=STOP|SKIP|WAIT fdt|(a,fet)

(1)

式(1)的進程表達式解釋如下:

WAIT fdt表示進程的等待， fdt代表一個模糊延遲時間(FTS)，t1,t2,t3,t4∈R+，定義如下:

STOP、PA、SKIP、：μX?F(X)、P[R]、c!v→P、c?v→P與經(jīng)典CSP一致，在此不再贅述。

在標記遷移系統(tǒng)表示的CSP和時間遷移系統(tǒng)定義的TCSP的基礎上，定義了FTCSP的時間遷移系統(tǒng)[9-10]。

該語義模型表明FTCSP可以被描述為一個時間遷移序列，表示進程所有可能的行為遷移、執(zhí)行操作過程。鑒于形式化語義的操作語義方法通過語言的執(zhí)行與實施進而直觀、簡捷地顯示語言成分的含義[9-11]，我們在Schneider.S[10]定義TCSP操作語義的基礎上，定義了FTCSP算子的結構化操作語義，通過結構化操作語義可以計算出進程的執(zhí)行時間，進而可以分析服務組合時間模型，對時間規(guī)約等性質(zhì)進行驗證，得出FTCSP擴充了TCSP不確定時間的建模能力[12]。

3 基于FTCSP的服務組合時間建模與分析方法

基于上一節(jié)提出的FTCSP，提出了一種支持服務組合時間建模與分析的方法，具體流程如圖2所示，方法主要分為建模與分析兩大步。

圖2 服務組合時間建模和分析的方法流程

3.1 基于FTCSP的服務組合時間建模方法

基于FTCSP的服務組合時間建模方法，首先根據(jù)表1將抽象服務組合流程轉換成UML活動圖，為了體現(xiàn)服務組合的不確定時間信息，在每個活動節(jié)點加Sfet(單個服務執(zhí)行一個完整任務的模糊時間，可表示為[et1，et2，et3，et4])，在數(shù)據(jù)流中添加Smtt(每個交互消息從發(fā)送到接收的服務消息模糊傳輸時間，可表示為[tt1，tt2，tt3，tt4] )，以上兩者的取值由設計開發(fā)者通過主觀經(jīng)驗獲得。然后根據(jù)表2將UML活動圖轉換成FTCSP模型，不僅可以借助CSP的自動驗證工具FDR2[13]對服務組合進行功能分析和驗證，而且可以分析服務組合的時間特性。

表1 UML活動圖的轉換規(guī)則

通過將服務組合中的單個服務映射到FTCSP時間模型，使用并發(fā)組合算子來表示整個抽象服務組合流程，服務組合的FTCSP進程表達式如下所示：S1,S2,...,Sn表示UML活動圖中的每個活動

i∈R+,T,Ti∈FTS,Ai∈S∑

(2)

表2 FTCSP模型的轉換規(guī)則

3.2 基于FTCSP服務組合時間模型的分析方法

假設進程P獨自的模糊執(zhí)行時間為Pt=[p1,p2,p3,p4]，進程Q獨自的模糊執(zhí)行時間為Qt=[q1,q2,q3,q4]。以此為例給出了FTCSP三種組合算子的模糊時間運算規(guī)則，順序組合算子(;)定義為進程P和Q的模糊時間的和(⊕)運算；選擇組合算子：W外部選擇定義為執(zhí)行的第一個事件，∩內(nèi)部選擇具有不確定性，由內(nèi)部事件決定(最大或最小執(zhí)行時間)；并發(fā)組合算子(‖)定義為P和Q并發(fā)的最長進程時間；運算法則的證明詳細請參見參考文獻[6]。

以標準化的FTCSP模型作為輸入條件，通過FTCSP三種組合算子的模糊時間運算規(guī)則得到每個服務的模糊執(zhí)行時間，最后再根據(jù)規(guī)則多服務組合便可得到整個服務組合流程的模糊執(zhí)行時間。下面給出了基于FTCSP標準化模型的時間分析算法流程。

算法運行指令基于FTCSP服務組合時間模型的時間分析算法。

Output: FT， fuzzy execution time of abstract services composition process。/執(zhí)行時間/

3.WHILE i

4.AnalyzingOperator(S[i]， rule 2， rule 3， rule 4， St[i])；//St[i] represent output of the function

5.i=i+1；}

6.WHILE (j+1)

7.Concurrent max (St[j],St[j+1])；// rule 4

8.St[j+1]=Concurrent max(St[j],St[j+1])；//rule 4

9.j=j+1；}

10.Return FT= St[j]。

4 方法評估

UEIRS主要功能是將傳感器采集到的地下空間內(nèi)部的環(huán)境信息實時發(fā)送到各區(qū)域嵌入式控制器并顯示給用戶。該服務系統(tǒng)主要由6個子服務組成，為了保證UEIRS軟件服務的正常運行以及系統(tǒng)時間的嚴格受限性，不僅需要驗證UEIRS服務組合功能的正確性，而且還要滿足服務組合時間上的規(guī)約。本節(jié)以UEIRS為例來評估本文提出的服務組合不確定時間建模方法。UEIRS擴展模糊時間的UML活動圖如圖3所示。

圖3 UEIRS擴展模糊時間的UML活動圖

假設環(huán)境信息發(fā)布系統(tǒng)開始時間區(qū)間為[0，0，0，0]。最終得出抽象服務組合流程成功執(zhí)行一次的模糊時間如下:

Tstasanfang=T3=[1.4,2.1,2.7,3.65]

依據(jù)本文提出的基于FTCSP計算得到的服務組合執(zhí)行時間Tstasanfang代表UEIRS從啟動到客戶端成功連接并第一次顯示來自上位機組態(tài)數(shù)據(jù)庫中的UEIRS信息所使用的模糊時間，從得到的模糊時間數(shù)據(jù)來看，服務組合成功執(zhí)行最有可能發(fā)生在[2.1,2.7]時間區(qū)間，最長執(zhí)行時間為3.65個單位時間，最短執(zhí)行時間為1.4個單位時間。同時利用模糊時間還可以計算UEIRS信息發(fā)布服務組合在某一時間點成功執(zhí)行的可能性(概率)，如用戶要求在1.8個單位時間內(nèi)完成上述任務的可能性約等于0.57，若要求在2.3時間內(nèi)完成上述任務，則可能性為1，即在模糊時間確定發(fā)生的區(qū)間內(nèi)。通過對UEIRS服務組合系統(tǒng)不確定時間的實例建模與分析，可知本文提出的服務組合時間建模方法解決不確定性時間建模問題是可行且有效的。

結 語

[1] 祝義,黃志球,周航,等.基于進程代數(shù)規(guī)約生成軟件體系結構模型的方法[J].計算機研究與發(fā)展,2011(2):241-250.

[2] 楊進,張小彬,嚴博,等.基于進程代數(shù)的系統(tǒng)性能評價方法綜述[J].軟件導刊,2015(2):25-27.

[3] 肖芳雄,李燕,黃志球,等.基于時間概率代價進程代數(shù)的Web服務組合建模與分析[J].計算機學報,2012,35(5):918-936.

[4] MA Z M,ZHENG F,YAN L,et al.Repre- senting and reasoning on fuzzy UML models: a description logic approach[J].Expert Systems With Applications,2011,38 (3):2536-2549.

[5] 羅軍舟,金嘉暉,宋愛波,等.云計算:體系架構與關鍵技術[J].通信學報,2011(7):3-21.

[6] Negoita C V,Zadeh L A,Zimmermann H J.Fuzzy sets as a basis for a theory of possibility[J].Fuzzy Sets and Systems,1978(1):3-28.

[7] 齊美石.基于模糊Petri網(wǎng)的兩階段服務組合研究[D].合肥:中國科學技術大學,2011:15-17.

[8] 倪夏靜,李仁旺,王赟,等.基于Petri網(wǎng)的不確定時間工作流成本分析[J].浙江理工大學學報,2013(2):232-236.

[9] 張淼.基于TCSP的區(qū)域控制器分層建模與驗證[D].北京:北京交通大學,2015:35-47.

[10] Schneider S A.An Operational Semantics for Timed CSP[J].Information and Computation,1995,116(2):193-213.

[11] 周巢塵.形式語義學引論操作語義學[J].計算機研究與發(fā)展,1985(7):1-11.

[12] Davies J,Schneider S.A brief history of Timed CSP[J].Theoretical Computer Science,1995,138(2):243-271.

[13] 祝義,肖芳雄,周航,等.一種嵌入式實時系統(tǒng)軟件能耗建模與分析的方法[J].計算機研究與發(fā)展,2014(4):848-855.

[14] Security Analysis of an Electronic Commerce Protocol Using Casper/FDR2[J].Wuhan University Journal of Natural Sciences,2012(6):499-503.

[15] 李永湘,姚錫凡,徐川,等.基于擴展進程代數(shù)的云制造服務組合建模與QoS評價[J].計算機集成制造系統(tǒng),2014(3):689-700.

[16] 沈華.Web服務組合形式化性能分析方法簡述[J].教育教學論壇,2016(42):71-72.