Abstract
Service-oriented systems, especially web services, have been given strong attention as an important approach to integrate heterogeneous systems, in which complex services are composed of simpler services offered by various service providers. The correctness of service composition requires techniques to verify whether composite services behave properly. To this end, in this paper, we propose a novel method for runtime monitoring of composite services. In our method, system specifications, which are automatically generated from descriptions of service composition, and requirement specifications, which include safety properties, are constructed to detect Business Process Execution Language (BPEL) engine-related and BPEL process-related violations. We employ process algebra as the primary formalism to express specifications. To verify the correctness of composite services, we check the refinement relation between specifications and observed behaviors. Also, we formally discuss what kinds of specifications can be monitored at runtime.
Similar content being viewed by others
References
Canfora G, Penta MD (2006) Testing services and service-centric systems: challenges and opportunities. IT Prof 8: 10–17
Tsai W-T, Zhou X, Chen Y, Bai X (2008) On testing and evaluating service-oriented software. Computer 41: 40–46
Papazoglou M, van den euvel W (2007) Service oriented architectures: approaches, technologies and research issues. VLDB J 16(3): 389–415
Rao J, Su X (2005) A survey of automated web service composition methods, pp 43–54
Barbon F, Traverso P, Pistore M, Trainotti M (2006) Run-time monitoring of instances and classes of web service compositions. In: Proceedings of IEEE international conference on web services, vol 0, pp 63–71
Lazovik A, Papazoglou M, Aiello M (2006) Planning and monitoring the execution of web service requests. Int J Digit Libr 6: 235–246
Lazovik A, Aiello M, Papazoglou M (2004) Associating assertions with business processes and monitoring their execution. In: ICSOC ’04: proceedings of the 2nd international conference on service oriented computing, New York, NY, USA, pp 94–104, ACM
Baresi L, Ghezzi C, Guinea S (2004) “Smart monitors for composed services. In: ICSOC ’04: proceedings of the 2nd international conference on service oriented computing. ACM, New York, NY, USA, pp 193–202
Baresi L, Guinea S (2005) Towards dynamic monitoring of ws-bpel processes. In: Service-oriented computing—ICSOC 2005, vol 3826, pp 269–282, Nov 2005
Raimondi F, Skene J, Emmerich W (2008) Efficient online monitoring of web-service slas. In: SIGSOFT ’08/FSE-16: proceedings of the 16th ACM SIGSOFT international symposium on foundations of software engineering. ACM, New York, NY, USA, pp 170–180
Mahbub K, Spanoudakis G (2005) Run-time monitoring of requirements for systems composed of web-services: initial implementation and evaluation experience. In: Proceedings of IEEE international conference on web services, vol 0, pp 257– 265
Li Z, Jin Y, Han J (2006) A runtime monitoring and validation framework for web service interactions. In: Proceedings of Australian software engineering conference, vol 0, pp 70–79
Robinson WN (2003) Monitoring web service requirements. In: Proceedings of IEEE international conference on requirements engineering, vol 0, p 65
Simmonds J, Yuan G, Chechik M, Nejati S, O’Farrell B, Litani E, Waterhouse J (2009) Runtime monitoring of web service conversations. IEEE Trans Services Comput 2: 223–244
Simmonds J, Chechik M, Nejati S, Litani E, O’Farrell B (2008) Property patterns for runtime monitoring of web service conversations. In: Runtime verification: 8th international workshop, RV 2008, Budapest, Hungary. Selected papers. Springer, Berlin, Heidelberg, pp 137–157, 30 March 2008
Alves A, Arkin A, Askary S, Barreto C, Bloch B, Curbera F, Ford M, Goland Y, Guızar A, Kartha N, et al (2007) Web services business process execution language version 2.0. OASIS Standard, vol 11
Roscoe A (1998) The theory and practice of concurrency. Prentice Hall PTR, Upper Saddle River
Roscoe A (2005) On the expressive power of CSP refinement. Formal Aspects Comput 17(2): 93–112
Ryan P, Schneider S (2000) The modelling and analysis of security protocols: the csp approach. Addison-Wesley Professional, Reading
Emerson EA (1990) Temporal and modal logic, pp 995–1072
Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng 3: 125–143
Pnueli A (1992) System specification and refinement in temporal logic. In: Proceedings of foundations of software technology and theoretical computer science: 12th conference. Springer, New Delhi, India, pp 1–38, 18–20 Dec 1992
Peterson JL (1981) Petri net theory and the modeling of systems. Prentice Hall PTR, Upper Saddle River
Clarke E, Grumberg O, Peled D (2000) Model checking. MIT Press, USA
Rajamani S (1999) New directions in refinement checking. Ph.D. thesis
Boudol G, Larsen KG (1992) Graphical versus logical specifications. Theor Comput Sci 106(1): 3–20
Delgado N, Gates AQ, Roach S (2004) A taxonomy and catalog of runtime software-fault monitoring tools. IEEE Trans Softw Eng 30: 859–872
Elmas T, Tasiran S, Qadeer S (2005) Vyrd: verifying concurrent programs by runtime refinement-violation detection. In: PLDI ’05: proceedings of the 2005 ACM SIGPLAN conference on programming language design and implementation. ACM, New York, NY, USA, pp 27–37
Elmas T, Tasiran S (2006) Vyrdmc: driving runtime refinement checking with model checkers. In: Electronic notes in theoretical computer science, vol 144, no 4, pp 41–56, 2006. Proceedings of the fifth workshop on runtime verification (RV 2005)
Tasiran S, Qadeer S (2005) Runtime refinement checking of concurrent data structures. In: Electronic notes in theoretical computer science, vol 113, pp 163–179, 2005. Proceedings of the fourth workshop on runtime verification (RV 2004)
Stolz V, Bodden E (2006) Temporal assertions using AspectJ. In: Electronic notes in theoretical computer science, vol 144, no 4, pp 109–124, 2006. Proceedings of the fifth workshop on runtime verification (RV 2005)
Wolper P (1981) Temporal logic can be more expressive. In: Proceedings of annual IEEE symposium on foundations of computer science, vol 0, pp 340–348
Ferrara A (2004) Web services: a process algebra approach. In: ICSOC ’04: proceedings of the 2nd international conference on service oriented computing. ACM, New York, NY, USA, pp 242–251
Khaxar M, Jalili S, Khakpour N, Jokhio MS (2009) Monitoring safety properties of composite web services at runtime using csp, pp 107–113, Sept 2009
Baader F, Siekmann JH (1994) Unification theory, pp 41–125
Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: Proceedings of international conference on software engineering, vol 0, p 411
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Khaxar, M., Jalili, S. WSCMon: runtime monitoring of web service orchestration based on refinement checking. SOCA 6, 33–49 (2012). https://doi.org/10.1007/s11761-011-0098-3
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11761-011-0098-3