The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - Second (2012 vol.5)
pp: 192-206
Sylvain Hallé , Université du Québec à Chicoutimi, Chicoutimi
Roger Villemaire , Université du Québec à Chicoutimi, Chicoutimi
ABSTRACT
An increasing number of popular SOAP web services exhibit a stateful behavior, where a successful interaction is determined as much by the correct format of messages as by the sequence in which they are exchanged with a client. The set of such constraints forms a "message contract” that needs to be enforced on both sides of the transaction; it often includes constraints referring to actual data elements inside messages. We present an algorithm for the runtime monitoring of such message contracts with data parameterization. Their properties are expressed in {\rm LTL}\hbox{-}{\rm FO}^+, an extension of Linear Temporal Logic that allows first-order quantification over the data inside a trace of XML messages. An implementation of this algorithm can transparently enforce an {\rm LTL}\hbox{-}{\rm FO}^+ specification using a small and invisible Java applet. Violations of the specification are reported on-the-fly and prevent erroneous or out-of-sequence XML messages from being exchanged. Experiments on commercial web services from Amazon.com and Google indicate that {\rm LTL}\hbox{-}{\rm FO}^+ is an appropriate language for expressing their message contracts, and that its processing overhead on sample traces is acceptable both for client-side and server-side enforcement architectures.
INDEX TERMS
Web services, runtime monitoring, temporal logic.
CITATION
Sylvain Hallé, Roger Villemaire, "Runtime Enforcement of Web Service Message Contracts with Data", IEEE Transactions on Services Computing, vol.5, no. 2, pp. 192-206, Second 2012, doi:10.1109/TSC.2011.10
REFERENCES
[1] E. Christensen, F. Curbera, G. Meredith, and S. Weerawarana, "Web Services Description Language (WSDL) 1.1, W3C Note," http://www.w3.org/TRwsdl, 2001.
[2] E. Schonfeld, "Amazon Earnings Call Details: Web Services Use Up More Bandwidth than Amazon.com; the Kindle Is a Hit," http://tcrn.chcaKitG, 2008.
[3] "Amazon E-Commerce Service," http://webservices.amazon. com/AWSECommerceService AWSECommerceService.wsdl, 2005.
[4] "Amazon Fulfillment Web Service," http://docs.amazonweb services.com/AWSFWS/ 1.0DeveloperGuide, 2005.
[5] "Google Checkout APIs," http://code.google.com/apischeckout, 2009.
[6] C. Ghezzi and S. Guinea, "Run-Time Monitoring in Service-Oriented Architectures," Test and Analysis of Web Services, pp. 237-264, Springer, 2007.
[7] K. Mahbub and G. Spanoudakis, "Monitoring WS-Agreements: An Event Calculus-Based Approach," Test and Analysis of Web Services, pp. 265-306, Springer, 2007.
[8] S. Hallé, R. Villemaire, and O. Cherkaoui, "Specifying and Validating Data-Aware Temporal Web Service Properties," IEEE Trans. Software Eng., vol. 35, no. 5, pp. 669-683, Sept./Oct. 2009.
[9] S. Hallé, G. Hughes, T. Bultan, and M. Alkhalaf, "Generating Interface Grammars from WSDL for Automated Verification of Web Services," Proc. Seventh Int'l Joint Conf. Service-Oriented Computing (ICSOC-ServiceWave), L. Baresi, C.-H. Chi, and J. Suzuki, eds., pp. 516-530, 2009.
[10] G. Alonso, F. Casati, H. Kuno, and V. Machiraju, Web Services, Concepts, Architectures and Applications. Springer, 2004.
[11] K. Mahbub and G. Spanoudakis, "Run-Time Monitoring of Requirements for Systems Composed of Web-Services: Initial Implementation and Evaluation Experience," Proc. IEEE Int'l Conf. Web Services (ICWS), pp. 257-265, 2005.
[12] Y. Gan, M. Chechik, S. Nejati, J. Bennett, B. O'Farrell, and J. Waterhouse, "Runtime Monitoring of Web Service Conversations," Proc. Conf. Center for Advanced Studies on Collaborative Research (CASCON '07), pp. 42-57, 2007.
[13] F. Barbon, P. Traverso, M. Pistore, and M. Trainotti, "Run-Time Monitoring of Instances and Classes of Web Service Compositions," Proc. IEEE Int'l Conf. Web Services (ICWS), pp. 63-71, 2006.
[14] W.N. Robinson, "Monitoring Web Service Requirements," Proc. IEEE Int'l Requirements Eng. Conf., pp. 65-74, Sept. 2003.
[15] S. Nakajima, "Lightweight Formal Analysis of Web Service Flows," Progress in Informatics, vol. 2, pp. 57-76, 2005.
[16] X. Fu, T. Bultan, and J. Su, "Analysis of Interacting BPEL Web Services," Proc. 13th Int'l Conf. World Wide Web (WWW), S.I. Feldman, M. Uretsky, M. Najork, and C.E. Wills, eds., pp. 621-630, 2004.
[17] W. Robinson, "A Requirements Monitoring Framework for Enterprise Systems," Requirements Eng., vol. 11, no. 1, pp. 17-41, 2006.
[18] M. Caporuscio, P. Inverardi, and P. Pelliccione, "Compositional Verification of Middleware-Based Software Architecture Descriptions," Proc. 26th Int'l Conf. Software Eng. (ICSE), pp. 221-230, 2004.
[19] 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.
[20] G. Decker, J.M. Zaha, and M. Dumas, "Execution Semantics for Service Choreographies," Proc. Int'l Workshop Web Services and Formal Methods (WS-FM), M. Bravetti, M. Núñez, and G. Zavattaro, eds., pp. 163-177, 2006.
[21] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. MIT Press, 2000.
[22] G. Governatori, Z. Milosevic, and S.W. Sadiq, "Compliance Checking between Business Processes and Business Contracts," Proc. IEEE Conf. Enterprise Distributed Object Computing (EDOC), pp. 221-232, 2006.
[23] H. Barringer, A. Goldberg, K. Havelund, and K. Sen, "Rule-Based Runtime Verification," Proc. Int'l Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI), B. Steffen and G. Levi, eds., pp. 44-57, 2004.
[24] M.Y. Vardi, "An Automata-Theoretic Approach to Linear Temporal Logic," Proc. Banff Higher Order Workshop, F. Moller and G.M. Birtwistle, eds., pp. 238-266, 1995.
[25] A. Bauer, M. Leucker, and C. Schallhart, "Monitoring of Real-Time Properties," Proc. Int'l Conf. Foundations of Software Technology and Theoretical Computer Science (FSTTCS), S. Arun-Kumar and N. Garg, eds., pp. 260-272, 2006.
[26] R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper, "Simple On-the-Fly Automatic Verification of Linear Temporal Logic," Proc. Symp. Protocol Specification, Testing and Verification (PSTV), P. Dembinski and M. Sredniawa, eds., vol. 38, pp. 3-18, 1995.
[27] I.H. Krüger, M. Meisinger, and M. Menarini, "Runtime Verification of Interactions: From MSCs to Aspects," Proc. Int'l Workshop Runtime Verification (RV), O. Sokolsky and S. Tasiran, eds., pp. 63-74, 2007.
[28] J.H. Gallier, Logic for Computer Science: Foundation of Automatic Theorem Proving, Longman Higher Education, http://www.cis. upenn.edu/jean/gbookslogic.html , 1986.
[29] A. Bauer, M. Leucker, and C. Schallhart, "The Good, the Bad, and the Ugly, But How Ugly Is Ugly?" Proc. Seventh Int'l Conf. Runtime Verification (RV), O. Sokolsky and S. Tasiran, eds., pp. 126-138, 2007.
[30] G. Rosu, F. Chen, and T. Ball, "Synthesizing Monitors for Safety Properties: This Time with Calls and Returns," Proc. Int'l Conf. Runtime Verification (RV), M. Leucker, ed., pp. 51-68, 2008.
[31] Y. Falcone, J.-C. Fernandez, and L. Mounier, "Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties," Proc. Int'l Conf. Information Systems Security (ICISS), R. Sekar and A.K. Pujari, eds., pp. 41-55, 2008.
[32] J. Ligatti, L. Bauer, and D. Walker, "Edit Automata: Enforcement Mechanisms for Run-Time Security Policies," Int'l J. Information Security, vol. 4, nos. 1/2, pp. 2-16, 2005.
[33] F.B. Schneider, "Enforceable Security Policies," ACM Trans. Information and System Security, vol. 3, no. 1, pp. 30-50, 2000.
[34] R. Alur and D.L. Dill, "A Theory of Timed Automata," Theoretical Computer Science, vol. 126, pp. 183-235, 1994.
[35] J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi, "UPPAAL-A Tool Suite for Automatic Verification of Real-Time Systems," Proc. DIMACS/SYCON Workshop Hybrid Systems, R. Alur, T.A. Henzinger, and E.D. Sontag, eds., pp. 232-243, 1995.
[36] C. Constant, T. Jéron, H. Marchand, and V. Rusu, "Integrating Formal Verification and Conformance Testing for Reactive Systems," IEEE Trans. Software Eng., vol. 33, no. 8, pp. 558-574, Aug. 2007.
[37] K. Havelund and G. Rosu, "Testing Linear Temporal Logic Formulæ on Finite Execution Traces," technical report, May 2001.
[38] F. Massacci and K. Naliuka, "Multi-Session Security Monitoring for Mobile Code," Technical Report DIT-06-067, Nov. 2006.
[39] A. Pretschner, M. Büchler, M. Harvan, C. Schaefer, and T. Walter, "Usage Control Enforcement with Data Flow Tracking for X11," Proc. Fifth Int'l Workshop Security and Trust Management (STM), pp. 124-137, 2009.
[40] V. Stolz, "Temporal Assertions with Parametrised Propositions," Proc. Int'l Conf. Runtime Verification (RV), O. Sokolsky and S. Tasiran, eds., pp. 176-187, 2007.
[41] F. Wang, S. Tahar, and O.A. Mohamed, "First-Order LTL Model Checking Using Mdgs," Proc. Int'l Symp. Automated Technology for Verification and Analysis (ATVA), F. Wang, ed., pp. 441-455, 2004.
[42] H. Barringer, D. Rydeheard, and K. Havelund, "Rule Systems for Run-Time Monitoring: From Eagle to RuleR," J. Logic and Computation, pp. 675-706, 2008.
[43] I.M. Hodkinson, "Complexity of Monodic Guarded Fragments over Linear and Real Time," Annals Pure and Applied Logic, vol. 138, nos. 1-3, pp. 94-125, 2006.
[44] A. Deutsch, L. Sui, V. Vianu, and D. Zhou, "Verification of Communicating Data-Driven Web Services," Proc. ACM SIGMOD-SIGACT-SIGART Symp. Principles of Database Systems (PODS), S. Vansummeren, ed., pp. 90-99, 2006.
[45] C.E. Gerede and J. Su, "Specification and Verification of Artifact Behaviors in Business Process Models," Proc. Fifth Int'l Conf. Service-Oriented Computing (ICSOC), B.J. Krämer, K.-J. Lin, and P. Narasimhan, eds., pp. 181-192, 2007.
[46] M. Venzke, "Specifications Using XQuery Expressions on Traces," Electronic Notes in Theoretical Computer Science, vol. 105, pp. 109-118, 2004.
[47] S. Hallé and R. Villemaire, "Runtime Monitoring of Web Service Choreographies Using Streaming XML," Proc. ACM Symp. Applied Computing (SAC), pp. 1851-1858, 2009.
[48] C. Fritz, "Concepts of Automata Construction from LTL," Proc. Int'l Conf. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), G. Sutcliffe and A. Voronkov, eds., pp. 728-742, 2005.
[49] P. Gastin and D. Oddoux, "Fast LTL to Büchi Automata Translation," Proc. Int'l Conf. Computer Aided Verification (CAV), G. Berry, H. Comon, and A. Finkel, eds., pp. 53-65, 2001.
[50] O. Sokolsky and S. Tasiran, eds., Runtime Verification, Seventh Int'l Workshop, RV 2007, Vancover, Canada, March 13, 2007, Revised Selected Papers. Springer 2007.
13 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool