Constellation, le dépôt institutionnel de l'Université du Québec à Chicoutimi

Extending model checking to data-aware temporal properties of web services

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.

[thumbnail of shrvocjtbg-wsfm07.pdf]
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
Afficher les statistiques de telechargements

Éditer le document (administrateurs uniquement)

Creative Commons LicenseSauf indication contraire, les documents archivés dans Constellation sont rendus disponibles selon les termes de la licence Creative Commons "Paternité, pas d'utilisation commerciale, pas de modification" 2.5 Canada.

Bibliothèque Paul-Émile-Boulet, UQAC
555, boulevard de l'Université
Chicoutimi (Québec)  CANADA G7H 2B1
418 545-5011, poste 5630