基于VerICS的Web服务建模与验证

发布时间：2017-08-25 02:42

  本文关键词：基于VerICS的Web服务建模与验证

  更多相关文章： Web服务组合 模型检测 BPEL VerICS 时态认知逻辑

【摘要】：SOA的出现和快速发展,使得Web服务在软件开发过程中成为了一个举足轻重的角色。由于单一Web服务功能受限,它们很难满足用户日益复杂的需求,很多情况下需要将已存的原子Web服务组合起来以实现目标需求。然而,受到服务本身的特性、复杂多变的网络运行环境及服务开发模式的影响,服务组合的正确性、安全性、时效性性等可信性质很容易受到威胁,为保证Web服务组合的正确运行,有必要对Web服务组合进行可信性质的验证工作。形式化方法中的模型检测技术通常被用来建模Web服务组合的运行过程以及验证Web服务组合的可信性质。针对传统的模型检测方法并不能验证带有时间约束的Web服务组合相关性质的缺陷,本文提出了一种基于VerICS的Web服务建模与验证方法,该方法不仅能够验证带有时间约束的Web服务组合的时态逻辑性质,还能够验证Web服务组合的认知逻辑性质。本文的工作分为以下几个方面:(1)为了能够使用VerICS验证带有时间约束属性的Web服务组合的相关性质,首先提出了Web服务业务流程描述语言BPEL的时间约束属性扩展方法;(2)提出BPEL流程与VerICS输入语言IL的“中间桥梁”BPEL输入输出状态迁移系统BIOSTS形式模型的概念,给出BPEL流程各基本活动与结构活动的的BIOSTS形式化建模过程,为下一步提供BPEL流程的自动化验证程度打下基础;(3)提出BPEL流程到BIOSTS的转化算法BP2BS,以及BPEL各结构活动到BIOSTS的转化算法。这一系列算法实现了BPEL流程的自动形式化建模,提高了Web服务组合的自动化验证程度;(4)提出BIOSTS到VerICS的输入语言IL的转化算法BS2IL。该算法综合考虑形式模型BIOSTS的特征与IL的语法特征,将BIOSTS包含的各元素转化为IL语言中的各个组成部分;实现了二者之间的自动转化,减少转化过程中繁琐的人工编码工作,实现BPEL流程的自动化模型检测;(5)运用模型检测工具VerICS对虚拟旅游系统VTA的时态认知逻辑性质进行验证,根据验证结果判定该Web服务组合是否满足目标需求。这个实例说明了本文所提出的针对Web服务组合建模与验证的方法的可行性及有效性。
【关键词】：Web服务组合 模型检测 BPEL VerICS 时态认知逻辑
【学位授予单位】：华侨大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：TP393.09
【目录】：

• 摘要3-5
• Abstract5-9
• 第1章 绪论9-16
• 1.1 研究背景及意义9-10
• 1.2 国内外研究现状10-13
• 1.2.1 Petri网方法10-11
• 1.2.2 进程代数方法11
• 1.2.3 有限状态机方法11-12
• 1.2.4 时态认知逻辑模型检测方法12-13
• 1.3 本文研究内容与创新点13-14
• 1.4 论文结构14-16
• 第2章 模型检测16-25
• 2.1 Kripke结构16-17
• 2.2 时态逻辑17-19
• 2.2.1 线性时态逻辑LTL17-18
• 2.2.2 计算树逻辑CTL*18-19
• 2.3 知识推理19-21
• 2.4 时态认知逻辑CTLKD21-23
• 2.5 模型检测工具VerICS23-24
• 2.6 本章小结24-25
• 第3章 Web服务业务流程25-29
• 3.1 Web服务及其体系结构25-26
• 3.1.1 Web服务定义25
• 3.1.2 Web服务体系结构25-26
• 3.2 Web服务组合26-27
• 3.3 Web服务业务流程执行语言BPEL27-28
• 3.3.1 BPEL定义27
• 3.3.2 BPEL组成27
• 3.3.3 BPEL活动介绍27-28
• 3.4 本章小结28-29
• 第4章 BPEL形式模型及其自动化模型检测方法29-65
• 4.1 BPEL时间约束属性的扩展29-31
• 4.2 BPEL形式模型BIOSTS31-32
• 4.3 BPEL活动形式化建模32-50
• 4.3.1 BEPL基本活动形式化建模32-41
• 4.3.2 BPEL结构活动形式化建模41-50
• 4.4 BPEL流程自动化模型检测方法50-60
• 4.4.1 BPEL到BIOSTS转化算法50-55
• 4.4.2 BIOSTS到IL转化算法55-60
• 4.5 Web服务组合建模与验证框架60-64
• 4.5.1 时态认知逻辑ECTLKD与TECTLK61-62
• 4.5.2 框架结构62-64
• 4.6 本章小结64-65
• 第5章 实例研究65-76
• 5.1 VTA概述65
• 5.2 BPEL时间约束属性扩展65-67
• 5.3 将 BPEL 转化为 BIOSTS67-69
• 5.4 将BIOSTS转化为IL69-73
• 5.5 VTA规范验证73-75
• 5.6 本章小结75-76
• 第6章 总结与展望76-78
• 参考文献78-83
• 致谢83-84
• 个人简历、在学期间发表的学术论文及研究成果84

，

本文编号：734631