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
Session types for broadcasting
University of Glasgow.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)
University of Glasgow.
2014 (English)In: Proc. 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, 2014, 25-31 p.Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
2014. 25-31 p.
Series
Electronic Proceedings in Theoretical Computer Science, 155
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-230882DOI: 10.4204/EPTCS.155.4OAI: oai:DiVA.org:uu-230882DiVA: diva2:742347
Conference
PLACES 2014, April 12, Grenoble, France
Projects
ProFuN
Available from: 2014-06-13 Created: 2014-09-01 Last updated: 2014-10-27Bibliographically 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

Open Access in DiVA

fulltext(85 kB)180 downloads
File information
File name FULLTEXT01.pdfFile size 85 kBChecksum SHA-512
87e76e51d9a2026a492916db2045d405180f94e78f5200bedf6ea030a5862fb62ddfdabac5f8b5137c79fa1edc5168eccf4fc7ad5ddc5d66ecdd556afbbe39d8
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Authority records BETA

Gutkovas, Ramunas

Search in DiVA

By author/editor
Gutkovas, Ramunas
By organisation
Computing Science
Computer Science

Search outside of DiVA

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