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...

• Type: Conference
• Year: 2008
• Where: SIGSOFT
• Authors: Fang Yu, Chao Wang, Aarti Gupta, Tevfik Bultan
• Keywords: Modular Verification, Scalable Verification Approach, SIGSOFT 2008, Software Engineering, Software/ Program Verification