The Community for Technology Leaders
Green Image
Issue No. 05 - September/October (2009 vol. 35)
ISSN: 0098-5589
pp: 669-683
Sylvain Hallé , University of California, Santa Barbara, Santa Barbara
Roger Villemaire , Université du Québec à Montréal, Montréal
Omar Cherkaoui , Université du Québec à Montréal, Montréal
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 {\rm CTL}\hbox{-}{\rm FO}^+, an extension over Computation Tree Logic that includes first-order quantification on message content in addition to temporal operators. We show how {\rm CTL}\hbox{-}{\rm FO}^+ is adequate for expressing data-aware constraints, give a sound and complete model checking algorithm for {\rm CTL}\hbox{-}{\rm FO}^+, and establish its complexity to be PSPACE-complete. A “naive” translation of {\rm CTL}\hbox{-}{\rm FO}^+ into CTL leads to a serious exponential blowup of the problem that prevents existing validation tools to be used. We provide an alternate translation of {\rm CTL}\hbox{-}{\rm 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 formulas and makes model checking of data-aware temporal properties on real-world Web service workflows tractable using off-the-shelf tools.
Web services, software/program verification, model checking, temporal logic.

O. Cherkaoui, S. Hallé and R. Villemaire, "Specifying and Validating Data-Aware Temporal Web Service Properties," in IEEE Transactions on Software Engineering, vol. 35, no. , pp. 669-683, 2009.
97 ms
(Ver 3.3 (11022016))