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
Extending psi-calculi and their formal proofs
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)
2012 (English)Licentiate thesis, comprehensive summary (Other academic)
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. This thesis presents broadcast psi-calculi and higher-order psi-calculi, two extensions of the psi-calculi framework, allowing respectively one-to-many communications and the use of higher-order process descriptions through conditions in the parameterised logic. Both extensions preserve the purity of the psi-calculi semantics; the standard congruence and structural properties of bisimilarity are proved formally in Isabelle. The work going into the extensions show that depending on the specific extension, working out the formal proofs can be a work-intensive process. We find that some of this work could be automated, and implementing such automation may facilitate the development of future extensions to the psi-calculi framework.

Place, publisher, year, edition, pages
Uppsala University, 2012.
Series
Information technology licentiate theses: Licentiate theses from the Department of Information Technology, ISSN 1404-5117 ; 2012-008
National Category
Computer Science
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-183614OAI: oai:DiVA.org:uu-183614DiVA: diva2:563554
Presentation
2012-11-15, Room 1211, Polacksbacken, Lägerhyddsvägen 2, Uppsala, 10:15 (English)
Supervisors
Projects
UPMARC
Funder
Swedish Research Council
Available from: 2012-11-15 Created: 2012-10-30 Last updated: 2017-08-31Bibliographically approved
List of papers
1. Broadcast Psi-calculi with an Application to Wireless Protocols
Open this publication in new window or tab >>Broadcast Psi-calculi with an Application to Wireless Protocols
Show others...
2011 (English)In: Software Engineering and Formal Methods: SEFM 2011, Springer Berlin/Heidelberg, 2011, 74-89 p.Conference paper, Published paper (Refereed)
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 % to the psi-calculi framework. 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 Berlin/Heidelberg, 2011
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7041
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-156736 (URN)10.1007/978-3-642-24690-6_7 (DOI)978-3-642-24689-0 (ISBN)
Conference
9th International Conference on Software Engineering and Formal Methods, November 14-18, 2011, Montevideo, Uruguay
Projects
ProFuNUPMARC
Available from: 2011-12-06 Created: 2011-08-08 Last updated: 2016-02-25Bibliographically approved
2. Higher-order psi-calculi
Open this publication in new window or tab >>Higher-order psi-calculi
2014 (English)In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 24, no 2, e240203Article in journal (Refereed) Published
Abstract [en]

Psi-calculi is a parametric framework for extensions of the pi-calculus; in earlier work we have explored their expressiveness and algebraic theory. In this paper we consider higher-order psi-calculi through a technically surprisingly simple extension of the framework, and show how an arbitrary psi-calculus can be lifted to its higher-order counterpart in a canonical way. We illustrate this with examples and establish an algebraic theory of higher-order psi-calculi. The formal results are obtained by extending our proof repositories in Isabelle/Nominal.

Place, publisher, year, edition, pages
Cambridge University Press, 2014
Keyword
process calculi, psi calculi, isabelle, theorem proving, nominal, higher-order
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-183610 (URN)10.1017/S0960129513000170 (DOI)000343643500003 ()
Projects
UPMARCProFuN
Funder
Swedish Foundation for Strategic Research
Available from: 2013-06-24 Created: 2012-10-30 Last updated: 2017-12-07Bibliographically approved

Open Access in DiVA

fulltext(1083 kB)112 downloads
File information
File name FULLTEXT01.pdfFile size 1083 kBChecksum SHA-512
b44598fc4c29742911dd3e5f2309e441ba682d953648134ed92e5a4b8596dbe038b508b089349c199af314662c87cf6e898bc5c1735a488d1815f164b9ebf481
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Raabjerg, Palle
By organisation
Division of Computing ScienceComputing Science
Computer Science

Search outside of DiVA

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