Sciweavers

Share
WSFM
2007
Springer

Extending Model Checking to Data-Aware Temporal Properties of Web Services

11 years 6 months ago
Extending Model Checking to Data-Aware Temporal Properties of Web Services
A “data-aware” web service property is a constraint on the pattern of message exchanges of a workflow where the order of messages and their data content are interdependent. The logic CTL-FO+ expresses these properties by allowing temporal operators and first-order quantification over message content to be freely mixed. A “na¨ıve” translation of CTL-FO+ into CTL leads to a serious exponential blow-up of the problem that prevents existing validation tools to be used. In this paper, we provide an alternate translation of CTL-FO+ into CTL where the construction of the workflow model depends on the property to validate. We show experimentally how this translation is significantly more efficient and makes model checking of data-aware temporal properties on real-world web service workflows tractable using off-the-shelf tools.
Sylvain Hallé, Roger Villemaire, Omar Cherk
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where WSFM
Authors Sylvain Hallé, Roger Villemaire, Omar Cherkaoui, Jérôme Tremblay, Boubker Ghandour
Comments (0)
books