Message race detection for web services by an SMT-based analysis

  • Mohamed Elwakil
  • , Zijiang Yang
  • , Liqiang Wang
  • , Qichang Chen

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

11 Scopus citations

Abstract

The success of the cloud computing initiative is heavily dependent on realizing trustworthy Web Services. The trustworthiness of a Web Service is judged by four factors: security, privacy, reliability and business integrity. Web Services use message-passing for communication which opens the door for messages races. Messages race with each other when their order of arrival at a destination is not guaranteed and is affected non-deterministically by factors such as network latencies and scheduling variations. Message races are dangerous to Web Services because they can be unforeseen consequences of bugs, causing messages to arrive in an unexpected ordering. In this paper we present a novel approach for improving the reliability of Web Services by detecting message races using SMT-based analysis. We model a BPEL process as a Web Service Modeling Graph (WSMG). A WSMG model is then encoded into a set of SMT constraints. The satisfiability of these constraints means that message races will occur during the actual execution of the Web Service. Hence, we reduce the message race detection problem to constraint solving problem based on satisfiability modulo theories (SMT).

Original languageEnglish
Title of host publicationAutonomic and Trusted Computing - 7th International Conference, ATC 2010, Proceedings
Pages182-194
Number of pages13
DOIs
StatePublished - 2010
Event7th International Conference on Autonomic and Trusted Computing, ATC 2010 - Xi'an, China
Duration: 26 Oct 201029 Oct 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6407 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference7th International Conference on Autonomic and Trusted Computing, ATC 2010
Country/TerritoryChina
CityXi'an
Period26/10/1029/10/10

Keywords

  • satisfiability modulo theories
  • symbolic analysis
  • web services

Fingerprint

Dive into the research topics of 'Message race detection for web services by an SMT-based analysis'. Together they form a unique fingerprint.

Cite this