Compositional Specification of Web Services Via Behavioural Equivalence of Nets: A Case Study

  • Filippo Bonchi
  • Antonio Brogi
  • Sara Corfini
  • Fabio Gadducci
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5062)


Web services represent a promising technology for the development of distributed heterogeneous software systems. In this setting, a major issue is to establish whether two services can be used interchangeably in any context. This paper illustrates — through a concrete scenario from banking systems — how a suitable notion of behavioural equivalence over Petri nets can be effectively employed for checking the correctness of service specifications and the replaceability of (sub)services.


Composite Service Label Transition System Banking Service Data Place Control Place 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Papazoglou, M., Georgakopoulos, D.: Service-Oriented Computing. Communications of the ACM 46(10), 24–28 (2003)CrossRefGoogle Scholar
  2. 2.
    OWL-S Coalition: OWL-S: Semantic Markup for Web Service (2006),
  3. 3.
    Bonchi, F., Brogi, A., Corfini, S., Gadducci, F.: A Behavioural Congruence for Web services. In: Arbab, F., Sarjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 240–256. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  4. 4.
  5. 5.
    Reisig, W.: Petri Nets: An Introduction. EACTS Monographs on Theoretical Computer Science. Springer, Heidelberg (1985)zbMATHGoogle Scholar
  6. 6.
    Brogi, A., Corfini, S.: Behaviour-aware discovery of Web service compositions. International Journal of Web Services Research 4(3), 1–25 (2007)Google Scholar
  7. 7.
    Bonchi, F., König, B., Montanari, U.: Saturated semantics for reactive systems. In: Logic in Computer Science, pp. 69–80. IEEE Computer Society, Los Alamitos (2006)Google Scholar
  8. 8.
    Leifer, J., Milner, R.: Deriving bisimulation congruences for reactive systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 243–258. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  9. 9.
    Brogi, A., Corfini, S., Iardella, S.: From OWL-S descriptions to Petri nets. In: Nitto, E.D., Ripeanu, M. (eds.) ICSOC 2007 Workshops. LNCS, Springer, Heidelberg (to appear, 2008),
  10. 10.
    Verbeek, H., van der Aalst, W.: Analyzing BPEL processes using Petri nets. In: Marinescu, D. (ed.) Applications of Petri Nets to Coordination, Workflow and Business Process Management, pp. 59–78. Florida International University, Miami (2005)Google Scholar
  11. 11.
    van der Aalst, W.: Pi calculus versus Petri nets: Let us eat “humble pie” rather than further inflate the “Pi hype”. BPTrends 3(5), 1–11 (2005)Google Scholar
  12. 12.
    Martens, A.: On compatibility of Web services. Petri Net Newsletter 65, 12–20 (2003)Google Scholar
  13. 13.
    Martens, A.: Analyzing Web service based business processes. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 19–33. Springer, Heidelberg (2005)Google Scholar
  14. 14.
    Pathak, J., Basu, S., Honavar, V.: On context-specific substitutability of Web Services. In: Web Services, pp. 192–199. IEEE Computer Society, Los Alamitos (2007)Google Scholar
  15. 15.
    Puhlmann, F., Weske, M.: Interaction soundness for Service Orchestrations. In: Dan, A., Lamersdorf, W. (eds.) ICSOC 2006. LNCS, vol. 4294, pp. 302–313. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  16. 16.
    Massuthe, P., Reisig, W., Schmidt, K.: An operating guideline approach to the SOA. Annals of Mathematics, Computing & Teleinformatics 1(3), 35–43 (2005)Google Scholar
  17. 17.
    Lohmann, N., Massuthe, P., Wolf, K.: Operating Guidelines for finite-state services. In: Kleijn, Y., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 321–341. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  18. 18.
    Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing interacting BPEL processes. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol. 4102, pp. 17–32. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  19. 19.
    Castagna, G., Gesbert, N., Padovani, L.: A Theory of Contracts for Web Services. In: Ghelli, G. (ed.) Programming Language Technologies for XML, pp. 37–48 (2007)Google Scholar
  20. 20.
    Laneve, C., Padovani, L.: The must preorder revisited. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 212–225. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  21. 21.
    Bordeaux, L., Salaün, G., Berardi, D., Mecella, M.: When are Two Web Services Compatible? In: Shan, M.-C., Dayal, U., Hsu, M. (eds.) TES 2004. LNCS, vol. 3324, pp. 15–28. Springer, Heidelberg (2005)Google Scholar
  22. 22.
    Benatallah, B., Casati, F., Ponge, J., Toumani, F.: Compatibility and replaceability analysis for timed web service protocols. In: Benzaken, V. (ed.) Bases de Données Avancées (2005)Google Scholar
  23. 23.
    Fernandez, J.C., Mounier, L., Jard, C., Jeron, T.: On-the-fly verification of finite transition systems. Formal Methods in System Design 1(2/3), 251–273 (1992)CrossRefGoogle Scholar
  24. 24.
    Bonchi, F., Montanari, U.: Coalgebraic models for reactive systems. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 364–379. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  25. 25.
    BPEL Coalition: WS-BPEL 2.0 (2006),
  26. 26.
    Ouyang, C., Verbeek, E., van der Aalst, W., Breutel, S., Dumas, M., ter Hofstede, A.: Formal semantics and analysis of control flow in WS-BPEL. Technical Report BPM-05-15, BPM Center (2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Filippo Bonchi
    • 1
  • Antonio Brogi
    • 1
  • Sara Corfini
    • 1
  • Fabio Gadducci
    • 1
  1. 1.Department of Computer ScienceUniversity of PisaItaly

Personalised recommendations