@inproceedings{9e14533993d34d848e804e086c5ddcf6,
title = "Modular verification of web services using efficient symbolic encoding and summarization",
abstract = "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.",
keywords = "BPEL, Modular Verification, Summarization",
author = "Fang Yu and Chao Wang and Aarti Gupta and Tevfik Bultan",
year = "2008",
doi = "10.1145/1453101.1453127",
language = "English (US)",
isbn = "9781595939951",
series = "Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering",
pages = "192--202",
booktitle = "SIGSOFT 2008/FSE-16 - Proceedings of the 16th ACM SIGSOFT International Symposium on the Foundations of Software Engineering",
note = "16th ACM SIGSOFT International Symposium on the Foundations of Software Engineering, SIGSOFT 2008/FSE-16 ; Conference date: 09-11-2008 Through 14-11-2008",
}