The Community for Technology Leaders
RSS Icon
Issue No.02 - April-June (2013 vol.6)
pp: 262-275
Aysu Betin-Can , Middle East Tehcnical University, Ankara
Sylvain Halle , University of Quebec at Chicoutimi, Chicoutimi
Tevfik Bultan , University of California at Santa Barbara, Santa Barbara
A crucial problem in service-oriented computing is the specification and analysis of interactions among multiple peers that communicate via messages. We propose a design pattern that enables the specification of behavioral interfaces acting as communication contracts between peers. This "peer controller pattern” provides a modular, assume-guarantee style verification strategy that consists of three phases. 1) Each individual peer is statically verified for conformance to its part of the contract, using software model checking. 2) Alternately, a runtime enforcement mechanism blocks the communication events that violate the interface specification at runtime. 3) Using either of these two mechanisms, it can be assumed that the participating peers behave according to their interfaces and safety and liveness properties about the global behavior of the composite web service can then be verified directly on the communication contract. The interface verification of each peer and the behavior verification are hence handled in separate steps. A Java implementation of this pattern is developed and tested on a series of examples; we show that by working in such a modular fashion, it is possible to automatically and efficiently verify properties about service interactions that would otherwise be impossible to verify.
Web services, Contracts, Runtime, XML, Java, Monitoring, Asynchronous communication,design patterns, Web services, automated verification, runtime enforcement, asynchronous communication
Aysu Betin-Can, Sylvain Halle, Tevfik Bultan, "Modular Verification of Asynchronous Service Interactions Using Behavioral Interfaces", IEEE Transactions on Services Computing, vol.6, no. 2, pp. 262-275, April-June 2013, doi:10.1109/TSC.2011.55
[1] " Q4 2007 Earnings Call Transcript," http:// , 2013.
[2] A. Brown, M. Fuchs, J. Robie, and P. Wadler, "MSL: A Model for W3C XML Schema," Proc. 10th Int'l World Wide Web Conf., pp. 191-200, 2001.
[3] D. Brand and P. Zafiropulo, "On Communicating Finite-State Machines," J. ACM, vol. 30, no. 2, pp. 323-342, 1983.
[4] X. Fu, T. Bultan, and J. Su, "Synchronizability of Conversations among Web Services," IEEE Trans. Software Eng., vol. 31, no. 12, pp. 1042-1055, Dec. 2005.
[5] S. Hallé and R. Villemaire, "Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep," Proc. 21st Int'l Conf. Computer Aided Verification, pp. 648-653, 2009.
[6] A. Deutsch, L. Sui, V. Vianu, and D. Zhou, "Verification of Communicating Data-Driven Web Services," Proc. 25th ACM SIGACT-SIGMOD-SIGART Symp. Principles Database Systems, pp. 90-99, 2006.
[7] T. Andrews, F. Curbera, H. Dholakia, Y. Goland, J. Klein, F. Leymann, K. Liu, D. Roller, D. Smith, S. Thatte, I. Trickovic, and S. Weerawarana, "Business Process Execution Language for Web Services, Version 1.1," developerworks/library ws-bpel/, 2003.
[8] E. Jendrock, J. Ball, D. Carson, I. Evans, S. Fordin, and K. Haase, The Java EE 5 Tutorial, third ed. Prentice Hall, 2006.
[9] T. Bultan and A. Betin-Can, "Scalable Software Model Checking Using Design for Verification," Proc. IFIP TC 2/WG 2.3 Conf. Verified Software: Theories, Tools, Experiments, vol. 4171, pp. 337-346, 2005.
[10] S. Hallé, R. Villemaire, and O. Cherkaoui, "Specifying and Validating Data-Aware Temporal Web Service Properties," IEEE Trans. Software Eng., vol. 35, no. 6, pp. 669-683, Nov./Dec. 2009.
[11] G. Decker, J.M. Zaha, and M. Dumas, "Execution Semantics for Service Choreographies," Proc. Third Int'l Workshop Web Services and Formal Methods, pp. 163-177, 2006.
[12] G. Brat, K. Havelund, S. Park, and W. Visser, "Java Pathfinder: Second Generation of a Java Model Checker," Proc. Workshop Advances in Verification, 2000.
[13] G.J. Holzmann, The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2003.
[14] A. Betin-Can, T. Bultan, and X. Fu, "Design for Verification for Asynchronously Communicating Web Services," Proc. 14th Int'l Conf. World Wide Web, pp. 750-759, 2005.
[15] F. Leymann, "Web Services Flow Language (WSFL), Version 1.0," standards leymann-wsfl01.pdf, 2001.
[16] M. Baldoni, C. Baroglio, A. Martelli, and V. Patti, "Reasoning about Interaction Protocols for Web Service Composition," Electronic Notes Theoretical Computer Science, vol. 105, pp. 21-36, 2004.
[17] D. Berardi, D. Calvanese, G.D. Giacomo, M. Lenzerini, and M. Mecella, "Automatic Composition of e-Services That Export Their Behavior," Proc. First Int'l Conf. Service-Oriented Computing, pp. 43-58, 2003.
[18] B. Benatallah, Q.Z. Sheng, A.H.H. Ngu, and M. Dumas, "Declarative Composition and Peer-to-Peer Provisioning of Dynamic Web Services," Proc. 18th Int'l Conf. Data Eng., pp. 297-308, 2002.
[19] S. Nakajima, "Verification of Web Service Flows with Model-Checking Techniques," Proc. Int'l Symp. Cyber Worlds, p. 378, 2002.
[20] J. Arias-Fisteus, L.S. Fernández, and C.D. Kloos, "Applying Model Checking to BPEL4WS Business Collaborations," Proc. ACM Symp. Applied Computing, pp. 826-830, 2005.
[21] H. Foster, S. Uchitel, J. Magee, and J. Kramer, "Model-Based Verification of Web Service Compositions," Proc. 18th IEEE Int'l Conf. Automated Software Eng., pp. 152-163, 2003.
[22] S. Narayanan and S.A. McIlraith, "Simulation, Verification and Automated Composition of Web Services," Proc. 11th Int'l World Wide Web Conf., pp. 77-88, 2002.
[23] B.-H. Schlingloff, A. Martens, and K. Schmidt, "Modeling and Model Checking Web Services," Electronic Notes Theoretical Computer Science, vol. 126, pp. 3-26, 2005.
[24] N. Lohmann, P. Massuthe, C. Stahl, and D. Weinberg, "Analyzing Interacting BPEL Processes," Proc. Fourth Int'l Conf. Business Process Management, pp. 17-32, 2006.
[25] L. de Alfaro and T.A. Henzinger, "Interface Automata," Proc. Eighth European Software Eng. Conf. Held Jointly with Ninth ACM SIGSOFT Int'l Symp. Foundations of Software Eng., pp. 109-120, 2001.
[26] D. Beyer, A. Chakrabarti, and T.A. Henzinger, "Web Service Interfaces," Proc. 14th Int'l Conf. World Wide Web, pp. 148-159, 2005.
[27] S.K. Rajamani and J. Rehof, "Conformance Checking for Models of Asynchronous Message Passing Software," Proc. 14th Int'l Conf. Computer Aided Verification, pp. 166-179, 2002.
[28] M. Rouached, O. Perrin, and C. Godart, "Towards Formal Verification of Web Service Composition," Proc. Fourth Int'l Conf. Business Process Management, pp. 257-273, 2006.
[29] C. Flanagan and S. Qadeer, "Thread-Modular Model Checking," Proc. 10th Int'l SPIN Workshop, pp. 213-224, 2003.
[30] C. Colby, P. Godefroid, and L.J. Jagadeesan, "Automatically Closing Open Reactive Programs," Proc. 1998 ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 345-357, 1998.
[31] S.D. Stoller and Y.A. Liu, "Transformations for Model Checking Distributed Java Programs," Proc. Eighth Int'l SPIN Workshop, pp. 192-199, 2001.
[32] O. Tkachuk, M.B. Dwyer, and C.S. Pasareanu, "Automated Environment Generation for Software Model Checking," Proc. 18th IEEE Int'l Conf. Automated Software Engineering, pp. 116-129, 2003.
[33] A. Betin-Can and T. Bultan, "Verifiable Concurrent Programming Using Concurrency Controllers," Proc. 19th IEEE Int'l Conf. Automated Software Eng., pp. 248-257, 2004.
[34] M. Hills and G. Rosu, "A Rewriting Approach to the Design and Evolution of Object-Oriented Languages," Proc. 22nd Ann. ACM SIGPLAN Conf. Object-Oriented Programming, Systems, Languages, and Applications, pp. 827-828, 2007.
[35] 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, pp. 63-71, 2006.
[36] L. Baresi, D. Bianculli, C. Ghezzi, S. Guinea, and P. Spoletini, "Validation of Web Service Compositions," IET Software, vol. 1, pp. 219-232, 2007.
30 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool