This Article 
 Bibliographic References 
 Add to: 
Runtime Enforcement of Web Service Message Contracts with Data
Second 2012 (vol. 5 no. 2)
pp. 192-206
Sylvain Hallé, Université du Québec à Chicoutimi, Chicoutimi
Roger Villemaire, Université du Québec à Chicoutimi, Chicoutimi
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 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.

[1] E. Christensen, F. Curbera, G. Meredith, and S. Weerawarana, "Web Services Description Language (WSDL) 1.1, W3C Note,", 2001.
[2] E. Schonfeld, "Amazon Earnings Call Details: Web Services Use Up More Bandwidth than; the Kindle Is a Hit," http://tcrn.chcaKitG, 2008.
[3] "Amazon E-Commerce Service," com/AWSECommerceService AWSECommerceService.wsdl, 2005.
[4] "Amazon Fulfillment Web Service," http://docs.amazonweb 1.0DeveloperGuide, 2005.
[5] "Google Checkout APIs,", 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. , 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.

Index Terms:
Web services, runtime monitoring, temporal logic.
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
Usage of this product signifies your acceptance of the Terms of Use.