The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.05 - September/October (2009 vol.35)
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
ABSTRACT
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.
INDEX TERMS
Web services, software/program verification, model checking, temporal logic.
CITATION
Sylvain Hallé, Roger Villemaire, Omar Cherkaoui, "Specifying and Validating Data-Aware Temporal Web Service Properties", IEEE Transactions on Software Engineering, vol.35, no. 5, pp. 669-683, September/October 2009, doi:10.1109/TSE.2009.29
REFERENCES
[1] G. Meredith and S. Bjorg, “Contracts and Types,” Comm. ACM, vol. 46, no. 10, pp. 41-47, 2003.
[2] S. Parastatidis, J. Webber, S. Woodman, D. Kuo, and P. Greenfield, “SOAP Service Description Language (SSDL),” Technical Report CS-TR-899, Univ. of Newcastle, Newcastle upon Tyne, 2005.
[3] G.J. Holzmann, The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003.
[4] A. Cimatti, E.M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella, “NuSMV 2: An Opensource Tool for Symbolic Model Checking,” Proc. 14th Int'l Conf. Computer Aided Verification, E. Brinksma and K.G.Larsen, eds., pp. 359-364, 2002.
[5] T. Bultan, X. Fu, R. Hull, and J. Su, “Conversation Specification: A New Approach to Design and Analysis of E-Service Composition,” Proc. Int'l World Wide Web Conf., pp.403-410, 2003.
[6] H. Foster, S. Uchitel, J. Magee, and J. Kramer, “Model-Based Analysis of Obligations in Web Service Choreography,” Proc. Int'l Conf. Internet and Web Applications and Services/Advanced Int'l Conf. Telecomm., p. 149, 2006.
[7] M. Koshkina and F. van Breugel, “Modelling and Verifying Web Service Orchestration by Means of the Concurrency Workbench,” ACM SIGSOFT Software Eng. Notes, vol. 29, no. 5, pp. 1-10, Sept. 2004.
[8] S. Hinz, K. Schmidt, and C. Stahl, “Transforming BPEL to Petri Nets,” Proc. Int'l Conf. Business Process Management, W.M.P.vander Aalst, B. Benatallah, F. Casati, and F. Curbera, eds., pp. 220-235, 2005.
[9] J.M. Zaha, M. Dumas, A. ter Hofstede, A. Barros, and G. Decker, “Service Interaction Modeling: Bridging Global and Local Views,” Proc. 10th IEEE Int'l Enterprise Distributed Object Computing Conf., pp. 45-55, 2006.
[10] A. Deutsch, L. Sui, V. Vianu, and D. Zhou, “Verification of Communicating Data-Driven Web Services,” Proc. ACM Symp. Principles of Database Systems, S. Vansummeren, ed., pp.90-99, 2006.
[11] R. Kazhamiakin, M. Pistore, and L. Santuari, “Analysis of Communication Models in Web Service Compositions,” Proc. Int'l World Wide Web Conf., L. Carr, D.D. Roure, A. Iyengar, C.A.Goble, and M. Dahlin, eds., pp. 267-276, 2006.
[12] D. Berardi, D. Calvanese, G.D. Giacomo, R. Hull, and M. Mecella, “Automatic Composition of Transition-Based Semantic Web Services with Messaging,” Proc. 31st Int'l Conf. Very Large Data Bases, K. Böhm, C.S. Jensen, L.M. Haas, M.L.Kersten, P.-Å.Larson, and B.C. Ooi, eds., pp. 613-624, 2005.
[13] Z. Duan, A.J. Bernstein, P.M. Lewis, and S. Lu, “A Model for Abstract Process Specification, Verification and Composition,” Proc. Int'l Conf. Service Oriented Computing, M. Aiello, M.Aoyama, F. Curbera, and M.P. Papazoglou, eds., pp. 232-241, 2004.
[14] N. Lohmann, P. Massuthe, C. Stahl, and D. Weinberg, “Analyzing Interacting BPEL Processes,” Proc. Int'l Conf. Business Process Management, S. Dustdar, J.L. Fiadeiro, and A.P. Sheth, eds., pp. 17-32, 2006.
[15] S. Nakajima, “Model-Checking of Safety and Security Aspects in Web Service Flows,” Proc. Int'l Conf. Web Eng., N. Koch, P.Fraternali, and M. Wirsing, eds., vol. 3140, pp. 488-501, 2004.
[16] K.J. Turner, “Formalising Web Services,” Proc. Int'l Conf. Formal Techniques for Networked and Distributed Systems, F. Wang, ed., pp.473-488, 2005.
[17] C.D. Walton, “Model Checking Multi-Agent Web Services,” Proc. Spring Symp. Semantic Web Services, Mar. 2004.
[18] A. Brogi, C. Canal, E. Pimentel, and A. Vallecillo, “Formalizing Web Service Choreographies,” Electronic Notes in Theoretical Computer Science, vol. 105, pp. 73-94, 2004.
[19] M. Pistore, M. Roveri, and P. Busetta, “Requirements-Driven Verification of Web Services,” Electronic Notes in Theoretical Computer Science, vol. 105, pp. 95-108, 2004.
[20] X. Fu, T. Bultan, and J. Su, “Analysis of Interacting BPEL Web Services,” Proc. Int'l World Wide Web Conf., S.I. Feldman, M.Uretsky, M. Najork, and C.E. Wills, eds., pp. 621-630, 2004.
[21] X. Fu, T. Bultan, and J. Su, “Model Checking XML Manipulating Software,” Proc. Int'l Symp. Software Testing and Analysis, G.S.Avrunin and G. Rothermel, eds., pp. 252-262, 2004.
[22] J. Arias-Fisteus, L.S. Fernández, and C.D. Kloos, “Applying Model Checking to BPEL4WS Business Collaborations,” Proc. 2005 ACM Symp. Applied Computing, H. Haddad, L.M. Liebrock, A.Omicini, and R.L. Wainwright, eds., pp. 826-830, 2005.
[23] J.E. Johnson, D.E. Langworthy, L. Lamport, and F.H. Vogt, “Formal Specification of a Web Services Protocol,” Electronic Notes in Theoretical Computer Science, vol. 105, pp. 147-158, 2004.
[24] A. Deutsch, L. Sui, and V. Vianu, “Specification and Verification of Data-Driven Web Services,” Proc. ACM Symp. Principles of Database Systems, A. Deutsch, ed., pp. 71-82, 2004.
[25] S. Abiteboul, L. Segoufin, and V. Vianu, “Static Analysis of Active XML Systems,” Proc. ACM Symp. Principles of Database Systems, M. Lenzerini and D. Lembo, eds., pp. 221-230, 2008.
[26] C.E. Gerede and J. Su, “Specification and Verification of Artifact Behaviors in Business Process Models,” Proc. Int'l Conf. Service Oriented Computing, B.J. Krämer, K.-J. Lin, and P.Narasimhan, eds., vol. 4749, pp. 181-192, 2007.
[27] L. Baresi, D. Bianculli, C. Ghezzi, S. Guinea, and P. Spoletini, “Validation of Web Service Compositions,” IET Software, vol. 1, pp. 219-232, 2007.
[28] R. Boutaba, W. Golab, Y. Iraqi, and B.S. Arnaud, “Lightpaths on Demand: A Web-Services-Based Management System,” IEEE Comm. Magazine, vol. 42, no. 7, pp. 101-107, July 2004.
[29] S. Hallé, R. Villemaire, O. Cherkaoui, J. Tremblay, and B. Ghandour, “Extending Model Checking to Data-Aware Temporal Properties of Web Services,” Proc. Web Services and Formal Methods, M. Dumas and R. Heckel, eds., vol.4937, pp.31-45, 2007.
[30] J. Josephraj, “Web Services Choreography in Practice,” http://www-128.ibm.com/developerworks/webservices/ libraryws-choreography/, 2005.
[31] S. Hallé and R. Villemaire, “Runtime Monitoring of Message-Based Workflows with Data,” Proc. 12th IEEE Int'l Enterprise Distributed Object Computing Conf., pp. 67-83, 2008.
[32] J.E. Hopcroft, R. Motwani, and J.D. Ullman, Introduction to Automata Theory, Languages, and Computation, second ed. Addison Wesley, 2000.
[33] H. Foster, S. Uchitel, J. Magee, and J. Kramer, “Model-Based Verification of Web Service Compositions,” Proc. IEEE Int'l Conf. Automated Software Eng., pp. 152-163, 2003.
[34] C. Ouyang, E. Verbeek, W.M.P. van der Aalst, S. Breutel, M. Dumas, and A.H.M. ter Hofstede, “Formal Semantics and Analysis of Control Flow in WS-BPEL,” Science of Computer Programming, vol. 67, nos. 2/3, pp. 162-198, 2007.
[35] R. Lucchi and M. Mazzara, “A Pi-Calculus Based Semantics for WS-BPEL,” J. Logic and Algebraic Programming, vol. 70, no. 1, pp.96-118, 2007.
[36] J. Arias-Fisteus, A. Marin, and C.D. Kloos, “VERBUS: A Formal Model for Business Process Verification,” Proc. Information Resources Management Assoc., May 2004.
[37] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. MIT Press, 2000.
[38] P. Schnoebelen, “The Complexity of Temporal Logic Model Checking,” Advances in Modal Logic, vol. 4, pp. 393-436, http://citeseer.ist.psu.eduschnoebelen03complexity.html , 2003.
[39] O. Kupferman, “Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions,” Proc. Int'l Conf. Computer Aided Verification, P. Wolper, ed., vol. 939, pp. 325-338, http://www.cs.huji.ac.il/ornakpub.html, 1995.
[40] A. Rensink, “Model Checking Quantified Computation Tree Logic,” Proc. Int'l Conf. Concurrency Theory, C. Baier and H.Hermanns, eds., pp. 110-125, 2006.
[41] W.M. van der Aalst and M. Pesic, “DecSerFlow: Towards a Truly Declarative Service Flow Language,” Proc. Conf. Web Services and Formal Methods, M. Bravetti, M. Núñez, and G. Zavattaro, eds., pp. 1-23, 2006.
[42] M. Brambilla, A. Deutsch, L. Sui, and V. Vianu, “The Role of Visual Tools in a Web Application Design and Verification Framework: A Visual Notation for LTL Formulae,” Proc. Int'l Conf. Web Eng., D. Lowe and M. Gaedke, eds., pp. 557-568, 2005.
[43] H. Barringer, A. Goldberg, K. Havelund, and K. Sen, “Rule-Based Runtime Verification,” Proc. Int'l Conf. Verification, Model Chacking, and Abstract Interpretation, B. Steffen and G. Levi, eds., pp. 44-57, 2004.
[44] M.R.A. Huth and M.D. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge Univ. Press, citeseer.ist. psu.eduhuth99logic.html, 2000.
[45] T. Ball and S.K. Rajamani, “Boolean Programs: A Model and Process for Software Analysis,” Technical Report MSR-TR-2000-14, Microsoft Research, Feb. 2000.
[46] M.R. Garey and D.S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman, 1979.
[47] R. Alur and T.A. Henzinger, “A Really Temporal Logic,” J. ACM, vol. 41, no. 1, pp. 181-204, 1994.
28 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool