基于扩展自动机的服务组合静态与动态验证方法

• 作者: 张广泉 晏荣杰 朱雪阳 狄浩军 石慧娟
• 来源期刊: 通信学报
• 学科: 工学
• 关键词: Web服务组合 定量属性 有限自动机 CTL UPPAAL
• 年，卷（期）: 2012,（z1）
• 页码范围: 1-8
• 分类号: TP311
• 字数: 5696字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-436x.2012.z1.001

摘要

针对目前 Web服务组合研究中缺少对定量属性的验证以及在服务运行过程中缺乏对出现异常时的故障处理等问题,提出了一种基于扩展有限自动机的Web服务组合静态与动态验证方法.该方法首先对有限自动机进行扩展,建立了一个可以描述数据及时间等信息的Web服务组合形式化模型;基于该模型,采用计算树逻辑(CTL)描述相关属性,并利用模型检测工具UPPAAL对 Web服务组合的行为属性、时间属性以及数据属性等进行了验证;最后结合所建立的诊断模型,给出了一种能够对Web服务组合运行过程中出现异常时进行有效处理的错误诊断算法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张广泉	苏州大学计算机科学与技术学院	147	1056	16.0	25.0
2	石慧娟	苏州大学计算机科学与技术学院	3	22	3.0	3.0
3	朱雪阳	中国科学院软件研究所计算机科学国家重点实验室	7	85	5.0	7.0
4	狄浩军	苏州大学计算机科学与技术学院	2	11	2.0	2.0
5	晏荣杰	中国科学院软件研究所计算机科学国家重点实验室	6	21	3.0	4.0