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

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A Sorted Semantic Framework for Applied Process Calculi
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)ORCID iD: 0000-0001-5990-5742
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)ORCID iD: 0000-0003-0174-9032
Show others and affiliations
2016 (English)In: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 12, no 1, 1-49 p., 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.

Place, publisher, year, edition, pages
2016. Vol. 12, no 1, 1-49 p., 8
Keyword [en]
Expressiveness, Pattern matching, Type systems, Theorem proving, pi-calculus, Nominal sets
National Category
Computer Science
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-262199DOI: 10.2168/LMCS-12(1:8)2016ISI: 000374769600004OAI: oai:DiVA.org:uu-262199DiVA: diva2:852687
Funder
Swedish Research Council, 2013-4853
Available from: 2016-03-31 Created: 2015-09-09 Last updated: 2017-11-25Bibliographically 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
2. Culling Concurrency Theory: Reusable and trustworthy meta-theory, proof techniques and separation results
Open this publication in new window or tab >>Culling Concurrency Theory: Reusable and trustworthy meta-theory, proof techniques and separation results
2016 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

As concurrent systems become ever more complex and ever more ubiquitous, the need to understand and verify them grows ever larger. For this we need formal modelling languages that are well understood, with rigorously verified foundations and proof techniques, applicable to a wide variety of concurrent systems.

Defining modelling languages is easy; there is a stupefying variety of them in the literature. Verifying their foundations and proof techniques, and developing an understanding of their interrelationship with other modelling languages, is difficult, tedious and error-prone. The contributions of this thesis support these tasks in reusable and trustworthy ways, by results that apply to a wide variety of modelling languages, verified to the highest standards of mathematical rigour in an interactive theorem prover.

To this end, we extend psi-calculi - a family of process calculi with reusable foundations for formal verification - with several new language features. We prove that the bisimulation meta-theory of psi-calculi carries over to these extended settings. This widens the scope of psi-calculi to important application areas, such as cryptography and wireless communication. We develop bisimulation up-to techniques - powerful proof techniques for showing that two processes exhibit the same observable behaviour - that apply to all psi-calculi. By showing how psi-calculi can encode dynamic priorities under very strong quality criteria, we demonstrate that the expressive power is greater than previously thought. Finally, we develop a simple and widely applicable technique for showing that a process calculus adds expressiveness over another, based on little more than whether parallel components may act independently or not. Many separation results, both novel ones and strengthenings of known results from the literature, emerge as special cases of this technique.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2016. 113 p.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1397
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-297488 (URN)978-91-554-9639-5 (ISBN)
External cooperation:
Public defence
2016-09-22, ITC/2446, Lägerhyddsvägen 2, Uppsala, 13:15 (English)
Opponent
Supervisors
Available from: 2016-08-26 Created: 2016-06-23 Last updated: 2016-09-05Bibliographically approved

Open Access in DiVA

fulltext(562 kB)6 downloads
File information
File name FULLTEXT01.pdfFile size 562 kBChecksum SHA-512
1037974e2ec316a060b984ee646443aea2ad96799940d3c1b13a48266b5ec1a987d59af9c0a4e58591c26a2dc76bb66acd825818aeeb968b4cd6cdbe6348d134
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Authority records BETA

Borgström, JohannesGutkovas, RamunasParrow, JoachimVictor, BjörnÅman Pohjola, Johannes

Search in DiVA

By author/editor
Borgström, JohannesGutkovas, RamunasParrow, JoachimVictor, BjörnÅman Pohjola, Johannes
By organisation
Computing Science
In the same journal
Logical Methods in Computer Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 6 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

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 740 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf