%0 Conference Proceedings
%T Compliance and Subtyping in Timed Session Types
%+ Università degli Studi di Cagliari = University of Cagliari (UniCa)
%A Bartoletti, Massimo
%A Cimoli, Tiziana
%A Murgia, Maurizio
%A Podda, Alessandro, Sebastian
%A Pompianu, Livio
%Z Part 3: Real Time Systems
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Grenoble, France
%Y Susanne Graf
%Y Mahesh Viswanathan
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-9039
%P 161-177
%8 2015-06-02
%D 2015
%R 10.1007/978-3-319-19195-9_11
%K Service Composition
%K Success State
%K Session Type
%K Follow Theorem State
%K Runtime Monitoring
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X We propose an extension of binary session types, to formalise timed communication protocols between two participants at the endpoints of a session. We introduce a decidable compliance relation, which generalises to the timed setting the usual progress-based notion of compliance between untimed session types. We then show a sound and complete technique to decide when a timed session type admits a compliant one, and if so, to construct the least session type compliant with a given one, according to the subtyping preorder induced by compliance. Decidability of subtyping follows from these results. We exploit our theory to design and implement a message-oriented middleware, where distributed modules with compliant protocols can be dynamically composed, and their communications monitored, so to guarantee safe interactions.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01767334/document
%2 https://inria.hal.science/hal-01767334/file/978-3-319-19195-9_11_Chapter.pdf
%L hal-01767334
%U https://inria.hal.science/hal-01767334
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-9039