Hostname: page-component-8448b6f56d-jr42d Total loading time: 0 Render date: 2024-04-20T09:34:11.345Z Has data issue: false hasContentIssue false
  • English
  • Français

CaSPiS: a calculus of sessions, pipelines and services†

Published online by Cambridge University Press:  10 November 2014

MICHELE BOREALE ,
ROBERTO BRUNI ,
ROCCO DE NICOLA  and
MICHELE LORETI
MICHELE BOREALE
Affiliation:
Dipartimento di Statistica, Informatica, Applicazioni “G. Parenti”, Università di Firenze, Viale Morgagni 65, I-50134 Firenze, Italy Email: michele.boreale@unifi.it, michele.loreti@unifi.it
ROBERTO BRUNI
Affiliation:
Dipartimento di Informatica, Università di Pisa, Largo Bruno Pontecorvo 3, I-56127 Pisa, Italy Email: bruni@di.unipi.it
ROCCO DE NICOLA
Affiliation:
IMT- Institute for Advanced Studies Lucca, Piazza S. Ponziano, 6 I-55100 Lucca, Italy Email: rocco.denicola@imtlucca.it
MICHELE LORETI
Affiliation:
Dipartimento di Statistica, Informatica, Applicazioni “G. Parenti”, Università di Firenze, Viale Morgagni 65, I-50134 Firenze, Italy Email: michele.boreale@unifi.it, michele.loreti@unifi.it
Get access Rights & Permissions [Opens in a new window]

Abstract

Service-oriented computing is calling for novel computational models and languages with well-disciplined primitives for client–server interaction, structured orchestration and unexpected events handling. We present CaSPiS, a process calculus where the conceptual abstractions of sessioning and pipelining play a central role for modelling service-oriented systems. CaSPiS sessions are two-sided, uniquely named and can be nested. CaSPiS pipelines permit orchestrating the flow of data produced by different sessions. The calculus is also equipped with operators for handling (unexpected) termination of the partner's side of a session. Several examples are presented to provide evidence of the flexibility of the chosen set of primitives. One key contribution is a fully abstract encoding of Misra et al.'s orchestration language Orc. Another main result shows that in CaSPiS it is possible to program a ‘graceful termination’ of nested sessions, which guarantees that no session is forced to hang forever after the loss of its partner.

Type
Special Issue: Objects and Services
Information
Mathematical Structures in Computer Science , Volume 25 , Issue 3 , March 2015 , pp. 666 - 709
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

†

Research supported by the Project FET-GC II IST-2005-16004 Sensoria.

References

Acciai, L. and Boreale, M. (2008a) Responsiveness in process calculi. Theoretical Computer Science 409 (1)59–93.CrossRefGoogle Scholar
Acciai, L. and Boreale, M. (2008b) A type system for client progress in a service-oriented calculus. In: Festschrift in Honour of Ugo Montanari, on the Occasion of His 65th Birthday. Springer Lecture Notes in Computer Science 5065 642–658.Google Scholar
Acciai, L. and Boreale, M. (2008c) Xpi: A typed process calculus for xml messaging. Science of Computer Programming 71 (2)110–143.Google Scholar
Bartoletti, M., Degano, P., Ferrari, G. and Zunino, R. (2007). Types and effects for resource usage analysis. In: Seidl, H. (ed.) Proceedings of FOSSACS'07. Springer Lecture Notes in Computer Science 4423 32–47.Google Scholar
Bettini, L., De Nicola, R. and Loreti, M. (2008) Implementing session centered calculi. In: Lea, D. and Zavattaro, G. (eds.) Proceedings of COORDINATION'08. Springer Lecture Notes in Computer Science 5052 17–32.Google Scholar
Bodei, C., Brodo, L. and Bruni, R. (2009) Static detection of logic flaws in service applications. In: Degano, P. and Viganò, L. (eds.) Proceedings of ARSPA-WITS'09. Springer Lecture Notes in Computer Science 5511 70–87.Google Scholar
Bonelli, E. and Compagnoni, A. (2008) Multisession session types for a distributed calculus. In: Barthe, G. and Fournet, C. (eds.) Proceedings of TGC'07. Springer Lecture Notes in Computer Science 4912 240–256.Google Scholar
Boreale, M., Bruni, R., Caires, L., De Nicola, R., Lanese, I., Loreti, M., Martins, F., Montanari, U., Ravara, A., Sangiorgi, D., Vasconcelos, V. and Zavattaro, G. (2006) SCC: a service centered calculus. In: Bravetti, M., Núñez, M. and Zavattaro, G. (eds.) Proceedings of WS-FM'06. Springer Lecture Notes in Computer Science 4184 38–57.Google Scholar
Boreale, M., Bruni, R., De Nicola, R. and Loreti, M. (2008) Sessions and pipelines for structured service programming. In: Barthe, G. and de Boer, F.S. (eds.) Proceedings of FMOODS'08. Springer Lecture Notes in Computer Science 5051 19–38.Google Scholar
Boreale, M. and Sangiorgi, D. (1998) A fully abstract semantics for causality in the pi-calculus. Acta Informatica 35 (5)353–400.Google Scholar
Bravetti, M. and Zavattaro, G. (2007) A theory for strong service compliance. In: Murphy, A.L. and Vitek, J. (eds.) Proceedings of COORDINATION'07. Springer Lecture Notes in Computer Science 4467 96–112.CrossRefGoogle Scholar
Bravetti, M. and Zavattaro, G. (2008) A foundational theory of contracts for multi-party service composition. Fundamenta Informaticae 89 (4)451–478.Google Scholar
Bruni, R. (2009) Calculi for service-oriented computing. In: Bernardo, M., Padovani, L. and Zavattaro, G. (eds.) Proceedings of SFM-WS'09. Springer Lecture Notes in Computer Science 5569 1–41.Google Scholar
Bruni, R., Butler, M., Ferreira, C., Hoare, T., Melgratti, H. and Montanari, U. (2005) Comparing two approaches to compensable flow composition. In: Abadi, M. and de Alfaro, L. (eds.) Proceedings of CONCUR'05. Springer Lecture Notes in Computer Science 3653 383–397.Google Scholar
Bruni, R., De Nicola, R., Loreti, M. and Mezzina, L. (2009) Provably correct implementations of services. In: Kaklamanis, C. and Nielson, F. (eds.) Proceedings of TGC'08. Springer Lecture Notes in Computer Science 5474 69–86.CrossRefGoogle Scholar
Bruni, R., Gadducci, F. and Lluch-Lafuente, A. (2010a) An algebra of hierarchical graphs and its application to structural encoding. Scientific Annals of Computer Science 20 53–96.Google Scholar
Bruni, R., Lanese, I., Melgratti, H. and Tuosto, E. (2008) Multiparty sessions in SOC. In: Lea, D. and Zavattaro, G. (eds.) Proceedings of COORDINATION'08. Springer Lecture Notes in Computer Science 5052 67–82.Google Scholar
Bruni, R., Liu, Z. and Zhao, L. (2010b) Graph representation of sessions and pipelines for structured service programming. In: Proceedings of FACS'10. Springer Lecture Notes in Computer Science 6921 259–276.Google Scholar
Bruni, R., Melgratti, H. and Montanari, U. (2004) Nested commits for mobile calculi: extending join. In Lévy, J.-J., Mayr, E. and Mitchell, J. (eds.) Proceedings of IFIP-TCS'04, Kluwer Academic Publishers 569–582.Google Scholar
Bruni, R. and Mezzina, L. (2008) Types and deadlock freedom in a calculus of services, sessions and pipelines. In: Rosu, G. and Meseguer, J. (eds.) Proceedings of AMAST'08. Springer Lecture Notes in Computer Science 5140 100–115.Google Scholar
Buscemi, M. and Montanari, U. (2007) CC-Pi: A constraint-based language for specifying service level agreements. In: De Nicola, R. (ed.) Proceedings of ESOP'07. Springer Lecture Notes in Computer Science 4421 18–32.Google Scholar
Busi, N., Gorrieri, R., Guidi, C., Lucchi, R. and Zavattaro, G. (2006) Choreography and orchestration conformance for system design. In: Ciancarini, P. and Wiklicky, H. (eds.) Proceedings of COORDINATION'06. Springer Lecture Notes in Computer Science 4038 63–81.Google Scholar
Caires, L., Vieira, H.T. and Seco, J.C. (2008) The conversation calculus: A model of service oriented computation. In: Drossopoulou, S. (ed.), Proceedings of ESOP'08. Springer Lecture Notes in Computer Science 4960 269–283.Google Scholar
Capecchi, S., Giachino, E. and Yoshida, N. (2010) Global escape in multiparty sessions. In: Lodaya, K. and Mahajan, M. (eds.) Proceedings of FSTTCS'10. Leibniz International Proceedings in Informatics 8 338–351. (Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.)Google Scholar
Carbone, M., Honda, K. and Yoshida, N. (2007) Structured communication-centred programming for web services. In: De Nicola, R. (ed.) Proceedings of ESOP'07. Springer Lecture Notes in Computer Science 4421 2–17.Google Scholar
Carbone, M., Honda, K. and Yoshida, N. (2008) Structured interactional exceptions in session types. In: van Breugel, F. and Chechik, M. (eds.) Proceedings of CONCUR'08. Springer Lecture Notes in Computer Science 5201 402–417.Google Scholar
Carbone, M., Yoshida, N. and Honda, K. (2009) Asynchronous session types: exceptions and multiparty interactions. In: Bernardo, M., Padovani, L. and Zavattaro, G. (eds.)Proceedings of SFM-WS'09. Springer Lecture Notes in Computer Science 5569 187–212.Google Scholar
Carpineti, S., Castagna, G., Laneve, C. and Padovani, L. (2006) A formal account of contracts for web services. In: Bravetti, M., Núñez, M. and Zavattaro, G. (eds.) Proceedings of WS-FM'06. Springer Lecture Notes in Computer Science 4184 148–162.Google Scholar
Castagna, G., Gesbert, N. and Padovani, L. (2008) A theory of contracts for web services. In: Necula, G.C. and Wadler, P. (eds.) Proceedings of POPL'08, ACM 261–272.Google Scholar
Cook, W. R., Patwardhan, S. and Misra, J. (2006) Workflow patterns in Orc. In: Ciancarini, P. and Wiklicky, H. (eds.) Proceedings of COORDINATION'06. Springer Lecture Notes in Computer Science 4038 82–96.Google Scholar
De Nicola, R., Latella, D., Loreti, M. and Massink, M. (2009) MarCaSPiS: a Markovian extension of a calculus for services. Electronic Notes in Theoretical Computer Science 229 (4)11–26.CrossRefGoogle Scholar
Dezani-Ciancaglini, M., Yoshida, N., Ahern, A. and Drossopoulou, S. (2007) A distributed object-oriented language with session types. In: De Nicola, R. and Sangiorgi, D. (eds.) Proceedings of TGC'05. Springer Lecture Notes in Computer Science 3705 299–318.Google Scholar
Ferrari, G., Guanciale, R. and Strollo, D. (2006) JSCL: a middleware for service coordination. In: Najm, E., Pradat-Peyre, J.-F. and Donzeau-Gouge, V. (eds.) Proceedings of FORTE'06. Springer Lecture Notes in Computer Science 4229 46–60.Google Scholar
Ferrari, G., Guanciale, R., Strollo, D. and Tuosto, E. (2007) Coordination via types in an event-based framework. In: Derrick, J. and Vain, J. (eds.), Proceedings of FORTE'07. Lecture Notes in Computer Science 4574 66–80.CrossRefGoogle Scholar
Gay, S.J. and Hole, M.J. (1999) Types and subtypes for client-server interactions. In: Swierstra, S.D. (ed.), Proceedings of ESOP'99. Springer Lecture Notes in Computer Science 1576 74–90.Google Scholar
Honda, K. (1993) Types for dyadic interaction. In: Best, E. (ed.) Proceedings of CONCUR'93. Springer Lecture Notes in Computer Science 4421 509–523.Google Scholar
Honda, K., Vasconcelos, V.T. and Kubo, M. (1998) Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.), Proceedings of ESOP'98. Springer Lecture Notes in Computer Science 1381 122–138.Google Scholar
Honda, K., Yoshida, N. and Carbone, M. (2008) Multiparty asynchronous session types. In: Necula, G.C. and Wadler, P. (eds.) Proceedings of POPL'08, ACM, 273–284.CrossRefGoogle Scholar
Kitchin, D., Cook, W.R. and Misra, J. (2006) A language for task orchestration and its semantic properties. In: Baier, C. and Hermanns, H. (eds.) Proceedings of CONCUR'06. Springer Lecture Notes in Computer Science 4137 477–491.Google Scholar
Kolundzija, M. (2009) Security types for sessions and pipelines. In: Bruni, R. and Wolf, K. (eds.) Proceedings of WS-FM'08. Springer Lecture Notes in Computer Science 5387 176–190.Google Scholar
Lanese, I., Vasconcelos, V., Martins, F. and Ravara, A. (2007) Disciplining orchestration and conversation in service-oriented computing. In: Proceedings of SEFM'07, IEEE Computer Society Press 305–314.Google Scholar
Laneve, C. and Padovani, L. (2008). The pairing of contracts and session types. In: Concurrency, Graphs and Models: Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday Springer Lecture Notes in Computer Science 5065 681–700.Google Scholar
Laneve, C. and Zavattaro, G. (2005) Foundations of web transactions. In: Sassone, V. (ed.) Proceedings of FOSSACS'05. Springer Lecture Notes in Computer Science 3441 282–298.CrossRefGoogle Scholar
Lapadula, A., Pugliese, R. and Tiezzi, F. (2007) A calculus for orchestration of web services. In: De Nicola, R. (ed.) Proceedings of ESOP'07. Springer Lecture Notes in Computer Science 4421 33–47.Google Scholar
Mezzina, L. (2008) How to infer finite session types in a calculus of services and sessions. In: Lea, D. and Zavattaro, G. (eds.), Proceedings of COORDINATION'08. Springer Lecture Notes in Computer Science 5052 216–231.Google Scholar
Mezzina, L. (2009) Typing Services. Ph.D. in Computer Science and Engineering, IMT Institute for Advanced Studies, Lucca.Google Scholar
Milner, R., Parrow, J. and Walker, J. (1992) A calculus of mobile processes, I and II. Information and Computation 100 (1)1–77.Google Scholar
Misra, J. and Cook, W.R. (2007) Computation orchestration: a basis for wide-area computing. Journal of Software and Systems Modeling 6 (1)83–110.Google Scholar
OASIS (2007) Web Services Business Process Execution Language Version 2.0, Working Draft. Available at http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.pdf.Google Scholar
Sensoria Project (2010) Software Engineering for Service-Oriented Overlay Computers. Public Web Site. http://sensoria.fast.de/.Google Scholar
van der Aalst, W.M.P., ter Hofstede, A.H.M., Kiepuszewski, B. and Barros, A.P. (2003) Workflow patterns. Distributed and Parallel Databases 14 (1)5–51.CrossRefGoogle Scholar
Wehrman, I., Kitchin, D., Cook, W.R. and Misra, J. (2008) A timed semantics of Orc. Theoretical Computer Science 402 (2–3)234–248.Google Scholar
Wirsing, M. and Hölzl, M.M. (eds.) (2011) Rigorous Software Engineering for Service-Oriented Systems - Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing. Springer Lecture Notes in Computer Science 6582. ISBN 978-3-642-20400-5.Google Scholar