中文摘要：

为了更好地理解和分析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.