A Type System for Client Progress in a Service-Oriented Calculus

  • Lucia Acciai
  • Michele Boreale
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5065)


We introduce a type system providing a guarantee of client progress for a fragment of CaSPiS, a recently proposed process calculus for serviceoriented applications. The interplay of sessioning and data-orchestration primitives makes the design of a type system for CaSPiS challenging. Our main result states that in a well-typed CaSPiS system, and in absence of divergence, any client invoking a service is guaranteed not to get stuck during the execution of a conversation protocol because of inadequate service communication capabilities.


process calculi service-oriented computing pi-calculus type systems 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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
  2. 2.
    Boreale, M., Bruni, R., De Nicola, R., Loreti, M.: Sessions and Pipelines for Structured Service Programming. FMOODS 2008 (to appear, 2008),
  3. 3.
    Bruni, R., Mezzina, L.G.: A deadlock free type system for a calculus of services and sessions (submitted, 2007)Google Scholar
  4. 4.
    Carpineti, S., Laneve, C.: A Basic Contract Language for Web Services. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 197–213. Springer, Vienna (2006)CrossRefGoogle Scholar
  5. 5.
    Carpineti, S., Castagna, G., Laneve, C., Padovani, L.: A formal account of contracts for web services. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 148–162. Springer, Vienna (2006)CrossRefGoogle Scholar
  6. 6.
    Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. In: POPL 2008, pp. 261–272. ACM Press, San Francisco (2008)CrossRefGoogle Scholar
  7. 7.
    Christensen, S., Hirshfeld, Y., Moller, F.: Bisimulation equivalence is decidable for basic parallel processes. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 143–157. Springer, Heidelberg (1993)Google Scholar
  8. 8.
    Cook, W.R., Misra, J.: Computation Orchestration: A Basis for Wide-Area Computing. Journal of Software and Systems Modeling (2006),
  9. 9.
    Deng, Y., Sangiorgi, D.: Ensuring Termination by Typability. Information and Computation 204(7), 1045–1082 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Gay, S., Hole, M.: Subtyping for session types in the pi-calculus. Acta Informatica 42(2), 191–225 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type disciplines for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 22–138. Springer, Lisbon (1998)CrossRefGoogle Scholar
  12. 12.
    Kobayashi, N.: A New Type System for deadlock-Free Processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 233–247. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Kobayashi, N.: A type system for lock-free processes. Information and Computation 177(2), 122–159 (2002)zbMATHMathSciNetGoogle Scholar
  14. 14.
    Lanese, I., Martins, F., Vasconcelos, V.T., Ravara, A.: Disciplining Orchestration and Conversation in Service-Oriented Computing. In: Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), pp. 305–314. IEEE Press, London (2007)CrossRefGoogle Scholar
  15. 15.
    Milner, R.: The polyadic π-calculus: a tutorial. Logic and Algebra of Specification, pp. 203–246. Springer, Heidelberg (1993)Google Scholar
  16. 16.
    Milner, R., Parrow, J., Walker, D.: A calculus of Mobile Processes, part I and II. Information and Computation 100, 1–40 and 41–78 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    SENSORIA: Software Engineering for Service-Oriented Overlay Computers. fet-gc ii ist-2005-16004 EU Project,
  18. 18.
    Talpin, J.P., Jouvelot, P.: The Type and Effect Discipline. Information and Computation 111(2), 245–296 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Vieira, H.T., Caires, L., Seco, J.C.: The Conversation Calculus: a Model of Service Oriented Computation. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 269–283. Springer, Heidelberg (2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Lucia Acciai
    • 1
  • Michele Boreale
    • 1
  1. 1.Dipartimento di Sistemi e InformaticaUniversità di Firenze 

Personalised recommendations