，，

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

引 言

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

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

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

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

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

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

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

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

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的基礎(chǔ)上，定義了FTCSP的時間遷移系統(tǒng)[9-10]。

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

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

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

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

3.1 基于FTCSP的服務(wù)組合時間建模方法

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

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

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

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

(2)

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

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

假設(shè)進程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ī)則得到每個服務(wù)的模糊執(zhí)行時間，最后再根據(jù)規(guī)則多服務(wù)組合便可得到整個服務(wù)組合流程的模糊執(zhí)行時間。下面給出了基于FTCSP標準化模型的時間分析算法流程。

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

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ū)域嵌入式控制器并顯示給用戶。該服務(wù)系統(tǒng)主要由6個子服務(wù)組成，為了保證UEIRS軟件服務(wù)的正常運行以及系統(tǒng)時間的嚴格受限性，不僅需要驗證UEIRS服務(wù)組合功能的正確性，而且還要滿足服務(wù)組合時間上的規(guī)約。本節(jié)以UEIRS為例來評估本文提出的服務(wù)組合不確定時間建模方法。UEIRS擴展模糊時間的UML活動圖如圖3所示。

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

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

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

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

結(jié) 語

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

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

[3] 肖芳雄,李燕,黃志球,等.基于時間概率代價進程代數(shù)的Web服務(wù)組合建模與分析[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] 羅軍舟,金嘉暉,宋愛波,等.云計算:體系架構(gòu)與關(guān)鍵技術(shù)[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)的兩階段服務(wù)組合研究[D].合肥:中國科學技術(shù)大學,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ù)的云制造服務(wù)組合建模與QoS評價[J].計算機集成制造系統(tǒng),2014(3):689-700.

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