Sciweavers

Share
SIGSOFT
2008
ACM

Modular verification of web services using efficient symbolic encoding and summarization

10 years 7 months ago
Modular verification of web services using efficient symbolic encoding and summarization
We propose a novel method for modular verification of web service compositions. We first use symbolic fixpoint computations to derive conditions on the incoming messages and relations among the incoming and outgoing messages of individual BPEL web services. These pre- and post-conditions are accumulated and serve as a repository of summarizations of individual web services. We then compose the summaries of the invoked BPEL services to model external invocations, resulting in a scalable verification approach for web service compositions. Our technical contributions include (1) an efficient symbolic encoding for modeling the concurrency semantics of systems having both multi-threading and message passing, and (2) a scalable method for summarizing concurrent processes that interact with each other using synchronous message passing, along with a modular framework that utilizes these summaries for scalable verification. Categories and Subject Descriptors: D.2.4 [Software/ Program Verificat...
Fang Yu, Chao Wang, Aarti Gupta, Tevfik Bultan
Added 20 Nov 2009
Updated 20 Nov 2009
Type Conference
Year 2008
Where SIGSOFT
Authors Fang Yu, Chao Wang, Aarti Gupta, Tevfik Bultan
Comments (0)
books