LiveZilla Live Chat Software

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

Specifying and validating data-aware temporal web service properties

Hallé Sylvain, Villemaire Roger et Cherkaoui Omar. (2009). Specifying and validating data-aware temporal web service properties. IEEE Transactions on Software Engineering, 35, (5), p. 669-683.

[img]
Prévisualisation
PDF
342kB

URL officielle: http://dx.doi.org/10.1109/TSE.2009.29

Résumé

Most works that extend workflow validation beyond syntactical checking consider constraints on the sequence of messages exchanged between services. These constraints are expressed only in terms of message names and abstract away their actual data content. We provide examples of real-world “data-aware” web service constraints where the sequence of messages and their content are interdependent. To this end, we present CTL-FO+, an extension over Computation Tree Logic that includes first-order quantification on message content in addition to temporal operators. We show how CTL-FO+ is adequate for expressing data-aware constraints, give a sound and complete model checking algorithm for CTL-FO+ and establish its complexity to be PSPACE-complete. 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. 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 for complex formulæ 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
ISSN:0098-5589
Volume:35
Numéro:5
Pages:p. 669-683
Version évaluée par les pairs:Oui
Date:2009
Identifiant unique:10.1109/TSE.2009.29
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, software/program verification, model checking, temporal logic
Déposé le:11 avr. 2013 00:04
Dernière modification:24 mai 2016 14:56
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