基于符号模型检测的Web服务组合形式化验证∗

张世杰 徐 鹏 刘沛瑶

（1.西南交通大学数学学院 成都 610031）

（2.系统可信性自动验证国家地方联合工程实验室 成都 610031）

1 引言

面向服务的体系结构SOA（Service Oriented Architecture）是一种构建分布式系统的方式，将功能作为服务提供，强调交互服务之间的松散耦合［1］。Web服务随着SOA的提出而不断发展，其是SOA体系结构的基本单元，是一种新型的Web应用［2］。随着经济的发展与用户需求的多样化和综合化，单一Web服务所提供的功能已经不能满足需求，因此产生了Web服务组合（Web Service Composition，WSC）。WSC可以集成现有的异构服务而组合成可以提供更复杂功能的新服务，实现更高的服务可重用性和获取增值服务［3］。但WSC也带来了一些新的挑战：如何保证Web服务组合过程的正确性？如何验证组合服务满足某些需要的特性？如何对WSC进行有效的建模、分析和验证？

Web服务组合问题包括：Web服务发现，Web服务组合及组合Web服务的形式化验证。本文研究的重点是组合Web服务的形式化验证，其是保证组合Web服务正式发布投入市场运行，减小其故障的重要手段。常用的服务组合验证方法是69%的模型检查，进程代数的使用率为29%，定理证明方法应用于9%的被调查机制。Web服务组合验证广泛使用的建模工具是NuSMV（22%），SPIN（17%），CPN（12%），UPPAAL（12%），Event-B（10%）和PAT（5%）［4］。

基于Petri网及进程代数的演绎验证方法验证能力很强，但自动化程度不高验证过程需要大量人工参与，当组合Web服务系统比较庞大时就变得相当复杂。沈华等［5］在基于随机Petri网的Web服务组合模型WSCPAM的基础上，提出了对模型进行有界性、死锁、陷阱验证的必要性、意义和算法实现。……