Modular verification of web services using efficient symbolic encoding and summarization

Fang Yu, Chao Wang, Aarti Gupta, Tevfik Bultan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationSIGSOFT 2008/FSE-16 - Proceedings of the 16th ACM SIGSOFT International Symposium on the Foundations of Software Engineering
Pages192-202
Number of pages11
DOIs
StatePublished - Dec 1 2008
Externally publishedYes
Event16th ACM SIGSOFT International Symposium on the Foundations of Software Engineering, SIGSOFT 2008/FSE-16 - Atlanta, GA, United States
Duration: Nov 9 2008Nov 14 2008

Publication series

NameProceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering

Other

Other16th ACM SIGSOFT International Symposium on the Foundations of Software Engineering, SIGSOFT 2008/FSE-16
CountryUnited States
CityAtlanta, GA
Period11/9/0811/14/08

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • BPEL
  • Modular Verification
  • Summarization

Fingerprint Dive into the research topics of 'Modular verification of web services using efficient symbolic encoding and summarization'. Together they form a unique fingerprint.

  • Cite this

    Yu, F., Wang, C., Gupta, A., & Bultan, T. (2008). Modular verification of web services using efficient symbolic encoding and summarization. In SIGSOFT 2008/FSE-16 - Proceedings of the 16th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (pp. 192-202). (Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering). https://doi.org/10.1145/1453101.1453127