Hallé Sylvain, Villemaire Roger, Cherkaoui Omar, Tremblay Jérôme et Ghandour Boubker. (2008). Extending model checking to data-aware temporal properties of web services. Lecture Notes in Computer Science, 4937, p. 31-45.
Prévisualisation |
PDF
208kB |
URL officielle: http://dx.doi.org/10.1007/978-3-540-79230-7_3
Résumé
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.
Type de document: | Article publié dans une revue avec comité d'évaluation |
---|---|
Volume: | 4937 |
Pages: | p. 31-45 |
Version évaluée par les pairs: | Oui |
Date: | 2008 |
Identifiant unique: | 10.1007/978-3-540-79230-7_3 |
Sujets: | Sciences naturelles et génie > Sciences mathématiques > Informatique |
Département, module, service et unité de recherche: | Départements et modules > Département d'informatique et de mathématique |
Mots-clés: | web services, formal methods, temporal logic, model checking, LTL-FO+ |
Déposé le: | 11 avr. 2013 00:38 |
---|---|
Dernière modification: | 11 avr. 2013 00:38 |
Éditer le document (administrateurs uniquement)