Validation of web service compositions

Validation of web service compositions

For access to this article, please select a purchase option:

Buy article PDF
(plus tax if applicable)
Buy Knowledge Pack
10 articles for $120.00
(plus taxes if applicable)

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Your details
Why are you recommending this title?
Select reason:
IET Software — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

Web services support software architectures that can evolve dynamically. In particular, in this paper the focus is on architectures where services are composed (orchestrated) through a workflow described in the business process execution language (BPEL). It is assumed that the resulting composite service refers to external services through assertions that specify their expected functional and non-functional properties. On the basis of these assertions, the composite service may be verified at design time by checking that it ensures certain relevant properties. Because of the dynamic nature of web services and the multiple stakeholders involved in their provision, however, the external services may evolve dynamically, and even unexpectedly. They may become inconsistent with respect to the assertions against which the workflow was verified during development. As a consequence, validation of the composition must extend to run time. In this work, an assertion language, called assertion language for BPEL process interactions (ALBERT), is introduced; it can be used to specify both functional and non-functional properties. An environment which supports design-time verification of ALBERT assertions for BPEL workflows via model checking is also described. At run time, the assertions can be turned into checks that a software monitor performs on the composite system to verify that it continues to guarantee its required properties. A TeleAssistance application is provided as a running example to illustrate our validation framework.


    1. 1)
      • L. Baresi , E. Di Nitto , C. Ghezzi . Towards open-world software: issues and challenges. IEEE Comp. , 36 - 43
    2. 2)
      • Jini Network Technology [homepage on the Internet]. Sun Corporation; 2007. Available from:
    3. 3)
      • OSGi [homepage on the Internet]. OSGi Alliance; 2007. Available from:
    4. 4)
      • T. Andrews , F. Curbera , H. Dholakia , Y. Goland , J. Klein , F. Leymann , K. Liu , D. Roller , D. Smith , S. Thatte , I. Trickoric , S. Weerawarana . (2003) Business Process Execution Language for Web Services, Version 1.1.
    5. 5)
      • M. Colombo , E. Di Nitto , M. Mauri . (2006) SCENE: a service composition execution environment supporting dynamic changes disciplined through rule, Service-Oriented Computing - ICSOC 2006, 4th Int. Conf., Proc. Lecture Notes in Computer Science.
    6. 6)
      • E.M. Clarke , O. Grumberg . (1999) Model checking.
    7. 7)
    8. 8)
      • D.C. Luckham , F.W. von Henke , B. Krieg-Brueckner , O. Owe . (1987) ANNA: a language for annotating Ada programs.
    9. 9)
      • G.T. Leavens , A.L. Baker , C. Ruby , H. Kilov , B. Rumpe , I. Simmonds . (1999) JML: a notation for detailed design, Behavioral specifications of businesses and systems.
    10. 10)
      • Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: `Lazy abstraction', POPL 2002: Proc. 29th ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages, 2002, p. 58–70.
    11. 11)
      • Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: `Counterexample-guided abstraction refinement’. CAV 2000', Proc. 12th Int. Conf. on Computer Aided Verification, 2000, Springer, p. 154–169, 1855 of Lectures notes in Computer Science.
    12. 12)
      • M.B. Robby, Dwyer , J. Hatcliff . (2003) Bogor: an extensible and highly-modular software model checking framework, ESEC/FSE-11: Proc. 9th European Software Engineering Conference held jointly with 11th ACM SIGSOFT Int. Symp. Foundations of Software Engineering.
    13. 13)
      • D. Bianculli , C. Ghezzi , P. Spoletini . (2007) A model checking approach to verify BPEL4WS workflows, Proc. 2007 IEEE Int. Conf. Service-oriented Computing and Applications.
    14. 14)
      • E.A. Emerson , A.P. Sistla . Symmetry and model checking. Form. Methods Syst. Des. , 105 - 131
    15. 15)
      • M.B. Robby, Dwyer , J. Hatcliff , R. Iosif . Space-reduction strategies for model checking dynamic systems, Proc. 2003 Workshop on Software Model Checking.
    16. 16)
      • P. Godefroid . (1991) Using partial orders to improve automatic verification methods, CAV 1990 Proc. 2nd Int. Workshop on Computer Aided Verification.
    17. 17)
      • L. Baresi , C. Ghezzi , L. Mottola . (2006) Towards fine-grained automated verification of publish-subscribe architectures, (FORTE06) Proc. 26th Int. Conf. on Formal Methods for Networked and Distributed Systems.
    18. 18)
      • ActiveBPEL Engine Architecture [homepage on the Internet]. Active Endpoints; 2006. Available from:
    19. 19)
      • G. Kiczales , J. Lamping , A. Mendhekar , C. Maeda , C.V. Lopes , J.M. Loingtier , J. Irwin . (1997) Aspect-oriented Programming, ECOOP'97 – Object-Oriented Programming.
    20. 20)
      • Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: `An overview of AspectJ', ECOOP 2001 - Object-Oriented Programming. 15th European Conf., Proc., 2001, 2072, p. 327–353, Lecture Notes in Computer Science. Springer.
    21. 21)
      • O. Kupferman , M. Vardi . (1997) Weak alternating automata are not that weak, Fifth Israle Symp. Theory of Computing and Systems, ISTCS'97, Proc..
    22. 22)
      • Fu, X., Bultan, T., Su, J.: `Analysis of interacting BPEL web services', WWW 2004: Proc. 13th Int. Conf. World Wide Web, 2004, New York, NY, ACM Press, p. 621–630.
    23. 23)
    24. 24)
      • J. Arias-Fisteus , L.S. Fernández , C.D. Kloos . (2004) Formal verification of BPEL4WS business collaborations, Lecture Notes in Computer Science.
    25. 25)
      • S. Nakajima . Model-checking behavioral specification of BPEL applications. Electron. Notes Theor. Comput. Sci. , 2 , 89 - 105
    26. 26)
      • B.H. Schlingloff , A. Martens , K. Schmidt . Modeling and model checking web services. Electron. Notes Theor. Comput. Sci. , 3 - 26
    27. 27)
      • K. Schmidt . (2000) LoLA: a low level analyser, Lecture Notes in Computer Science.
    28. 28)
      • Foster, H., Uchitel, S., Magee, J., Kramer, J.: `Model-based verification of web service compositions', Proc. 18th IEEE Int. Conf. Automated Software Engineering (ASE 2003). IEEE Computer Society, 2003, p. 152–163.
    29. 29)
      • M. Koshkina , F. van Breugel . (2003) Verification of business processes for web services'. 4700 Keele Street, Toronto, M3J 1P3.
    30. 30)
      • R. Cleaveland , J. Parrow , B. Steffen . The concurrency workbench: a semantics-based tool for the verification of concurrent systems. ACM Trans.Program. Lang. Syst. , 1 , 36 - 72
    31. 31)
      • Sahai, A., Machiraju, V., Sayal, M., Jin, L.J., Casati, F.: `Automated SLA Monitoring for Web Services', Proc. 13th IFIP/IEEE Int. Workshop on Distributed Systems: Operations and Management - Management Technologies for E-Commerce and E-Business Applications, 2002, 2506, Springer, p. 28–41, Lecture Notes in Computer Science.
    32. 32)
      • Keller, A., Ludwig, H.: `Defining and monitoring service-level agreements for dynamic e-business', Proc. 16th Conf. Systems Administration, 2002, Berkeley, CA, USENIX Association, p. 189–204.
    33. 33)
      • Skene, J., Lamanna, D.D., Emmerich, W.: `Precise service level agreements', ICSE 2004: Proc. 26th Int. Conf. Software Engineering, 2004, Washington, DC, IEEE Computer Society, p. 179–188.
    34. 34)
      • Skene, J., Skene, A., Crampton, J., Emmerich, W.: `The monitorability of service-level agreements for application-service provision', WOSP 2007: Proc. 6th Int. Workshop on Software and performance, 2007, New York, NY, ACM Press, p. 3–14.
    35. 35)
      • Robinson, W.N.: `Monitoring web service requirements', RE 2003: Proc. 11th IEEE Int. Conf. Requirements Engineering, 2003, Washington, DC, IEEE Computer Society, p. 65.
    36. 36)
      • Mahbub, K., Spanoudakis, G.: `A framework for requirements monitoring of service based systems', ICSOC 2004: Proc. 2nd int. conf. Service Oriented Computing, 2004, New York, NY, ACM Press, p. 84–93.
    37. 37)
      • Barbon, F., Traverso, P., Pistore, M., Trainotti, M.: `Run-time monitoring of instances and classes of web service compositions', ICWS 2006: Proc. 2006 IEEE Int. Conf. Web Services, 2006, Washington, DC, IEEE Computer Society, p. 63–71.
    38. 38)
    39. 39)
      • Graf, S., Saidi, H.: `Construction of abstract state graphs with PVS', CAV 1997: Proc. 9th Int. Conf. Computer Aided Verification, 1997, Springer, p. 72–83, Vol. 1254 of Lectures Notes in Computer Science.

Related content

This is a required field
Please enter a valid email address