带时间约束的Web服务组合建模与分析  

Modeling and analysis of Web service composition with time constraint

作　　者：吴剑峰[1] 朱稷涵[1] 张广泉[1] 

机构地区：[1]苏州大学计算机科学与技术学院,江苏苏州215006

出　　处：《苏州大学学报（自然科学版）》2012年第1期53-58,共6页Journal of Soochow University(Natural Science Edition)

基　　金：苏州大学"莙政基金"项目;苏州大学国家级大学生创新性实验计划项目(101028524)

摘　　要：如何将现有的Web服务进行组合、实现服务的增值是目前服务计算领域的一个研究热点.针对目前服务组合研究中缺乏对时间属性分析的不足,提出了一种基于时间服务模型(TSM)的Web服务组合模型检测方法.该方法首先将BPEL描述的Web服务行为文档建模为TSM,并转化为UPPAAL规约,然后用分支时序逻辑CTL表示服务组合的性质,最后采用模型检测工具UPPAAL验证服务组合的性质,并结合实例分析了该方法的可行性.How to combine the existing Web services to achieve value-added service is the current research focus.Considering that the current service composition lacks of time property analysis,this paper proposes a method for model checking of Web service composition based on a time aware service model(TSM).First of all,we make a TSM model for the web service interaction behavior described by BPEL and translate it to UPPAAL specification,then use CTL formula to represent properties of the service composition.Finally we validate the properties of composite web services with the UPPALL model checker.After that,we give an example to illustrate the feasibility of this method.

关 键 词：服务组合 BPEL tsm模型 UPPAAL 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]