Change search
ReferencesLink to record
Permanent link

Direct link
Languages, Logics, Types and Tools for Concurrent System Modelling
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computing Science. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
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 [en]
process calculus, modal logic, session types, tool
National Category
Computer Science
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-300029ISBN: 978-91-554-9628-9OAI: oai:DiVA.org:uu-300029DiVA: diva2:950714
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
List of papers
1. Modal Logics for Nominal Transition Systems
Open this publication in new window or tab >>Modal Logics for Nominal Transition Systems
Show others...
(English)Manuscript (preprint) (Other academic)
Abstract [en]

We define a uniform semantic substrate for a wide variety of process calculi where states and action labels can be from arbitrary nominal sets. A Hennessy-Milner logic for these systems is introduced, and proved adequate for bisimulation equivalence. A main novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late, open and weak in a systematic way, and make substantial comparisons with related work. The main definitions and theorems have been formalized in Nominal Isabelle. 

Keyword
modal logic, process calculi, nominal transition system, adequacy, bisimulation
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-300027 (URN)
Available from: 2016-08-01 Created: 2016-08-01 Last updated: 2016-08-16
2. A Sorted Semantic Framework for Applied Process Calculi
Open this publication in new window or tab >>A Sorted Semantic Framework for Applied Process Calculi
Show others...
2016 (English)In: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 12, no 1, 8Article in journal (Refereed) Published
Abstract [en]

Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondeterminism, process creation, and dynamic connection topologies. Several such formalisms, e.g. the applied pi calculus, are extensions of the the pi-calculus; a growing number is geared towards particular applications or computational paradigms.

Our goal is a unified framework to represent different process calculi and notions of computation. To this end, we extend our previous work on psi-calculi with novel abstract patterns and pattern matching, and add sorts to the data term language, giving sufficient criteria for subject reduction to hold. Our framework can directly represent several existing process calculi; the resulting transition systems are isomorphic to the originals up to strong bisimulation. We also demonstrate different notions of computation on data terms, including cryptographic primitives and a lambda-calculus with erratic choice. Finally, we prove standard congruence and structural properties of bisimulation; the proof has been machine-checked using Nominal Isabelle in the case of a single name sort.

Keyword
Expressiveness; Pattern matching; Type systems; Theorem proving; pi-calculus; Nominal sets
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-262199 (URN)10.2168/LMCS-12(1:8)2016 (DOI)000374769600004 ()
Available from: 2016-03-31 Created: 2015-09-09 Last updated: 2016-08-26Bibliographically approved
3. A Session Type System for Unreliable Broadcast Communication
Open this publication in new window or tab >>A Session Type System for Unreliable Broadcast Communication
(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
session type, process calculus, broadcast, unreliable
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-300028 (URN)
Available from: 2016-08-01 Created: 2016-08-01 Last updated: 2016-08-16Bibliographically approved
4. The Psi-Calculi Workbench: A Generic Tool for Applied Process Calculi
Open this publication in new window or tab >>The Psi-Calculi Workbench: A Generic Tool for Applied Process Calculi
2015 (English)In: ACM Transactions on Embedded Computing Systems, ISSN 1539-9087, E-ISSN 1558-3465, Vol. 14, no 1, 9Article in journal (Refereed) Published
Abstract [en]

Psi-calculi is a parametric framework for extensions of the pi-calculus with arbitrary data and logic. All instances of the framework inherit machine-checked proofs of the metatheory such as compositionality and bisimulation congruence. We present a generic analysis tool for psi-calculus instances, enabling symbolic execution and (bi)simulation checking for both unicast and broadcast communication. The tool also provides a library for implementing new psi-calculus instances. We provide examples from traditional communication protocols and wireless sensor networks. We also describe the theoretical foundations of the tool, including an improved symbolic operational semantics, with additional support for scoped broadcast communication.

National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-233750 (URN)10.1145/2682570 (DOI)000349302200009 ()
Projects
ProFuNUPMARC
Funder
Swedish Foundation for Strategic Research , RIT08­0065
Available from: 2015-01-21 Created: 2014-10-09 Last updated: 2016-08-16Bibliographically approved

Open Access in DiVA

fulltext(575 kB)43 downloads
File information
File name FULLTEXT01.pdfFile size 575 kBChecksum SHA-512
650f45cba07468a19811d7d84e1c24445340d2075150f222fba9f34108d5a5117b4c3cca9e1d5c1423d949037ff2209ef9f15c13260a2d404821c16e0f329117
Type fulltextMimetype application/pdf
Buy this publication >>

Search in DiVA

By author/editor
Gutkovas, Ramūnas
By organisation
Division of Computing ScienceComputing Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 43 downloads
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: 616 hits
ReferencesLink to record
Permanent link

Direct link