基于动态描述逻辑和模型检测的语义Web服务验证方法

摘要

本发明公开一种基于动态描述逻辑和模型检测的语义Web服务验证方法，在语义Web环境中模型验证技术的基础上，引入动态描述逻辑，将动作的执行作为Web服务模型中状态变化的原因，其可以将传统的模型检测技术应用到语义Web环境下Web服务验证的问题上。从系统模型的角度，将语义Web服务抽象为模型检测中的状态迁移系统；同时引入了动作理论，将原子服务的前提条件和执行结果抽象为动作理论的原子动作，将动作的执行看作是原子服务中状态迁移的原因。在此基础上，考察动作的执行所产生的模型是否满足时态规范。本发明弥补了传统的验证方法没有考虑Web服务中状态迁移原因的局限性，丰富了语义Web环境下Web服务验证的方法。