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

摘要

Web service compxosition is the hotspot in the field of Web services. Many methods are proposed to describe and verify its correctness. This paper reseaaches specification and verification of Web services composition from software architecture.Refinement checking and model checking are two important formal verification methods. This paper explores the problem of Web service composition based on both software architecture description language XYZ/ADL and formal verification, then proposes a specification and verification method of Web service composition. XYZ/ADL is the extension of the temporal logic language XYZ/E. Considering most Web service with real time characteristics, we can use XYZ/RE which is the real time extension of XYZ/E to express time constraints of the system. For systems with time constraints,we transform the system description to conresponding timed automata according to the mapping rudes,then use refinement checking and model checking to verify the correctness of web service composition. Experiments demonstrate feasibility and validity of above idea.%Web服务组合是当前Web服务领域的一个研究热点,目前已有一些相关的描述与验证方法,本文从软件体系结构角度研究Web服务组合描述与验证方法.基于软件体系结构描述语言XYZ/ADL和精化检验/模型检测方法,提出了一种Web服务组合的描述与验证方法.XYZ/ADL是时序逻辑语言XYZ/E的扩展,考虑到多数Web服务具有实时特征,采用XYZ/E的实时扩展语言XYZ/RE表示系统应满足的时间约束.针对Web服务组合系统,根据XYZ/RE到时间自动机的映射规则将系统描述转换为对应的时间自动机,分别采用精化检验和模型检测两种技术验证Web服务组合的正确性;最后通过两个实例分析分别阐述了上述方法的可行性和有效性.