uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
A Session Type System for Unreliable Broadcast Communication
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
School of Computing Science, University of Glasgow, UK.
School of Computing Science, University of Glasgow, UK.
(English)Manuscript (preprint) (Other academic)
Abstract [en]

 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.

Keyword [en]
session type, process calculus, broadcast, unreliable
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-300028OAI: oai:DiVA.org:uu-300028DiVA: diva2:950712
Available from: 2016-08-01 Created: 2016-08-01 Last updated: 2016-08-16Bibliographically approved
In thesis
1. Languages, Logics, Types and Tools for Concurrent System Modelling
Open this publication in new window or tab >>Languages, Logics, Types and Tools for Concurrent System Modelling
2016 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

A concurrent system is a computer system with components that run in parallel and interact with each other. Such systems are ubiquitous and are notably responsible for supporting the infrastructure for transport, commerce and entertainment. They are very difficult to design and implement correctly: many different modeling languages and verification techniques have been devised to reason about them and verifying their correctness. However, existing languages and techniques can only express a limited range of systems and properties.

In this dissertation, we address some of the shortcomings of established models and theories in four ways: by introducing a general modal logic, extending a modelling language with types and a more general operation, providing an automated tool support, and adapting an established behavioural type theory to specify and verify systems with unreliable communication.

A modal logic for transition systems is a way of specifying properties of concurrent system abstractly. We have developed a modal logic for nominal transition systems. Such systems are common and include the pi-calculus and psi-calculi. The logic is adequate for many process calculi with regard to their behavioural equivalence even for those that no logic has been considered, for example, CCS, the pi-calculus, psi-calculi, the spi-calculus, and the fusion calculus.

The psi-calculi framework is a parametric process calculi framework that subsumes many existing process calculi. We extend psi-calculi with a type system, called sorts, and a more general notion of pattern matching in an input process. This gives additional expressive power allowing us to capture directly even more process calculi than was previously possible. We have reestablished the main results of psi-calculi to show that the extensions are consistent.

We have developed a tool that is based on the psi-calculi, called the psi-calculi workbench. It provides automation for executing the psi-calculi processes and generating a witness for a behavioural equivalence between processes. The tool can be used both as a library and as an interactive application.

Lastly, we developed a process calculus for unreliable broadcast systems and equipped it with a binary session type system. The process calculus captures the operations of scatter and gather in wireless sensor and ad-hoc networks. The type system enjoys the usual property of subject reduction, meaning that well-typed processes reduce to well-typed processes. To cope with unreliability, we also introduce a notion of process recovery that does not involve communication. This is the first session type system for a model with unreliable communication.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2016. 60 p.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1392
Keyword
process calculus, modal logic, session types, tool
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-300029 (URN)978-91-554-9628-9 (ISBN)
External cooperation:
Public defence
2016-09-09, ITC/2446, Lägerhyddsvägen 2, Uppsala, 10:15 (English)
Opponent
Supervisors
Available from: 2016-08-16 Created: 2016-08-01 Last updated: 2016-08-26Bibliographically approved

Open Access in DiVA

No full text

Search in DiVA

By author/editor
Gutkovas, Ramūnas
By organisation
Department of Information Technology
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 22 hits
ReferencesLink to record
Permanent link

Direct link