The Community for Technology Leaders
RSS Icon
Issue No.03 - July-September (2009 vol.2)
pp: 223-244
Jocelyn Simmonds , University of Toronto, Toronto
Yuan Gan , IBM Toronto Lab, Markham
Marsha Chechik , University of Toronto, Toronto
Shiva Nejati , Simula Research Laboratory, Lysaker
Bill O'Farrell , IBM Toronto Lab, Markham
Elena Litani , IBM Toronto Lab, Markham
Julie Waterhouse , IBM Toronto Lab, Markham
For a system of distributed processes, correctness can be ensured by (statically) checking whether their composition satisfies properties of interest. However, Web services are distributed processes that dynamically discover properties of other Web services. Since the overall system may not be available statically and since each business process is supposed to be relatively simple, we propose to use runtime monitoring of conversations between partners as a means of checking behavioral correctness of the entire Web service system. Specifically, we identify a subset of UML 2.0 Sequence Diagrams as a property specification language and show that it is sufficiently expressive for capturing safety and liveness properties. By transforming these diagrams to automata, we enable conformance checking of finite execution traces against the specification. We show how our language can be used to specify the Specification Property System (SPS) [1]. We describe an implementation of our approach as part of an industrial system. Finally, we discuss our experience of specifying and monitoring a number of properties from three existing applications.
Nondeterministic finite automata, runtime monitoring, sequence diagrams, temporal logic patterns, Web service conversations.
Jocelyn Simmonds, Yuan Gan, Marsha Chechik, Shiva Nejati, Bill O'Farrell, Elena Litani, Julie Waterhouse, "Runtime Monitoring of Web Service Conversations", IEEE Transactions on Services Computing, vol.2, no. 3, pp. 223-244, July-September 2009, doi:10.1109/TSC.2009.16
[1] M. Dwyer, G. Avrunin, and J. Corbett, “Patterns in Property Specifications for Finite-State Verification,” Proc. 21st Int'l Conf. Software Eng. (ICSE '99), pp. 411-420, May 1999.
[2] OASIS, Web Services Business Process Execution Language Version 2.0, wsbpel-v2.0-OS.html, Jan. 2009.
[3] X. Fu, T. Bultan, and J. Su, “Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services,” Proc. Eighth Int'l Conf. Implementation and Application of Automata (CIAA '03), pp. 188-200, July 2003.
[4] X. Fu, T. Bultan, and J. Su, “Analysis of Interacting BPEL Web Services,” Proc. 13th Int'l World Wide Web Conf. (WWW '04), pp.621-630, May 2004.
[5] R. Kazhamiakin and M. Pistore, “A Parametric Communication Model for the Verification of BPEL4WS Compositions,” Proc. Int'l Workshop Web Services and Formal Methods (WS-FM '05), pp. 318-332, 2005.
[6] M. Baldoni, C. Baroglio, A. Martelli, V. Patti, and C. Schifanella, “Verifying the Conformance of Web Services to Global Interaction Protocols: A First Step,” Proc. Int'l Workshop Web Services and Formal Methods (WS-FM '05), pp. 257-271, 2005.
[7] 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. (ASE '03), pp. 152-163, 2003.
[8] N. Ghafari, A. Gurfinkel, N. Klarlund, and R. Trefler, “Algorithmic Analysis of Piecewise FIFO Systems,” Proc. Seventh Int'l Conf. Formal Methods in Computer-Aided Design (FMCAD '07), pp. 45-52, Nov. 2007.
[9] L.K. Dillon, G. Kutty, L.E. Moser, P.M. Melliar-Smith, and Y.S. Ramakrishna, “A Graphical Interval Logic for Specifying Concurrent Systems,” ACM Trans. Software Eng. and Methodology (TOSEM), vol. 3, no. 2, pp. 131-165, 1994.
[10] M. Smith, G. Holzmann, and K. Etessami, “Events and Constraints: A Graphical Editor for Capturing Logic Requirements of Programs,” Proc. Fifth IEEE Int'l Symp. Requirements Eng. (RE '01), pp. 14-22, Aug. 2001.
[11] ITU-TS, “ITU-TS Recommendation Z.120: Message Sequence Chart 1996 (MSC96),” technical report, ITU-TS, Geneva, 1996.
[12] W. Damm and D. Harel, “LSCs: Breathing Life into Message Sequence Charts,” J. Formal Methods in System Design (FMSD), vol. 19, no. 1, pp. 45-80, 2001.
[13] Object Management Group (OMG), Unified Modeling Language (UML 2.0),, Jan. 2009.
[14] Object Management Group (OMG), Object Constraint Language (OCL 2.0),, Jan. 2009.
[15] R. Alur and M. Yannakakis, “Model Checking of Message Sequence Charts,” Proc. 10th Int'l Conf. Concurrency Theory (CONCUR '99), pp. 114-129, 1999.
[16] D. Harel and S. Maoz, “Assert and Negate Revisited: Modal Semantics for UML Sequence Diagrams,” Proc. Int'l Conf. Software Eng. (ICSE '06) Workshop Scenarios and State Machines (SCESM '06), pp. 13-20, 2006.
[17] R. Grosu and S.A. Smolka, “Safety-Liveness Semantics for UML 2.0 Sequence Diagrams,” Proc. Fifth Int'l Conf. Application of Concurrency to System Design (ACSD '05), pp. 6-14, 2005.
[18] M. Autili, P. Inverardi, and P. Pelliccione, “A Scenario Based Notation for Specifying Temporal Properties,” Proc. Int'l Conf. Software Eng. (ICSE '06) Workshop Scenarios and State Machines (SCESM '06), 2006.
[19] J.E. Hopcroft and J.D. Ullman, Introduction to Automata Theory Languages and Computation. Addison Wesley, 1979.
[20] H. Störrle, “Assert, Negate and Refinement in UML 2 Interactions,” Proc. Unified Modeling Language (UML '03) Workshop Critical Systems Development with UML, pp. 79-94, 2003.
[21] M. Vardi, “An Automata-Theoretic Approach to Linear Temporal Logic,” Proc. Eighth Banff Higher Order Workshop, pp. 238-266, Aug. 1996.
[22] IBM, IBM Rational Software Architect, software/awdtools/architect swarchitect, Jan. 2008.
[23] M.B. Dwyer, G.S. Avrunin, and J.C. Corbett, “Property Specification Patterns for Finite-State Verification,” Proc. Second Workshop Formal Methods in Software Practice (FMSP '98), Mar. 1998.
[24] E. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 1999.
[25] J. Yu, T.P. Manh, J. Han, Y. Jin, Y. Han, and J. Wang, “Pattern Based Property Specification and Verification for Service Composition,” Proc. Seventh Int'l Conf. Web Information Systems Eng. (WISE '06), pp. 156-168, 2006.
[26] IBM, WebSphere Business Integration Software, http://www-306. index.jsp?tab=productsbusinessint , Jan. 2009.
[27] IBM, WebSphere Process Server, software/integration wps, Jan. 2009.
[28] IBM, WebSphere Integration Developer, wid, Jan. 2009.
[29] P. Inverardi, H. Muccini, and P. Pelliccione, “CHARMY: An Extensible Tool for Architectural Analysis,” Proc. 13th ACM SIGSOFT Int'l Symp. Foundations of Software Eng. (FSE '05), pp.111-114, Sept. 2005.
[30] A. Møller, dk.brics.automaton, http://www.brics.dkautomaton, Jan. 2009.
[31] Duke Univ., JFLAP, http:/, Jan. 2009.
[32] Y. Gan, “Runtime Monitoring of Web Service Conversations,” master's thesis, Dept. of Computer Science, Univ. of Toronto, Mar. 2007.
[33] M. Lettrari and J. Klose, “Scenario-Based Monitoring and Testing of Real-Time UML Models,” Proc. Fourth Int'l Conf. Unified Modeling Language, Modeling Languages, Concepts, and Tools (UML '01), pp. 317-328, 2001.
[34] M.A. Ameedeen and B. Bordbar, “A Model Driven Approach to Represent Sequence Diagrams as Free Choice Petri Nets,” Proc. 12th Int'l IEEE Enterprise Distributed Object Computing Conf. (EDOC '08), pp. 213-221, 2008.
[35] Ø. Haugen, K.E. Husa, R.K. Runde, and K. Stølen, “STAIRS: Towards Formal Design with Sequence Diagrams,” J. Software and System Modeling, vol. 4, pp. 355-357, 2005.
[36] S. Maoz and D. Harel, “From Multi-Modal Scenarios to Code: Compiling LSCs into AspectJ,” Proc. SIGSOFT Conf. Foundations of Software Eng. (FSE '06), pp. 219-230, 2006.
[37] F. Chen and G. Rosu, “MOP: An Efficient and Generic Runtime Verification Framework,” Proc. Int'l Conf. Object-Oriented Programming, Systems, Languages and Applications (OOPSLA '07), pp. 569-588, 2007.
[38] D. Harel and R. Marelly, Come Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, 2003.
[39] T. Bultan, “Modeling Interactions of Web Software,” Proc. Second Int'l Workshop Automated Specification and Verification of Web Systems (WWV '06), pp. 45-52, 2006.
[40] A. Lazovik, M. Aiello, and M.P. Papazoglou, “Associating Assertions with Business Processes and Monitoring Their Execution,” Proc. Second Int'l Conf. Service Oriented Computing (ICSOC '04), pp. 94-104, Nov. 2004.
[41] L. Baresi, C. Ghezzi, and S. Guinea, “Smart Monitors for Composed Services,” Proc. Second Int'l Conf. Service Oriented Computing (ICSOC '04), pp. 193-202, Nov. 2004.
[42] L. Baresi and S. Guinea, “Towards Dynamic Monitoring of WS-BPEL Processes,” Proc. Third Int'l Conf. Service Oriented Computing (ICSOC '05), pp. 269-282, 2005.
[43] M. Pistore and P. Traverso, “Assumption-Based Composition and Monitoring of Web Services,” Test and Analysis of Web Services, pp.307-335, Springer, 2007.
[44] M. Lohmann, L. Mariani, and R. Heckel, “A Model-Driven Approach to Discovery, Testing and Monitoring of Web Services,” Test and Analysis of Web Services, pp. 173-204, Springer, 2007.
[45] Z. Li, Y. Jin, and J. Han, “A Runtime Monitoring and Validation Framework for Web Service Interactions,” Proc. 17th Australian Software Eng. Conf. (ASWEC '06), pp. 70-79, 2006.
[46] K. Mahbub and G. Spanoudakis, “A Framework for Requirements Monitoring of Service Based Systems,” Proc. Second Int'l Conf. Service Oriented Computing (ICSOC '04), pp. 84-93, 2004.
[47] K. Mahbub and G. Spanoudakis, “Run-Time Monitoring of Requirements for Systems Composed of Web-Services: Initial Implementation and Evaluation Experience,” Proc. Int'l Conf. Web Services (ICWS '05), pp. 257-265, July 2005.
[48] W.M.P. van der Aalst and M. Pesic, “Specifying and Monitoring Service Flows: Making Web Services Process-Aware,” Test and Analysis of Web Services, pp. 11-55, Springer, 2007.
[49] Z. Li, J. Han, and Y. Jin, “Pattern-Based Specification and Validation of Web Services Interaction Properties,” Proc. Third Int'l Conf. Service Oriented Computing (ICSOC '05), pp. 73-86, 2005.
[50] M. Shanahan, “The Event Calculus Explained,” Artificial Intelligence Today, pp. 409-430, Springer, 1999.
[51] J.A. Baier and S.A. McIlraith, “Planning with First-Order Temporally Extended Goals Using Heuristic Search,” Proc. 21st Nat'l Conf. Artificial Intelligence (AAAI '06) and the 18th Innovative Applications of Artificial Intelligence Conf. (IAAI '06), July 2006.
[52] L. Baresi, S. Guinea, and L. Pasquale, “Self-Healing BPEL Processes with Dynamo and the JBoss Rule Engine,” Proc. Int'l Workshop Eng. of Software Services for Pervasive Environments (ESSPE '07), pp. 11-20, 2007.
[53] O. Moser, F. Rosenberg, and S. Dustdar, “Non-Intrusive Monitoring and Service Adaptation for WS-BPEL,” Proc. 17th Int'l Conf. World Wide Web (WWW '08), pp. 815-824, 2008.
[54] M. Reichert and P. Dadam, “ADEPTflex: Supporting Dynamic Changes of Workflows without Losing Control,” J. Intelligent Information Systems, vol. 10, no. 2, pp. 93-129, 1998.
[55] A. Zeller, “Isolating Cause-Effect Chains from Computer Programs,” SIGSOFT Software Eng. Notes, vol. 27, no. 6, pp. 1-10, 2002.
[56] A. Groce, S. Chaki, D. Kroening, and O. Strichman, “Error Explanation with Distance Metrics,” Int'l J. Software Tools for Technology Transfer, vol. 8, no. 3, pp. 229-247, 2006.
[57] P. Inverardi, L. Mostarda, M. Tivoli, and M. Autili, “Synthesis of Correct and Distributed Adaptors for Component-Based Systems: An Automatic Approach,” Proc. 20th Int'l Conf. Automated Software Eng. (ASE '05), pp. 405-409, 2005.
86 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool