[1]吉顺慧,李必信,周宇.基于顺序图的Web组合服务属性验证[J].东南大学学报(自然科学版),2011,41(2):305-311.[doi:10.3969/j.issn.1001-0505.2011.02.018]
 Ji Shunhui,Li Bixin,Zhou Yu.Sequence diagram based property verification for web service composition[J].Journal of Southeast University (Natural Science Edition),2011,41(2):305-311.[doi:10.3969/j.issn.1001-0505.2011.02.018]
点击复制

基于顺序图的Web组合服务属性验证()
分享到:

《东南大学学报(自然科学版)》[ISSN:1001-0505/CN:32-1178/N]

卷:
41
期数:
2011年第2期
页码:
305-311
栏目:
计算机科学与工程
出版日期:
2011-03-20

文章信息/Info

Title:
Sequence diagram based property verification for web service composition
作者:
吉顺慧李必信周宇
(东南大学计算机科学与工程学院,南京 211189)
Author(s):
Ji ShunhuiLi BixinZhou Yu
(School of Computer Science and Engineering, Southeast University, Nanjing 211189,China)
关键词:
Web组合服务UML建模模型验证SPIN
Keywords:
web service composition UML(unified modeling language) modeling model checking SPIN
分类号:
TP311
DOI:
10.3969/j.issn.1001-0505.2011.02.018
摘要:
为了更好地理解和分析Web组合服务的过程及其相关属性,针对个体服务的WSDL文档和服务组合规约BPEL,提出了基于UML的Web组合服务建模和验证方法.从服务的WSDL中提取消息、操作等基本元素,用类图构建静态模型,以便考虑Web组合服务数据相关属性; 用顺序图对业务流程构建动态模型,以形象易理解的方式刻画组合服务的行为,并简单地考虑了BPEL中的异常处理机制.在此基础上,将模型转换为Promela程序,利用模型检测工具SPIN对服务组合流程相关属性进行验证.实例分析表明,基于UML顺序图的服务组合建模和验证方法是有效的.
Abstract:
To better understand and analyze the process of web service composition and its related properties, a UML(unified modeling language) based modeling and verification approach is proposed for the WSDL (web service description language) of individual service and the business process specification BPEL (business process execution language). Extracting elementary elements from WSDL document of web service, such as message and operation, the class diagram is constructed as the static model to verify the data related properties. The sequence diagram is used to construct the dynamic model for the business process, which visually and intelligibly describes the behavior of web service composition, and it simply considers the fault handling of BPEL. Finally, the model is transferred into the Promela program, and the model checker SPIN is exploited to verify the related properties. The case study illustrates the effectiveness of the approach.

参考文献/References:

[1] Alves A,Arkin A,Askary S.Web services business process execution language version 2.0 [EB/OL].(2007-04-11)[2010-04-20].http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.html.
[2] Object Management Group.Unified modeling language,version 2.0[EB/OL].(2005-07)[2010-04-10].http://www.omg.org/spec/UML/2.0/.
[3] Amsden J,Gardner T,Griffin C,et al.Draft UML 1.4 profile for automated business processes with a mapping to BPEL 1.0,version 1.1[EB/OL].(2003-06)[2010-04-15].http://dwdemos.alphaworks.ibm.com/wstk/common/wstkdoc/services/demos/uml2bpel/README.htm.
[4] Skogan D,Bronmo R,Solheim I.Web service composition in UML[C]//Proceedings of the 8th IEEE Intl Enterprise Distributed Object Computing Conf.Monterey,CA,USA,2004:47-57.
[5] Dumez C,Nait-sidi-moh A,Gaber J,et al.Modeling and specification of web services composition using UML-S[C]//4th International Conference on Next Generation Web Services Practices.Seoul,South Korea,2008:15-20.
[6] Cambronero M E,Diaz G,Pardo J J,et al.Using UML diagrams to model real-time web services[C]//Second International Conference on Internet and Web Applications and Services.Mauritius,2007:24-29.
[7] Clarke E M,Grumberg O,Peled D A.Model checking[M].MIT Press,2000:27-140.
[8] 喻坚,韩燕波.面向服务的计算——原理和应用[M].北京:清华大学出版社,2006:35-170.
[9] 周宇.基于模型的Web服务组合设计、验证及代码生成[D].南京:东南大学计算机科学与工程学院,2008.
[10] 王巧丽.SPIN模型检测的研究与应用[D].贵阳:贵州大学计算机科学与信息学院,2006.
[11] Lima V,Talhi C,Mouheb D,et al.Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages[J].Electronic Notes in Theoretical Computer Science,2009,254:143-160.

备注/Memo

备注/Memo:
作者简介:吉顺慧(1987—),女,博士生;李必信(联系人),男,博士,教授,博士生导师,bx.li@163.com.
基金项目:国家高技术研究发展计划(863计划)资助项目 (2008AA01Z113)、国家自然科学基金资助项目(60773105,60973149).
引文格式: 吉顺慧,李必信,周宇.基于顺序图的Web组合服务属性验证[J].东南大学学报:自然科学版,2011,41(2):305-311.[doi:10.3969/j.issn.1001-0505.2011.02.018]
更新日期/Last Update: 2011-03-20