摘要
为了更好地理解和分析Web组合服务的过程及其相关属性,针对个体服务的WSDL文档和服务组合规约BPEL,提出了基于UML的Web组合服务建模和验证方法.从服务的WSDL中提取消息、操作等基本元素,用类图构建静态模型,以便考虑Web组合服务数据相关属性;用顺序图对业务流程构建动态模型,以形象易理解的方式刻画组合服务的行为,并简单地考虑了BPEL中的异常处理机制.在此基础上,将模型转换为Promela程序,利用模型检测工具SPIN对服务组合流程相关属性进行验证.实例分析表明,基于UML顺序图的服务组合建模和验证方法是有效的.
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.
出处
《东南大学学报（自然科学版）》
EI
CAS
CSCD
北大核心
2011年第2期305-311,共7页
Journal of Southeast University：Natural Science Edition
基金
国家高技术研究发展计划(863计划)资助项目(2008AA01Z113)
国家自然科学基金资助项目(60773105
60973149)
关键词
WEB组合服务
UML建模
模型验证
SPIN
web service composition
UML（unified modeling language） modeling
model checking
SPIN
