技术简介

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