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 £75.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)
      • Towards open-world software: issues and challenges
    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)
      • Business Process Execution Language for Web Services, Version 1.1
    5. 5)
      • 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)
      • Model checking
    7. 7)
    8. 8)
      • ANNA: a language for annotating Ada programs
    9. 9)
      • 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)
      • 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)
      • A model checking approach to verify BPEL4WS workflows, Proc. 2007 IEEE Int. Conf. Service-oriented Computing and Applications
    14. 14)
      • Symmetry and model checking
    15. 15)
      • Space-reduction strategies for model checking dynamic systems, Proc. 2003 Workshop on Software Model Checking
    16. 16)
      • Using partial orders to improve automatic verification methods, CAV 1990 Proc. 2nd Int. Workshop on Computer Aided Verification
    17. 17)
      • 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)
      • 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)
      • 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)
      • Formal verification of BPEL4WS business collaborations, Lecture Notes in Computer Science
    25. 25)
      • Model-checking behavioral specification of BPEL applications
    26. 26)
      • Modeling and model checking web services
    27. 27)
      • 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)
      • Verification of business processes for web services'. 4700 Keele Street, Toronto, M3J 1P3
    30. 30)
      • The concurrency workbench: a semantics-based tool for the verification of concurrent systems
    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