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

以Web服务组合为研究对象，重点讨论了服务组合中异步通信行为和时间属性的形式化描述和验证。首先，从软件体系结构角度分析Web服务组合，采用基于时序逻辑的XYZ/ADL描述Web服务的交互行为和时间属性;然后，提出一种符合模型检测工具UPPAAI规约的时间异步通信模型TACM;最后，实现了XYZ/RE通信命令到TACM的映射，利用UPPAA工验证了服务组合系统异步通信行为的正确性。