摘要：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：///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