论文部分内容阅读
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服务组合建模与验证的方法的可行性及有效性。