Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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
The Psi-Calculi Workbench: A Generic Tool 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
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.

Place, publisher, year, edition, pages
2015. Vol. 14, no 1, 9
National Category
Computer Science
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-233750DOI: 10.1145/2682570ISI: 000349302200009OAI: oai:DiVA.org:uu-233750DiVA: diva2:754138
Projects
ProFuNUPMARC
Funder
Swedish Foundation for Strategic Research , RIT08­0065
Available from: 2015-01-21 Created: 2014-10-09 Last updated: 2017-12-05Bibliographically approved
In thesis
1. Advancing concurrent system verification: Type based approach and tools
Open this publication in new window or tab >>Advancing concurrent system verification: Type based approach and tools
2014 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Concurrent systems, i.e., systems of parallel processes, are nearly ubiquitous and verifying the correctness of such systems is becoming an important subject. Many formalisms were invented for such purpose, however, new types of systems are introduced and there is a need for handling larger systems. One examples is wireless sensor networks that are being deployed in increasing numbers in various areas; and in particular safety-critical areas, e.g., bush fire detection. Thus, ensuring their correctness is important.

A process calculus is a formal language for modeling concurrent systems. The pi-calculus is a prominent example of such a language featuring message-passing concurrency. Psi-calculi is a parametric framework that extends the pi-calculus with arbitrary data and logics. Psi-calculi feature a universal theory with its results checked in an automated theorem prover ensuring their correctness.

In this thesis, we extend psi-calculi expressiveness and modeling precision by introducing a sort system and generalised pattern matching. We show that the extended psi-calculi enjoy the same meta-theoretical results.

We have developed the Pwb, a tool for the psi-calculi framework. The tool provides a high-level interactive symbolic execution and automated behavioral equivalence checking. We exemplify the use of the tool by developing a high-level executable model of a data collection protocol for wireless sensor networks.

We are the first to introduce a session types based system for systems with unreliable communication. Remarkably, we do not need to add specific extensions to the types to accommodate such systems. We prove the standard desirable properties for type systems hold also for our type system.

Place, publisher, year, edition, pages
Uppsala University, 2014
Series
Information technology licentiate theses: Licentiate theses from the Department of Information Technology, ISSN 1404-5117 ; 2014-007
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-233765 (URN)
Presentation
2014-10-20, Room 2446, Polacksbacken, Lägerhyddsvägen 2, Uppsala, 13:15 (English)
Supervisors
Projects
ProFuNUPMARC
Available from: 2014-10-09 Created: 2014-10-09 Last updated: 2017-08-31Bibliographically approved
2. 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

fulltext(1911 kB)48 downloads
File information
File name FULLTEXT01.pdfFile size 1911 kBChecksum SHA-512
a80561739c8d9fd7d1aa83750255ec015edaf64bcc9696757fb7a3f99cf36c38274d169a85164f371181643fb6e3a08bd1bbc223fc9b1eaa231d93bd4b2e2035
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Authority records BETA

Borgström, JohannesGutkovas, RamunasRodhe, IoanaVictor, Björn

Search in DiVA

By author/editor
Borgström, JohannesGutkovas, RamunasRodhe, IoanaVictor, Björn
By organisation
Computing Science
In the same journal
ACM Transactions on Embedded Computing Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 48 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: 642 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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