论文部分内容阅读
Web服务技术给企业的应用程序集成带来了方便,但是分布的单个Web服务功能简单有限,因此有必要将它们进行组合。Web服务的这种组合方式使得各原子服务间产生了大量复杂的信息交互。为了保障组合Web服务的正确性,有必要对其运行过程进行检测。模型检测技术以其自动化程度高,在Web服务的形式化验证中倍受关注。 传统的模型检测方法不能保证带有严格时间约束的实时组合Web服务的正确性。本文将带有时间约束的组合Web服务建模为一组时间自动机,并用基于时间自动机的模型检测工具验证了组合Web服务实时的时态逻辑特性、组合Web服务中存在的特征冲突问题及组合Web服务的时态认知逻辑特性。为了系统的研究组合Web服务,还提出了一种执行代价较小的Web服务组合方法。本文的工作主要体现在以下几个方面: (1)提出了用基于时间自动机的模型检测技术对组合Web服务进行形式化验证的方法。将组合Web服务建模成一组相互通信的时间自动机,并用UPPAAL模拟其运行过程,验证其系统的一些实时时态逻辑特性。以两个组合Web服务为例阐述了该验证过程,并发现其中一个服务存在死锁问题;通过分析死锁产生的路径完善了该服务的协议,从而消除了死锁。此外,首次采用该技术对组合Web服务的特征冲突问题进行了分析和检测。发现了在线股票交易系统的特征冲突现象,验证了该服务的特征冲突属性。 (2)提出了用基于Verics的有界模型检测技术对组合Web服务系统的时态认知逻辑特性进行验证。将组合Web服务建模成时间自动机,用模型检测工具Verics对其系统特性进行分析,验证了传统模型检测工具无法检测的时态认知逻辑;以旅游预订票系统为例阐述了该验证过程。 (3)提出了一种执行代价较小的Web服务反向链组合算法。该方法根据用户的输入和期望的输出,在兼顾Web服务执行代价的同时,动态生成一个执行代价较小以BPEL语言描述的Web服务组合方案;该方案考虑了Web服务的组合效率和执行代价,并且可以采用上述模型检测方法对其进行验证。