Broadcast Psi-calculi with an Application to Wireless Protocols
2011 (English)In: Software Engineering and Formal Methods: SEFM 2011, Springer Berlin/Heidelberg, 2011, 74-89 p.Conference paper (Refereed)
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.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 7041
IdentifiersURN: urn:nbn:se:uu:diva-156736DOI: 10.1007/978-3-642-24690-6_7ISBN: 978-3-642-24689-0OAI: oai:DiVA.org:uu-156736DiVA: diva2:433096
9th International Conference on Software Engineering and Formal Methods, November 14-18, 2011, Montevideo, Uruguay