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

Specification and Verification of Web Service Composition Based on XYZ/ADL

作　　者：张广泉[1,2] 戎玫[3] 朱雪阳[2] 何亚丽[1] 石慧娟[1] 

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

出　　处：《电子学报》2011年第A03期86-93,共8页Acta Electronica Sinica

基　　金：国家自然科学基金(No.60973149);中国科学院计算机科学国家重点实验室开放课题(No.SYSKF0908);江苏省高校自然科学研究项目(No.08KJB520010)

摘　　要：Web服务组合是当前Web服务领域的一个研究热点,目前已有一些相关的描述与验证方法,本文从软件体系结构角度研究Web服务组合描述与验证方法.基于软件体系结构描述语言XYZ/ADL和精化检验/模型检测方法,提出了一种Web服务组合的描述与验证方法.XYZ/ADL是时序逻辑语言XYZ/E的扩展,考虑到多数Web服务具有实时特征,采用XYZ/E的实时扩展语言XYZ/RE表示系统应满足的时间约束.针对Web服务组合系统,根据XYZ/RE到时间自动机的映射规则将系统描述转换为对应的时间自动机,分别采用精化检验和模型检测两种技术验证Web服务组合的正确性;最后通过两个实例分析分别阐述了上述方法的可行性和有效性.Web service composition is the hotspot in the field of Web services.Many methods are proposed to describe and verify its correctness.This paper researches 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 corresponding timed automata according to the mapping rules,then use refinement checking and model checking to verify the correctness of web service composition.Experiments demonstrate feasibility and validity of above idea.

关 键 词：WEB服务组合 XYZ/ADL XYZ/RE 时间自动机 精化检验 模型检测 

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