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
Broadcast psi-calculi with an application to wireless protocols
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)
Show others and affiliations
2015 (English)In: Software and Systems Modeling, ISSN 1619-1366, E-ISSN 1619-1374, Vol. 14, no 1, 201-216 p.Article in journal (Refereed) Published
Abstract [en]

Psi-calculi is a parametric framework for extensions of the pi-calculus, with arbitrary data structures and logical assertions for facts about data. In this paper we add primitives for broadcast communication in order to model wireless protocols. The additions preserve the purity of the psi-calculi semantics, and we formally prove the standard congruence and structural properties of bisimilarity. We demonstrate the expressive power of broadcast psi-calculi by modelling the wireless ad-hoc routing protocol LUNAR and verifying a basic reachability property.

Place, publisher, year, edition, pages
Springer, 2015. Vol. 14, no 1, 201-216 p.
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-205258DOI: 10.1007/s10270-013-0375-zISI: 000349026100012OAI: oai:DiVA.org:uu-205258DiVA: diva2:641007
Projects
UPMARCProFuN
Funder
Swedish Research Council, 2013-4853
Available from: 2013-11-08 Created: 2013-08-15 Last updated: 2017-12-06Bibliographically approved
In thesis
1. Bells and Whistles: Advanced language features in psi-calculi
Open this publication in new window or tab >>Bells and Whistles: Advanced language features in psi-calculi
2013 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Remarkably, machine-checked proofs of standard algebraic and congruence properties of bisimilarity apply to every instance of the framework.

The contribution of this licentiate thesis is to significantly extend the applicability and expressiveness of psi-calculi by incorporating several advanced language features into the framework: broadcasts, higher-order communication, generalised pattern matching, sorts and priorities. The extensions present several interesting technical challenges, such as negative premises. The machine-checked proofs for standard results about bisimilarity are generalised to each of these new settings, and the proof scripts are freely available online.

Place, publisher, year, edition, pages
Uppsala University, 2013
Series
Information technology licentiate theses: Licentiate theses from the Department of Information Technology, ISSN 1404-5117 ; 2013-004
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-227638 (URN)
Supervisors
Projects
UPMARC
Available from: 2013-10-04 Created: 2014-06-29 Last updated: 2017-08-31Bibliographically 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

broadcastPsi.pdf(1158 kB)49 downloads
File information
File name FULLTEXT01.pdfFile size 1158 kBChecksum SHA-512
df9debc22cc9afeac7e4f1a376b2c9d066a6d9c301f8ad1203604084296f1465b9d2611c61f3582a1dc9d6de6c89873411710597724c5dccc224e3ae9f97c99d
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Authority records BETA

Borgström, JohannesJohansson, MagnusRaabjerg, PalleVictor, BjörnÅman Pohjola, JohannesParrow, Joachim

Search in DiVA

By author/editor
Borgström, JohannesJohansson, MagnusRaabjerg, PalleVictor, BjörnÅman Pohjola, JohannesParrow, Joachim
By organisation
Computing Science
In the same journal
Software and Systems Modeling
Computer Science

Search outside of DiVA

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