Broadcast psi-calculi with an application to wireless protocols

作者：Borgstrom Johannes; Huang Shuqin; Johansson Magnus; Raabjerg Palle; Victor Bjorn^*; Pohjola Johannes Aman; Parrow Joachim

来源：Software and Systems Modeling, 2015, 14(1): 201-216.

DOI：10.1007/s10270-013-0375-z

• Psi-calculus
• Broadcast communication
• Bisimulation
• Ad hoc routing protocol

Psi-calculi is a parametric framework for the extensions of 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.

• 出版日期2015-2
• 单位北京大学