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
Advancing concurrent system verification: Type based approach and tools
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. (Mobility)
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: urn:nbn:se:uu:diva-233765OAI: oai:DiVA.org:uu-233765DiVA: diva2:754219
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
List of papers
1. 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: 2017-12-05Bibliographically approved
2. Session types for broadcasting
Open this publication in new window or tab >>Session types for broadcasting
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)
Series
Electronic Proceedings in Theoretical Computer Science, 155
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-230882 (URN)10.4204/EPTCS.155.4 (DOI)
Conference
PLACES 2014, April 12, Grenoble, France
Projects
ProFuN
Available from: 2014-06-13 Created: 2014-09-01 Last updated: 2014-10-27Bibliographically approved
3. A Sorted Semantic Framework for Applied Process Calculi (extended abstract)
Open this publication in new window or tab >>A Sorted Semantic Framework for Applied Process Calculi (extended abstract)
Show others...
2014 (English)In: Trustworthy Global Computing: TGC 2013, Springer Berlin/Heidelberg, 2014, 103-118 p.Conference paper, Published paper (Refereed)
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 accommodate 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. Substantial parts of the meta-theory of sorted psi-calculi have been machine-checked using Nominal Isabelle.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2014
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8358
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-203382 (URN)10.1007/978-3-319-05119-2_7 (DOI)978-3-319-05118-5 (ISBN)
Conference
8th International Symposium on Trustworthy Global Computing, August 30-31, 2013, Buenos Aires, Argentina
Projects
UPMARCProFuN
Funder
Swedish Foundation for Strategic Research , RIT08­0065
Available from: 2014-03-08 Created: 2013-07-09 Last updated: 2016-02-25

Open Access in DiVA

fulltext(2097 kB)197 downloads
File information
File name FULLTEXT01.pdfFile size 2097 kBChecksum SHA-512
5b9995e770dfc9ad58ab3ead1675d42f23f2a2ce18958a3f4dd9d65e97ec99b62671f6cae0107e78fb323c4cc56f36ae8d32e63819e580a0709c4d6381f58d69
Type fulltextMimetype application/pdf

Authority records BETA

Gutkovas, Ramunas

Search in DiVA

By author/editor
Gutkovas, Ramunas
By organisation
Division of Computing ScienceComputing Science
Computer Science

Search outside of DiVA

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

urn-nbn

Altmetric score

urn-nbn
Total: 576 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