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

ZHANG Guang-quan; RONG Mei; ZHU Xue-yang; HE Ya-Li; SHI Hui-juan

您当前的位置：

首页 >

文章列表页 >

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

更新时间：2025-07-16

- Specification and Verification of Web Service Composition Based on XYZ/ADL
- Acta Electronica Sinica Vol. 39, Issue 3A, Pages: 86-93(2011)
- 作者机构：
  
  1. 苏州大学计算机科学与技术学院,江苏,苏州,215006
  2. 中国科学院计算机科学国家重点实验室,北京,100080
  3. 暨南大学深圳旅游学院,广东,深圳,518053
  4. 苏州大学计算机科学与技术学院江苏苏州,215006
  5. 中国科学院计算机科学国家重点实验室北京,100080
  6. 暨南大学深圳旅游学院广东深圳,518053
- 作者简介：
- 基金信息：
- DOI：
  CLC： TP311
- Published：2011
- 稿件说明：
移动端阅览
ZHANG Guang-quan, RONG Mei, ZHU Xue-yang, et al. Specification and Verification of Web Service Composition Based on XYZ/ADL[J]. Acta Electronica Sinica, 2011, 39(3A): 86-93.
DOI：

ZHANG Guang-quan, RONG Mei, ZHU Xue-yang, et al. Specification and Verification of Web Service Composition Based on XYZ/ADL[J]. Acta Electronica Sinica, 2011, 39(3A): 86-93. DOI：

摘要

Web服务组合是当前Web服务领域的一个研究热点

目前已有一些相关的描述与验证方法

本文从软件体系结构角度研究Web服务组合描述与验证方法.基于软件体系结构描述语言XYZ/ADL和精化检验/模型检测方法

提出了一种Web服务组合的描述与验证方法.XYZ/ADL是时序逻辑语言XYZ/E的扩展

考虑到多数Web服务具有实时特征

采用XYZ/E的实时扩展语言XYZ/RE表示系统应满足的时间约束.针对Web服务组合系统

根据XYZ/RE到时间自动机的映射规则将系统描述转换为对应的时间自动机

分别采用精化检验和模型检测两种技术验证Web服务组合的正确性;最后通过两个实例分析分别阐述了上述方法的可行性和有效性.

Abstract

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.

关键词

Keywords

references

Views

1429

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Exact Acceleration of Real-Time Model Checking Based on Parking Cycle

Research on Interaction Modeling and Mismatch Checking of Time-Aware Web Services

Behavioral Compatibility Analysis and Optimal Control Policy in Web Services Composition

Precisely Detecting Buffer Overflow Vulnerabilities

Model Checking: Theories, Techniques and Applications

Related Author

WANG Cong-yin

ZHUANG Lei

YIN Chuan-long

Sheng

WANG Sheng

ZHANG Guang-quan

ZHU Zhi-liang

BI Jing

Related Institution

School of Information Engineering, Zhengzhou University

College of Maths and Computer Science,Jishou University,Jishou

School of Information EngineeringZhengzhou UniversityZhengzhouHenan 450052China

College of Maths and Computer ScienceJishou UniversityJishouHunan 416000China

State Key Laboratory of Computer Science,Chinese Academy of Science

⁰