论文部分内容阅读
面向服务的体系结构(SOA)作为一种新的软件开发范型,正逐步成为未来软件发展的趋势之一,而其主流的实现方式Web服务技术也得到了快速的发展与应用。由于单个Web服务提供的功能有限,有必要将多个服务组装成一个价值增值的、粒度更大的服务或系统以满足复杂的应用需求。但在服务组合过程中,因存在接口类型、数据格式或交互协议不一致等失配情况,导致服务无法正确组合。服务失配检测可准确捕捉失配点,为实现服务的正确组合奠定基础。从互操作性分层的角度分析,服务失配可能发生在签名、行为、语义等层次。其中行为层的失配研究是关键也是难点,本文研究Web服务在行为层次的失配。如果参与交互的服务最终能到达各自的终止状态,则服务交互过程不存在失配,否则就存在失配。换言之,本文将服务的失配检测问题转化为服务兼容性判定问题。形式化验证技术(如模型检测)作为软件质量保证的一种重要方法,目前已广泛应用于Web服务相关性质验证。限界模型检测(BMC)采用由局部到全局渐进式检测,能快速寻找到反例。本文采用BMC围绕Web服务失配检测展开了研究,具体内容包括:(1)提出了一种基于NuSMV的Web服务失配检测方法。首先给出Web服务交互行为以及兼容性质的形式化描述,然后利用支持BMC的模型检测工具NuSMV验证服务交互模型是否满足兼容性质,性质不满足时,给出反例说明。(2)提出了一种基于SMT的Web服务失配检测方法,通过检测服务交互过程死锁状态是否可达来判定Web服务交互行为的兼容性。首先对Web服务交互行为进行建模,然后将其转化为SMT工具可识别的逻辑公式,并用逻辑公式表示兼容性质的否定,利用SMT工具实现Web服务的失配检测。(3)将时间属性引入Web服务交互过程中,建立带有时间属性的Web服务形式化模型,提出基于SMT的时间感知Web服务失配检测方法。