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

，，

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

引 言

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

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

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

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

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

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

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

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

2 FTCSP的語義及語法定義

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

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與經典CSP一致，在此不再贅述。

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

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

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

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

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

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

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

表1 UML活動圖的轉換規則

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

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

(2)

表2 FTCSP模型的轉換規則

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

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

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

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

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

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

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

假設環境信息發布系統開始時間區間為[0，0，0，0]。最終得出抽象服務組合流程成功執行一次的模糊時間如下:

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

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

結 語

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

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

[3] 肖芳雄,李燕,黃志球,等.基于時間概率代價進程代數的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網的兩階段服務組合研究[D].合肥:中國科學技術大學,2011:15-17.

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

[9] 張淼.基于TCSP的區域控制器分層建模與驗證[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].計算機研究與發展,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] 祝義,肖芳雄,周航,等.一種嵌入式實時系統軟件能耗建模與分析的方法[J].計算機研究與發展,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] 李永湘,姚錫凡,徐川,等.基于擴展進程代數的云制造服務組合建模與QoS評價[J].計算機集成制造系統,2014(3):689-700.

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