中文摘要：

万维网服务是高度分布式的程序，并且并发的软件是非常错误容易的。模型检查是一种强大的技术在并发的系统发现错误。然而，存在模型检查器没有足够的能力为为万维网服务使用的程序语言和通讯机制支持。我们建议把 Kripke 结构用作为万维网服务建模的工具。这篇论文论述一个自动化方法从为抽象模型检查用谓词抽象实现万维网服务的程序提取正式模型。抽象模型借助于一个模型检查器被检查实现自动抽象精炼。这些结果启用实现万维网服务的应用程序的确认。

英文摘要：

Web-services are highly distributed programs, and concurrent software is notoriously error-prone. Model checking is a powerful technique to find bugs in concurrent systems. However, the existing model checkers have no enough ability to support for the programming languages and communication mechanisms used for Web services. We propose to use Kripke structures as means of modeling Web service. This paper presents an automated way to extract formal models from programs implementing Web services using predicate abstraction for abstract model checking. The abstract models are checked by means of a model checker that implements automatic abstraction refinement. These results enable the verification of the applications that implement Web services.