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
Broadcast Psi-calculi with an Application to Wireless Protocols
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)
Peking University, China.
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)
Show others and affiliations
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. 74-89 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7041
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-156736DOI: 10.1007/978-3-642-24690-6_7ISBN: 978-3-642-24689-0 (print)OAI: oai:DiVA.org:uu-156736DiVA: diva2:433096
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
In thesis
1. Extending psi-calculi and their formal proofs
Open this publication in new window or tab >>Extending psi-calculi and their formal proofs
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:nbn:se:uu:diva-183614 (URN)
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

Open Access in DiVA

fulltext(341 kB)352 downloads
File information
File name FULLTEXT02.pdfFile size 341 kBChecksum SHA-512
6fc7bb2e2ea6e6fa42a0a80eabdcd181b64ecf48bddef68de28e69e8bcd57fe0bc809e37684c936c1d0fb900d247c82b0f9c14a5ef6639bab02d909f0511ae7d
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Borgström, JohannesJohansson, MagnusRaabjerg, PalleVictor, BjörnÅman Pohjola, JohannesParrow, Joachim
By organisation
Computing Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 352 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
isbn
urn-nbn

Altmetric score

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