TY - GEN
T1 - Modular verification of web services using efficient symbolic encoding and summarization
AU - Yu, Fang
AU - Wang, Chao
AU - Gupta, Aarti
AU - Bultan, Tevfik
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
KW - BPEL
KW - Modular Verification
KW - Summarization
UR - http://www.scopus.com/inward/record.url?scp=70349707526&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70349707526&partnerID=8YFLogxK
U2 - 10.1145/1453101.1453127
DO - 10.1145/1453101.1453127
M3 - Conference contribution
AN - SCOPUS:70349707526
SN - 9781595939951
T3 - Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering
SP - 192
EP - 202
BT - SIGSOFT 2008/FSE-16 - Proceedings of the 16th ACM SIGSOFT International Symposium on the Foundations of Software Engineering
T2 - 16th ACM SIGSOFT International Symposium on the Foundations of Software Engineering, SIGSOFT 2008/FSE-16
Y2 - 9 November 2008 through 14 November 2008
ER -