Hostname: page-component-586b7cd67f-rdxmf Total loading time: 0 Render date: 2024-11-28T17:19:06.491Z Has data issue: false hasContentIssue false
  • English
  • Français

Sub-behaviour relations for session-based client/server systems

Published online by Cambridge University Press:  14 November 2014

FRANCO BARBANERA  and
UGO DE'LIGUORO
FRANCO BARBANERA
Affiliation:
Dipartimento di Matematica e Informatica, University of Catania, Catania, Italy Email: [email protected].
UGO DE'LIGUORO
Affiliation:
Dipartimento di Informatica, University of Torino, Torino, Italy Email: [email protected].
Get access Rights & Permissions [Opens in a new window]

Abstract

We propose a refinement and a simplification of the behavioural semantics of session types, based on the concepts of compliance and sub-behaviour from the theory of web contracts. We introduce three relations on a suitable class of behaviours with higher-order input/output, called ‘session behaviours’. Such relations, depending on each other, represent the idea of sub-behaviour from the point of view of a client, a server or a peer, respectively. A restriction of the intersection of the first two relations characterizes the ‘usual’ sub-behaviour relation from the literature. We then device an algorithmic formal system for three subtyping relations (dubbed CSP-subtyping) for session types that takes into account the role played by a user of a channel during an interaction, so extending Gay and Hole subtyping theory. We show that our session behaviours and sub-behaviour relations provide sound and complete semantics for CSP-subtyping, and for Gay and Hole subtyping as a by-product.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 25 , Issue 6 , September 2015 , pp. 1339 - 1381
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.)

References

Amadio, R. and Cardelli, L. (1993) Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15 (4) 575–631.CrossRefGoogle Scholar
Barbanera, F., Capecchi, S. and de'Liguoro, U. (2010) Typing asymmetric client-server interaction. In: Proceedings of FSEN'09. Lecture Notes in Computer Science 5961 97–112.Google Scholar
Barbanera, F. and de'Liguoro, U. (2010) Two notions of sub-behaviour for session-based client/server systems. In: Proceedings of PPDP'10. ACM SIGPLAN 155–164.Google Scholar
Bernardi, G. and Hennessy, M. (2013a) Modelling session types using contracts. Mathematical Structures in Computer Science, To appear.Google Scholar
Bernardi, G. and Hennessy, M. (2013b) Mutually testing processes - (Extended Abstract). In: Proceedings of CONCUR'13. Lecture Notes in Computer Science 8052 61–75.Google Scholar
Bernardi, G. and Hennessy, M. (2013c) Using higher-order contracts to model session types. In: http://adsabs.harvard.edu/abs/2013arXiv1310.6176B.Google Scholar
Brandt, M. and Henglein, F. (1998) Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticae 33 (4) 309–338.Google Scholar
Bravetti, M. and Zavattaro, G. (2007) Contract based multi-party service composition. In: Proceedings of FSEN'07. Springer Lecture Notes in Computer Science 4767 207–222.CrossRefGoogle Scholar
Bravetti, M. and Zavattaro, G. (2008) A foundational theory of contracts for multi-party service composition. Fundamamenta Informaticae 89 (4) 451–478.Google Scholar
Carpineti, S., Castagna, G., Laneve, C. and Padovani, L. (2006) A formal account of contracts for Web Services. In: Proceedings of WS-FM'06. Lecture Notes in Computer Science 4184 148–162.Google Scholar
Castagna, G., Dezani-Ciancaglini, M., Giachino, E. and Padovani, L. (2009) Foundations of session types. In: Proceedings of PPDP'09, ACM Press 219–230.Google Scholar
Castagna, G. and Frisch, A. (2005) A gentle introduction to semantic subtyping. In: Proceedings of ICALP'05. Lecture Notes in Computer Science 3580 30–34.Google Scholar
Castagna, G., Gesbert, N. and Padovani, L. (2009) A theory of contracts for web services. ACM Transactions on Programming Languages and Systems (TOPLAS)volume 31, number 5.Google Scholar
Castagna, G. and Padovani, L. (2009) Contracts for mobile processes. In: Proceedings CONCUR'09. Lecture Notes in Computer Science 5710 211–228.CrossRefGoogle Scholar
De Nicola, R. and Hennessy, M. (1987) CCS without tau's. In: Proceedings of TAPSOFT'87. Lecture Notes in Computer Science 249 138–152.Google Scholar
De Nicola, R. and Hennessy, M. (1993) Testing equivalence for processes. In: Proceedings of ICALP'83. Lecture Notes in Computer Science 154 548–560.Google Scholar
Dezani-Ciancaglini, M., de' Liguoro, U. and Yoshida, N. (2008) On progress for Structured communications. In: Proceedings of TGC'07. Lecture Notes in Computer Science 4912 257–275.Google Scholar
Gapeyev, V., Levin, M. Y. and Pierce, B. C. (2002) Recursive subtyping revealed. Journal of Functional Programming 12 (6) 511–548.Google Scholar
Gay, S. and Hole, M. (1999) Types and subtypes for client-server interactions. In: Proceedings of ESOP'99. Lecture Notes in Computer Science 1576 74–90.CrossRefGoogle Scholar
Gay, S. and Hole, M. (2005) Subtyping for session types in the Pi-calculus. Acta Informatica 42 (2) 191–225.Google Scholar
Honda, K., Vasconcelos, V. T. and Kubo, M. (1998) Language primitives and type disciplines for structured communication-based programming. In: Proceedings of ESOP'98. Lecture Notes in Computer Science 1381 22–138.Google Scholar
Laneve, C. and Padovani, L. (2007) The must preorder revisited: An algebraic theory for web services contracts. In: Proceedings of CONCUR'07. Lecture Notes in Computer Science 4703 212–225.Google Scholar
Laneve, C. and Padovani, L. (2008) The pairing of contracts and session types. In: Concurrency, Graphs and Models. Lecture Notes in Computer Science 5065 681–700.CrossRefGoogle Scholar
Leavens, G. T. and Pigozzi, D. (2000) A complete algebraic characterization of behavioral subtyping. Acta Informatica 36 (8) 617–663.CrossRefGoogle Scholar
Padovani, L. (2010) Contract-based discovery and adaptation of web services. Theoretical Computer Science 411 (37) 3328–3347.Google Scholar
Padovani, L. (2009) Session types at the mirror. In: Proceedings of IVE'09. Electronic Proceedings in Theoretical Computer Science 12 71–86.Google Scholar
Padovani, L. (2011) Private communication.Google Scholar
Padovani, L. (2012) On projecting processes into session types. Mathematical Structures in Computer Science 22 (2) 237–289.Google Scholar
Padovani, L. (2013) Fair subtyping for multi-party session types. Mathematical Structures in Computer Science, To appear.Google Scholar
Pierce, B. and Sangiorgi, D. (1996) Typing and subtyping for mobile processes. Mathematical Structures in Computer Science 6 (5) 409–453.Google Scholar
Ravara, A., Resende, P. and Vasconcelos, V. T. (2012) An algebra of behavioural types. Information and Computation 212 64–91.Google Scholar
Rensink, A. and Vogler, W. (2007) Fair testing. Information and Computation 205 (2) 125–198.Google Scholar
Sangiorgi, D. and Walker, D. (2001) The π-Calculus: A Theory of Mobile Processes, Cambridge University Press.Google Scholar
Yoshida, N. and Vasconcelos, V. T. (2007) Language primitives and type disciplines for structured communication-based programming revisited. In: Proceedings of SecReT'06. Electronic Notes in Theoretical Computer Science 171 73–93.Google Scholar