基于uMSD的Web服务组合验证方法研究  

Research on Verification of Web Service Composition Based on uMSD

作　　者：王志坚[1] 李雯睿[2,3] 杨种学[2] 张鹏程[1,3] 

机构地区：[1]河海大学计算机与信息学院,南京210098 [2]南京晓庄学院数学与信息技术学院,南京211171 [3]武汉大学软件工程国家重点实验室,武汉430072

出　　处：《计算机科学》2011年第9期119-125,共7页Computer Science

基　　金：国家高技术研究发展计划(2007AA01Z178);武汉大学软件工程国家重点实验室开放(2010-08-01);河海大学中央高校基本科研业务经费(2009B04314);江苏省高校自然科学基金(11KJD520010)资助

摘　　要：手工分析组合服务相当困难和耗时,为此提出了一种基于uMSD的Web服务组合的模型检验方法。如何简单和直观地表示Web服务组合的时态性质是该方法的关键问题。鉴于uMSD在简单性和表达力之间找到了一个平衡点,定义了uMSD的形式语法和语义。以Web服务组合OJA为实例,使用uMSD来图形化地表示组合服务的时态性质,展示了uMSD的可行性。实验分析表明,该验证方法能够有效地检测组合服务中的逻辑错误。In order to solve the problem that analyzing the composite services by manual is rather difficult and time-consuming,an approach was proposed to verify composite services by model checking based on uMSD.How to represent the temporal properties of the composite service easily and intuitively is a critical issue of the approach.Because uMSD finds a balance between simplicity of use and expressiveness,the paper defined the formal syntax and semantics of uMSD.In the paper,uMSD was used to graphically represent the temporal properties of a composite service On-the-Job Assistant as a case study,presenting the feasibility of uMSD.A series of experiments show the approach can effectively detect the logical errors in the composite service.

关 键 词：模态顺序图 WEB服务组合 模型检验 

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