Broadcast psi-calculi with an application to wireless protocols
2015 (English)In: Software and Systems Modeling, ISSN 1619-1366, E-ISSN 1619-1374, Vol. 14, no 1, 201-216 p.Article in journal (Refereed) Published
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 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, 2015. Vol. 14, no 1, 201-216 p.
IdentifiersURN: urn:nbn:se:uu:diva-205258DOI: 10.1007/s10270-013-0375-zISI: 000349026100012OAI: oai:DiVA.org:uu-205258DiVA: diva2:641007
FunderSwedish Research Council, 2013-4853