Automatic dynamic generation of likely invariants for WS-BPEL compositions

Manuel Palomo-Duarte*, Antonio García-Domínguez, Inmaculada Medina-Bulo

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review


The wide adoption of Web Services has led to the development of languages to compose them, like the WS-BPEL standard. In order to check whether the composition works as expected, one common approach is to analyze it and infer functional properties describing its behavior. Traditional approaches for inferring properties in WS-BPEL have been static: compositions are transformed into specialized analysis models based on some formalization. However, this formalization could be inexact due to theoretical limitations or differing interpretations of the standard by implementers. Dynamic invariant generation solves these problems by extracting the properties from actual executions and has been successfully used in popular languages, but not to WS-BPEL yet. In this work, we apply dynamic invariant generation to WS-BPEL, providing innovative solutions for several features that require special consideration, like highly multidimensional values in variables, an advanced type system or unstructured code. We have implemented these solutions in Takuan and evaluated its performance with several compositions of varying complexity. We present the results obtained and a comparative analysis of the efficiency and effectiveness of our solutions. Results show that the solutions are successful in reducing the cost of applying dynamic invariant generation and the number of uninteresting invariants generated.

Original languageEnglish
Pages (from-to)5041-5055
Number of pages15
JournalExpert Systems with Applications
Issue number11
Early online date25 Feb 2014
Publication statusPublished - 1 Sept 2014


  • dynamic invariant generation
  • web service composition
  • white-box testing


Dive into the research topics of 'Automatic dynamic generation of likely invariants for WS-BPEL compositions'. Together they form a unique fingerprint.

Cite this