一种基于UPPAAL的Web服务组合模型检测方法

计算机科学 ›› 2010, Vol. 37 ›› Issue (11): 122-125.

一种基于UPPAAL的Web服务组合模型检测方法

何亚丽,戎玫,张广泉

(苏州大学计算机科学与技术学院苏州215006);(暨南大学深圳旅游学院深圳518053);(中国科学院软件研究所计算机科学国家重点实验室北京100080)

出版日期:2018-12-01 发布日期:2018-12-01
基金资助:
本文受中国科学院计算机科学国家重点实验室开放课题(SYSKF0908) ,江苏省高校自然科学研究项目(08KJB520010)资助。

Model Checking of Web Service Composition Based on UPPAAL

HE Ya-li,RONG Mei,ZHANG Guang-quan

Online:2018-12-01 Published:2018-12-01

摘要/Abstract

摘要： Web服务组合的正确性验证对提高软件开发效率、实现服务增值具有重要意义。为从高层抽象层次研究Web服务组合的正确性及其形式化验证方法，考虑到Web服务组合中的实时特征，在采用软件体系结构描述语言XYG/ADL对Web服务组合进行描述的基础上，将其实时描述部分XYZ/RE转换至时间自动机模型，组合后系统应满足的性质用分支时序逻辑CTL公式表示，最后应用模型检测工具UPPAAL实现了Web服务组合正确性的自动化验证。

关键词: Web服务组合，模型检测，XYZ/ADL, XYZ/RE, UPPAAL

Abstract: Correctness verification of Web service composition plays an important role for improving software development efficiency and realizing service value-added. To study the correctness of Web service composition and their formal verification method from a high and abstract view, considering the real-time feature in Web service composition, based on the description of Web service composition using software architecture description language XYZ/ADL,the real-time description XYZ/RE was transformed to timed automata, the properties that the composite system should be satisfied were expressed in CTL formula, last, the correctness of Web service composition was automatically verified through a model checking tool-UPPAAL.

Key words: Web service composition, Model checking, XYZ/ADL, XYZ/RE, UPPAAL

何亚丽,戎玫,张广泉. 一种基于UPPAAL的Web服务组合模型检测方法[J]. 计算机科学, 2010, 37(11): 122-125. https://doi.org/

HE Ya-li,RONG Mei,ZHANG Guang-quan. Model Checking of Web Service Composition Based on UPPAAL[J]. Computer Science, 2010, 37(11): 122-125. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed