A Session Type System for Unreliable Broadcast Communication
(English)Manuscript (preprint) (Other academic)
Session types are formal specifications of communication protocols, allowing protocol implementations to be verified by typechecking. Up to now, session type disciplines have assumed that the communication medium is reliable, with no loss of messages. However, unreliable broadcast communication is common in a wide class of distributed systems such as ad-hoc and wireless sensor networks. Often such systems have structured communication patterns that should be amenable to analysis by means of session types. We introduce a process calculus with unreliable broadcast communication, and equip it with a session type system that we show is sound. We capture two common operations, scatter and gather, inhabiting dual session types. To cope with unreliability in a session we introduce an autonomous recovery mechanism that does not require acknowledgements from session participants. Our session type formalisation is the first to consider unreliable communication.
session type, process calculus, broadcast, unreliable
IdentifiersURN: urn:nbn:se:uu:diva-300028OAI: oai:DiVA.org:uu-300028DiVA: diva2:950712