沈華

摘要：Web服務(wù)組合是若干子服務(wù)按照一定的業(yè)務(wù)流程構(gòu)成的復(fù)合服務(wù)。為了保證這個復(fù)合服務(wù)能夠達(dá)到客戶的預(yù)期目標(biāo)，在將其正式投入運(yùn)行之前，需要對其進(jìn)行結(jié)構(gòu)驗(yàn)證和性能分析。基于數(shù)學(xué)的形式化方法是對Web服務(wù)組合進(jìn)行性能分析的一種有效途徑。本文介紹了幾種常用的形式化方法。

關(guān)鍵詞：Web服務(wù);性能分析;形式化方法

中圖分類號：G642.0 ? ? 文獻(xiàn)標(biāo)志碼：A ? ? 文章編號：1674-9324（2016）42-0071-02

一、引言

Web服務(wù)技術(shù)吸收了分布式計(jì)算、網(wǎng)格計(jì)算和XML等技術(shù)的優(yōu)點(diǎn)，有效地解決了位置對服務(wù)使用的制約問題，解決了組織之間數(shù)據(jù)格式異構(gòu)、平臺環(huán)境異構(gòu)的問題，具有高度的協(xié)同性、跨平臺性、跨地域性和松耦合性。單個Web服務(wù)提供的功能單一，不能滿足用戶各種各樣的應(yīng)用需求。為了求解更為復(fù)雜的問題，需要有效地組合各種不同功能的Web服務(wù)。為了保證Web服務(wù)組合的正確性和契約目標(biāo)，需要對Web服務(wù)組合進(jìn)行驗(yàn)證和性能分析。Ulrich Herzog[1]提倡將形式化方法應(yīng)用到性能評價(jià)領(lǐng)域。

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

下面我們將介紹在Web服務(wù)組合性能評價(jià)領(lǐng)域常用的幾種形式化方法。

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

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

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

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

4.Pi-演算（Pi-Calculus）。Pi-演算是一種移動進(jìn)程代數(shù)，以進(jìn)程間的移動通信為研究重點(diǎn)，可以對并發(fā)和動態(tài)變化的系統(tǒng)進(jìn)行建模。Pi-演算的基本計(jì)算實(shí)體是名字和進(jìn)程，進(jìn)程之間通過傳遞名字來完成通信。Pi-演算將變量、值、通道名都統(tǒng)稱為名字而不作區(qū)分，使得Pi-演算具有了建立新通道的能力，因此Pi-演算可以用來描述結(jié)構(gòu)不斷變化的并發(fā)系統(tǒng)[10]。這是CSP或者CCS無法比擬的。Web服務(wù)組合具有拓?fù)浣Y(jié)構(gòu)動態(tài)變化的特點(diǎn)，所以可以選擇使用Pi-演算對web服務(wù)組合進(jìn)行建模。

5.自動機(jī)理論（automata theory）。自動機(jī)理論是將離散數(shù)學(xué)系統(tǒng)的構(gòu)造、作用和關(guān)系作為研究對象的數(shù)學(xué)理論。自動機(jī)可分為有限自動機(jī)、后進(jìn)先出自動機(jī)、線性有界自動機(jī)、圖靈機(jī)等幾種。有限自動機(jī)（Finite State Machine，F(xiàn)AM或Finite State Automaton，F(xiàn)SA）擁有有限個狀態(tài)，每個狀態(tài)可以根據(jù)遷移函數(shù)遷移到零個或多個狀態(tài)。Web服務(wù)組合在整個業(yè)務(wù)流程中的狀態(tài)也是有限的，因此可以考慮運(yùn)用有限自動機(jī)對Web服務(wù)進(jìn)行建模。實(shí)際上，基于有限自動機(jī)對Web服務(wù)組合進(jìn)行模型與驗(yàn)證的研究成果已有不少[3]。

三、結(jié)語

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

通常，對Web服務(wù)組合進(jìn)行性能評價(jià)可以采用性能測試方法和基于模型的方法。性能測試方法需要對真實(shí)系統(tǒng)進(jìn)行實(shí)時監(jiān)控，根據(jù)監(jiān)控到的數(shù)據(jù)進(jìn)行性能分析。基于模型的方法，首先對系統(tǒng)進(jìn)行建模得到性能分析模型，然后對模型進(jìn)行模擬仿真分析或基于數(shù)學(xué)方法的形式化分析。

本文的關(guān)注的是，基于模型的形式化分析方法在Web服務(wù)組合性能評價(jià)中的應(yīng)用情況。主要介紹了排隊(duì)論、Petri網(wǎng)、進(jìn)程代數(shù)、Pi-演算和自動機(jī)理論5種常見的形式化方法。

參考文獻(xiàn)：

[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]雷麗暉，段振華.一種基于擴(kuò)展有限自動機(jī)驗(yàn)證組合Web服務(wù)的方法[J].北京：軟件學(xué)報(bào)，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服務(wù)組合的驗(yàn)證[D].太原：太原理工大學(xué)，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]林闖，魏丫丫.隨機(jī)進(jìn)程代數(shù)與隨機(jī)Petri網(wǎng)[J].北京：軟件學(xué)報(bào)，2002，13（02）：0203-0213.

[10]廖軍，譚浩，劉錦德.基于Pi-演算的Web服務(wù)組合的描述和驗(yàn)證[J].北京：計(jì)算機(jī)學(xué)報(bào)，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