Compliance and Subtyping in Timed Session Types
Compliance and Subtyping in Timed Session Types
复制标题
定时会话类型中的合规性和子类型
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Livio Pompianu
中科院分区：
文献类型：
--
作者：
Massimo Bartoletti;Tiziana Cimoli;Maurizio Murgia;Alessandro Sebastian Podda;Livio Pompianu
我们提出了一个扩展的二进制会话类型，正式的两个参与者之间的定时通信协议在一个会话的端点。我们引入了一个可判定的合规关系，它概括了定时设置通常的基于进度的概念之间的非定时会话类型的合规性。然后，我们展示了一个健全的和完整的技术来决定何时一个定时会话类型承认一个兼容的，如果是这样的话，构造最少的会话类型符合给定的一个，根据子类型的前序诱导的遵守。根据这些结果可以确定亚型。我们利用我们的理论来设计和实现一个面向消息的中间件，分布式模块与兼容的协议可以动态组成，和他们的通信监控，以保证安全的交互。
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.