基于XYZ/ADL的异步Web服务组合描述与验证  

Description and Verification of Asynchronous Web Service Composition Based on XYZ/ADL

作　　者：石慧娟[1] 戎玫[2] 张广泉[1,3] 朱稷涵[1] 

机构地区：[1]苏州大学计算机科学与技术学院,苏州215006 [2]暨南大学深圳旅游学院,深圳518053 [3]中国科学院软件研究所计算机科学国家重点实验室,北京100080

出　　处：《计算机科学》2011年第12期139-143,共5页Computer Science

基　　金：国家自然科学基金(60973149);江苏省自然科学基金(BK2011281);中国科学院计算机科学国家重点实验室开放课题(SYSKF0908);江苏省高校自然科学研究项目(08KJB520010);苏州大学国家级大学生创新性实验计划项目(101028524)资助

摘　　要：以Web服务组合为研究对象,重点讨论了服务组合中异步通信行为和时间属性的形式化描述和验证。首先,从软件体系结构角度分析Web服务组合,采用基于时序逻辑的XYZ/ADL描述Web服务的交互行为和时间属性;然后,提出一种符合模型检测工具UPPAAL规约的时间异步通信模型TACM;最后,实现了XYZ/RE通信命令到TACM的映射,利用UPPAAL验证了服务组合系统异步通信行为的正确性。Concerned with Web service composition, this paper especially emphasized the formal description and verifi- cation of asynchronous communication behaviors and timed properties. Firstly,analyzing Web service composition from software architecture,the interactive behaviors and timed properties were described by XYZ/ADL based on temporal logic language. Secondly, timed asynchronous communication model （TACM） which accords with the specification of model checker UPPAAL was proposed. Finally, based on the transition from XYZ/RE communication command sentences to TACM, the correctness of asynchronous communication behaviors of the service composition system was verified by UPPAAL.

关 键 词：WEB服务组合 XYZ/ADL 异步通信 时间属性 模型检测 

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