一种基于约束求解器的服务组合验证方法

本发明提出了一种基于约束求解器的服务组合验证方法，该方法包括以下步骤：

1. Web服务文档解析过程：

   • 包括对WSDL文档和BPEL文档的解析。

2. 获取变量属性信息：

   • 根据BPEL中定义的命名空间对应关系，取得BPEL中变量在对应的WSDL中的元素属性信息。

3. 生成控制流图（CFG图）：

   • 根据BPEL文档生成服务组合的控制流图，即CFG图。

4. 描述CFG图：

   • 建立一个一阶公式来描述CFG图。

5. 生成约束条件：

   • 结合Z3求解器的输入语法要求，生成符合求解器输入格式的约束条件。

6. 验证过程：

   • 将上几步中生成的约束条件及逻辑公式代入Z3求解器，进行验证。

该方法从Web服务文档出发，对服务文档进行分析，能够方便且高效地验证Web服务。

本发明给出了一种基于约束求解器的服务组合验证方法，包含对WSDL，BPEL文档解析得到相关元素和变量的属性和取值，生成CFG图，描述CFG图，求解器求解等步骤。1)Web服务文档解析过程，包括对WSDL文档和BPEL文档的解析，2)根据BPEL中定义的命名空间对应关系，取得BPEL中变量在对应的WSDL中的元素属性信息，3)根据BPEL文档生成服务组合的控制流图即CFG图；4)建立一个一阶公式描述CFG图。5)结合Z3求解器对输入的语法要求，生成符合求解器输入格式的约束条件；6)将上几步中生成的约束条件及逻辑公式代入Z3求解器，进行验证。该方法从Web服务文档出发，对服务文档进行分析，可方便高效地验证Web服务。