(最新)语义web服务组合的形式化描述与验证研究

《(最新)语义web服务组合的形式化描述与验证研究》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、万方数据计算机科学2008V01．35No．4语义Web服务组合的形式化描述与验证研究*)程永上王志坚(河海大学计算机与信息工程学院南京210098)摘要web服务组合是Web服务的主要研究方向之一，对语叉Web服务组合进行形式化描述并进行分析和验证是组合服务正确运行的保证。本文首先给出了基于有色Petri网的语义Web服务形式化模型，形式化描述了OWL-S的ServiceModel中8种基本的Web服务组合模式，利用这些组合模式可以构造出满足需求的组合Web服务。然后，对服务组合形式化模型的正确性分析和验证进行研究后，给出了组合模型语法正确性、可达性

2、、活性和有界性的算法。最后，通过一个具体的建模实例展示了Web服务组合的Petri网建模。关键词Web服务，Web服务组合，Petri网，建模，验证ResearchonFormalDescriptionandVerificationofSemanticWebServiceCompositionCHENGYong-ShangWANGZhi-Jfan(ComputerandInformationEngineeringCollege，HohaiUniversity，Nanjing210098)Absh日ctComposingWebserviceisoneof

3、themainresearchdirections．FormallydescribingsemanticWebservicecomposition，analyzingandverifyillgthecompositionmodelcanguaranteethecorrectnessoftheW曲servicecomposi-tion．Inthispaper，firstly，theformalmodelofthesemanticWcbservicecompositionbased01"1coloredPetrinetsispresented，and8ki

4、ndsofbasicWebservicecompositionpatternsinServiceModelof咖一Sareprovided．UtilizingthesepatternscanconstructthecompositeWebserviceofsatisfyingusers’requirements．Then。afterthecorrectnessanalysisandverificationabouttheWebservicecompositionmodelarestudied，thealgorithmsonWebservicecompo

5、si—tionsyntaxcorrectness，reachability，livenessandboundednessaregiven．Finally，modelingtheWebservicecomposi-tionbasedoncoloredPetrinetsisappliedintoaease．KeywordsWebservice，Webservicecomposition，Petrinets，Model，Verification1引言Web服务提供了一种平台独立，自描述、松耦合、位置透明的软件模块，便于实现不同应用的交互和集成。而语义Web的

6、出现给Web服务技术带来了新的契机，两者的结合能够实现web服务的机器可理解和处理，使web服务发现、组合、运行和监督等自动化成为了可能。由于单个web服务功能有限，不能满足日趋复杂的实际应用需求，必须将多个可用的自治服务协调工作，产生一个新的增殖的功能更强的复合服务，Web的潜能才能被激发出来。如今，对于语义web服务组合的研究已成为一个热点，而以透明方式实现服务组合的自动化也成为一个挑战。一般而言，用于组合的各个服务均来自分布于Web上的不同组织或者机构的原子服务，使用者很难掌控，设计有误的组合服务一旦付诸实施，造成的损失将会比较大，且随着业务需求

7、的不断增强，Web服务组合日趋复杂，服务组合出错的可能性也在增大，这些错误将导致资源和时间上的巨大浪费。为了在组合服务执行前发现错误并改正错误，避免执行时因错误而造成重大的损失，必须在组合规划时对组合服务进行正确性验证。达到这种目标的一种途径就是建立web服务组合的形式化描述模型，利用对形式化模型的分析、验证方法来检验web服务组合的正确性。这里主要有两种类型的组合形式化建模方式：进程代数[1]和Petri网[2]。进程代数的起源可以追溯到20世纪70年代，它是一类用代数方法研究通信并发系统的理论的泛称，包括通信系统演算ccg引、通信顺序进程CSP[4

8、。、通信进程代数ACP[引、Pi-演算[6]等；而Petri网来源于1962年德国Petri教