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 (extended abstract)
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)
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
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. 103-118 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8358
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-203382DOI: 10.1007/978-3-319-05119-2_7ISBN: 978-3-319-05118-5 (print)OAI: oai:DiVA.org:uu-203382DiVA: diva2:636375
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
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. 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

No full text

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
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 548 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