Provably Correct Implementations of Services

  • Roberto Bruni
  • Rocco De Nicola
  • Michele Loreti
  • Leonardo Gaetano Mezzina
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5474)


A number of formalisms have been defined to support the specification and analysis of service oriented applications. These formalisms have been equipped with tools (types or logics) to guarantee the correct behavior of the specified services. Due to the semantic gap between the specification formalism and the programming languages of service oriented overlay computers a critical issue is guaranteeing that correctness is preserved when running the specified systems over available implementations. We have defined a service oriented abstract machine, equipped with a formal structural semantics, that can be used to implement service specification formalisms. We use our abstract machine to implement different service oriented formalisms that have been recently proposed, each posing specific challenges that we can address successfully. By exploiting the SOS semantics of the abstract machine and those of the considered service oriented formalisms we do prove that our implementations are correct (sound and complete). We also discuss possible implementations of other formalisms.


Operational Semantic Correctness Proof Abstract Machine Service Invocation Session Subject 
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.
    Bettini, L., De Nicola, R., Falassi, D., Lacoste, M., Lopes, L.M.B., Oliveira, L., Paulino, H., Vasconcelos, V.T.: A software framework for rapid prototyping of run-time systems for mobile calculi. In: Priami, C., Quaglia, P. (eds.) GC 2004. LNCS, vol. 3267, pp. 179–207. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  2. 2.
    Bettini, L., De Nicola, R., Loreti, M.: Implementing session centered calculi. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 17–32. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  3. 3.
    Bonelli, E., Compagnoni, A., Gunter, E.: Correspondence assertions for process synchronization in concurrent communications. J. Funct. Program. 15(2), 219–247 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Boreale, M., Bruni, R., Caires, L., De Nicola, R., Lanese, I., Loreti, M., Martins, F., Montanari, U., Ravara, A., Sangiorgi, D., Vasconcelos, V.T., Zavattaro, G.: SCC: a service centered calculus. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 38–57. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Boreale, M., Bruni, R., De Nicola, R., Loreti, M.: Sessions and pipelines for structured service programming. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 19–38. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  6. 6.
    Bruni, R., Lanese, I., Melgratti, H., Mezzina, L.G., Tuosto, E.: Towards trustworthy multiparty sessions (extended abstract). In: Vasconcelos, V.T., Yoshida, N. (eds.) Pre-proceedings of PLACES 2008, 1st Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software, pp. 22–27. Technical Report DI-FCUL TR-08-14, Departamento de Informatica, Faculdade de Ciencias da Universidade de Lisboa (2008)Google Scholar
  7. 7.
    Bruni, R., Lanese, I., Melgratti, H., Tuosto, E.: Multiparty sessions in SOC. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 67–82. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  8. 8.
    Bruni, R., Mezzina, L.G.: Types and deadlock freedom in a calculus of services, sessions and pipelines. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 100–115. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Busi, N., Gorrieri, R., Guidi, C., Lucchi, R., Zavattaro, G.: Sock: a calculus for service oriented computing. In: Dan, A., Lamersdorf, W. (eds.) ICSOC 2006. LNCS, vol. 4294, pp. 327–338. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. 10.
    Caires, L., Viera, H.T., Seco, J.C.: The conversation calculus: a model of service oriented computation. Technical Report TR DIFCTUNL 6/07, Univ. Lisbon (2007)Google Scholar
  11. 11.
    Dezani-Ciancaglini, M., de’Liguoro, U., Yoshida, N.: On progress for structured communications. In: Barthe, G., Fournet, C. (eds.) TGC 2007 and FODO 2008. LNCS, vol. 4912, pp. 257–275. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  12. 12.
    Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  13. 13.
    Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of POPL 2008, 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 273–284. ACM, New York (2008)Google Scholar
  14. 14.
    Kobayashi, N.: Typical: Type-based static analyzer for the pi-calculus. Tool,
  15. 15.
    Lanese, I., Martins, F., Ravara, A., Vasconcelos, V.T.: Disciplining orchestration and conversation in service-oriented computing. In: SEFM 2007, pp. 305–314. IEEE Computer Society Press, Los Alamitos (2007)Google Scholar
  16. 16.
    Lapadula, A., Pugliese, R., Tiezzi, F.: A calculus for orchestration of web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 33–47. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    Mezzina, L.G.: How to infer finite session types in a calculus of services and sessions. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 216–231. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  18. 18.
    Misra, J., Cook, W.R.: Computation orchestration: A basis for wide-area computing. Journal of Software and Systems Modeling 6(1), 83–110 (2007)CrossRefGoogle Scholar
  19. 19.
    Peschanski, F., Hym, S.: A stackless runtime environment for a pi-calculus. In: VEE 2006: Proceedings of the 2nd international conference on Virtual execution environments, pp. 57–67. ACM, New York (2006)Google Scholar
  20. 20.
    Pierce, B.C.: Programming in the pi-calculus: A tutorial introduction to pict. available electronically. Technical report (1997)Google Scholar
  21. 21.
    Rossberg, A., Le Botlan, D., Tack, G., Brunklaus, T., Smolka, G.: Alice Through the Looking Glass, Munich, Germany. Trends in Functional Programming, vol. 5, pp. 79–96. Intellect Books, Bristol (2006)Google Scholar
  22. 22.
    Turner, D.N.: Ph. D. The polymorphic pi-calculus: Theory and implementation. Technical report (1995)Google Scholar
  23. 23.
    Vieira, H., Caires, L.: The spatial logic model checker user’s manual. Technical report (2004)Google Scholar
  24. 24.
    Yoshida, N., Vasconcelos, V.T.: Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. Elect. Notes in Th. Comput. Sci. 171(4), 73–93 (2007)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Roberto Bruni
    • 1
  • Rocco De Nicola
    • 2
  • Michele Loreti
    • 2
  • Leonardo Gaetano Mezzina
    • 3
  1. 1.Dipartimento di InformaticaUniversità di PisaItaly
  2. 2.Dipartimento di Sistemi e InformaticaUniversità di FirenzeItaly
  3. 3.IMT Alti Studi LuccaItaly

Personalised recommendations