Web服務組合形式化性能分析方法簡述

沈華

摘要：Web服務組合是若干子服務按照一定的業務流程構成的復合服務。為了保證這個復合服務能夠達到客戶的預期目標，在將其正式投入運行之前，需要對其進行結構驗證和性能分析。基于數學的形式化方法是對Web服務組合進行性能分析的一種有效途徑。本文介紹了幾種常用的形式化方法。

關鍵詞：Web服務;性能分析;形式化方法

中圖分類號：G642.0 ? ? 文獻標志碼：A ? ? 文章編號：1674-9324（2016）42-0071-02

一、引言

Web服務技術吸收了分布式計算、網格計算和XML等技術的優點，有效地解決了位置對服務使用的制約問題，解決了組織之間數據格式異構、平臺環境異構的問題，具有高度的協同性、跨平臺性、跨地域性和松耦合性。單個Web服務提供的功能單一，不能滿足用戶各種各樣的應用需求。為了求解更為復雜的問題，需要有效地組合各種不同功能的Web服務。為了保證Web服務組合的正確性和契約目標，需要對Web服務組合進行驗證和性能分析。Ulrich Herzog[1]提倡將形式化方法應用到性能評價領域。

基于形式化方法對系統進行動態分析主要有兩種方法：解析/代數方法和數值分析法。解析/代數方法簡單地說就是建立一個解析可解的或代數可解的等式，該等式描述的是系統參數和某個選定性能標準之間的函數關系[2]。例如，C-K方程、穩定狀態方程、嵌入式再生過程、相位概念與矩陣分析、擴散近似方法、補充變量方法、指數卷積、Lindley積分方程、Little定律、流平衡定律、拉普拉斯轉換、離散傅立葉轉換、Jackson狀態概率等都屬于這類方法。數值分析方法包括直接求解、誤差累積、高斯消去法、矩陣幾何等等[3-4]。文獻[5-6]提出的數值分析方法由以下3個步驟組成：（1）將系統描述成一個馬爾可夫鏈;（2）基于馬爾可夫鏈求標識的穩定概率;（3）基于標識的穩定概率求解系統的其他性能參數。

下面我們將介紹在Web服務組合性能評價領域常用的幾種形式化方法。

二、幾種常見的形式化方法

1.排隊論（Queuing Theory）。排隊論是用來模型和分析系統性能的傳統方法，它的基本思想是1910年丹麥數學家A.K.Erlang在解決自動電話設計問題時開始形成的。上世紀50年代初，美國數學家研究了生滅過程，英國科學家D.G.Kendall提出了嵌入馬爾可夫鏈理論，并對排隊隊型提出了分類方法，這些研究工作為排隊論奠定了理論基礎[7]。排隊論用于預測“為隨機發生的需求提供服務”的系統行為，通過分析等待時間、隊列長度、利用率、吞吐量等性能指標的統計規律發現組合服務中可能存在的缺陷。排隊論的理論基礎已經非常成熟，在多個領域中得到了廣泛的應用。

2.Petri網（Petri Nets，PN）。Petri網作為一種重要的數學工具[8]，能夠有效地對分布式系統進行描述和建模，能夠很好地對系統的并發性、可靠性、異步性、不確定性和性能進行動態分析。它不僅具有豐富的形式化語義，而且提供直觀的圖形化表示，同時具備很多系統分析驗證方法（如可達樹、關聯矩陣和狀態方程、不變量和分析化簡規則等），因此被廣泛作為一種形式化工具用于對流程的分析和驗證。

3.進程代數（Process Algebra，PA）。進程代數[9]是將系統抽象成某種元素，在提供嚴格的語義描述系統及行為的基礎上以確定的語法規則來演算系統的動態行為。經典進程代數有：CSP、CCS、LOTOS等。在經典進程代數的基礎上增加定量分析的參數（如時間和概率）就得到了時間進程代數TPA和概率進程代數PPA。TPA和PPA是提出隨機進程代數SPA的基礎。SPA主要用于對并行與分布式系統的性能與可靠性的分析。

4.Pi-演算（Pi-Calculus）。Pi-演算是一種移動進程代數，以進程間的移動通信為研究重點，可以對并發和動態變化的系統進行建模。Pi-演算的基本計算實體是名字和進程，進程之間通過傳遞名字來完成通信。Pi-演算將變量、值、通道名都統稱為名字而不作區分，使得Pi-演算具有了建立新通道的能力，因此Pi-演算可以用來描述結構不斷變化的并發系統[10]。這是CSP或者CCS無法比擬的。Web服務組合具有拓撲結構動態變化的特點，所以可以選擇使用Pi-演算對web服務組合進行建模。

5.自動機理論（automata theory）。自動機理論是將離散數學系統的構造、作用和關系作為研究對象的數學理論。自動機可分為有限自動機、后進先出自動機、線性有界自動機、圖靈機等幾種。有限自動機（Finite State Machine，FAM或Finite State Automaton，FSA）擁有有限個狀態，每個狀態可以根據遷移函數遷移到零個或多個狀態。Web服務組合在整個業務流程中的狀態也是有限的，因此可以考慮運用有限自動機對Web服務進行建模。實際上，基于有限自動機對Web服務組合進行模型與驗證的研究成果已有不少[3]。

三、結語

隨著Internet的廣泛應用和高速發展，出現了大量基于Internet的Web服務，基于Web服務的分布式計算模式已經成為當前的主流技術。一般而言，用于組合的各個原子服務均來自不同的服務提供商，為了保證服務組合能正常工作以達到組合服務的業務目標，必然要求對Web服務組合進行驗證和性能分析。

通常，對Web服務組合進行性能評價可以采用性能測試方法和基于模型的方法。性能測試方法需要對真實系統進行實時監控，根據監控到的數據進行性能分析。基于模型的方法，首先對系統進行建模得到性能分析模型，然后對模型進行模擬仿真分析或基于數學方法的形式化分析。

本文的關注的是，基于模型的形式化分析方法在Web服務組合性能評價中的應用情況。主要介紹了排隊論、Petri網、進程代數、Pi-演算和自動機理論5種常見的形式化方法。

參考文獻：

[1]Ulrich Herzog.Formal Methods for Performance Evaluation[C].7th International School on Formal Methods for the Design of Computer，Communication，and Software Systems，SFM 2007，Bertinoro，Italy，May 8-June 2，2007.

[2]H.Kobayashi.Modeling and Analysis—An Introduction to System Performance Evaluation Methodology[M].London：Addison–Wesley，1978.

[3]雷麗暉，段振華.一種基于擴展有限自動機驗證組合Web服務的方法[J].北京：軟件學報，2007，18（12）：2980-2989.

[4]Solanki M，Cau A，Zedan H.Augmenting semantic Web service description with compositional specification[C].In：Proc.Of the 13th International Conference on World Wide Web.New York：ACM Press，2004：544-552.

[5]Milner R..Communicating and Mobile Systems：The Pi-Calculus[M].London：Cambridge University Press，1999.

[6]靖紅葉.基于Pi演算的Web服務組合的驗證[D].太原：太原理工大學，2008.

[7]http：//www.yeewe.com/edition-view-19101-1.html.

[8]Tadao Murata. Petri Nets：Properties[J].Analysis and Applications Proc. Of the IEEE，1989，77（4）.

[9]林闖，魏丫丫.隨機進程代數與隨機Petri網[J].北京：軟件學報，2002，13（02）：0203-0213.

[10]廖軍，譚浩，劉錦德.基于Pi-演算的Web服務組合的描述和驗證[J].北京：計算機學報，2005，28（04）：635-643.

Brief Introduction on Formal Method of Performance Analysis for Web Service Composition

SHEN Hua

（School of Computer Science，Hubei University of Technology，Wuhan，Hubei 430068，China）

Abstract：Web service composition is a composited service of serveral sub-services according to certain business process.In order to ensure composition service can achieve the expected target，We should verificate the structure of it and analyse its performance before formally putting it into operation.Formal method，which is based on mathematics，is an effective way to analyse the performance of Web service composition.This paper introduces several common formal methods for Web service compositon's performance analysis.

Key words：Web Service;Performance Analysis;Formal Method