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

被引：6

作者：

张广泉 ^{[1
,2
]}

戎玫 ^{[3
]}

朱雪阳 ^{[2
]}

何亚丽 ^{[1
]}

石慧娟 ^{[1
]}

机构：

[1] 苏州大学计算机科学与技术学院

[2] 中国科学院计算机科学国家重点实验室

[3] 暨南大学深圳旅游学院

来源：

电子学报 | 2011年 / 39(S1)卷 / S1期

关键词：

Web服务组合; XYZ/ADL; XYZ/RE; 时间自动机; 精化检验; 模型检测;

D O I：

暂无

中图分类号：

TP393.09 [];

学科分类号：

080402 ;

摘要：

Web服务组合是当前Web服务领域的一个研究热点,目前已有一些相关的描述与验证方法,本文从软件体系结构角度研究Web服务组合描述与验证方法.基于软件体系结构描述语言XYZ/ADL和精化检验/模型检测方法,提出了一种Web服务组合的描述与验证方法.XYZ/ADL是时序逻辑语言XYZ/E的扩展,考虑到多数Web服务具有实时特征,采用XYZ/E的实时扩展语言XYZ/RE表示系统应满足的时间约束.针对Web服务组合系统,根据XYZ/RE到时间自动机的映射规则将系统描述转换为对应的时间自动机,分别采用精化检验和模型检测两种技术验证Web服务组合的正确性;最后通过两个实例分析分别阐述了上述方法的可行性和有效性.

引用

页码：86 / 93

页数：8

共 5 条

[1] 并发反应式系统的组合模型检验与组合精化检验 [J].