Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of POPL 2001, pp. 104–115. ACM, New York (2001)
Austry, D., Boudol, G.: Algèbre de processus et synchronisation. Theor. Comput. Sci. 30, 91–131 (1984)
Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: Mobile processes, nominal data, and logic. In: Proceedings of LICS 2009, pp. 39–48. IEEE, Los Alamitos (2009)
Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: A framework for mobile processes with nominal data and logic. Logical Methods in Computer Science (2011), Accepted for publication. This is an extended version of [3]
Ene, C., Muntean, T.: Expressiveness of point-to-point versus broadcast communications. In: Ciobanu, G., Păun, G. (eds.) FCT 1999. LNCS, vol. 1684, pp. 258–268. Springer, Heidelberg (1999)
Gabbay, M., Pitts, A.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13, 341–363 (2001)
Ghassemi, F., Fokkink, W., Movaghar, A.: Restricted broadcast process theory. In: Cerone, A., Gruner, S. (eds.) SEFM, pp. 345–354. IEEE Computer Society, Los Alamitos (2008)
Godskesen, J.C.: A calculus for mobile ad hoc networks. In: Murphy, A.L., Ryan, M. (eds.) COORDINATION 2007. LNCS, vol. 4467, pp. 132–150. Springer, Heidelberg (2007)
Godskesen, J.C.: Observables for mobile and wireless broadcasting systems. In: Clarke, D., Agha, G. (eds.) COORDINATION 2010. LNCS, vol. 6116, pp. 1–15. Springer, Heidelberg (2010)
Johansson, M., Victor, B., Parrow, J.: A fully abstract symbolic semantics for psi-calculi. In: Proceedings of SOS 2009. EPTCS, vol. 18, pp. 17–31 (2010)
Johansson, M., Victor, B., Parrow, J.: Computing strong and weak bisimulations for psi-calculi (submitted for publication, 2011)
Lanese, I., Sangiorgi, D.: An operational semantics for a calculus for wireless systems. Theor. Comp. Sci. 411(19), 1928–1948 (2010)
Merro, M.: An observational theory for mobile ad hoc networks (full version). Inf. Comput. 207(2), 194–208 (2009)
Mezzetti, N., Sangiorgi, D.: Towards a calculus for wireless systems. Electr. Notes Theor. Comput. Sci. 158, 331–353 (2006)
Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)
Milner, R.: Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25, 267–310 (1983)
Nanz, S., Hankin, C.: A framework for security analysis of mobile wireless networks. Theor. Comp. Sci. 367(1-2), 203–227 (2006)
Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation 186, 165–193 (2003)
Prasad, K.V.S.: A calculus of broadcasting systems. In: Abramsky, S., Maibaum, T.S.E. (eds.) CAAP 1991 and TAPSOFT 1991. LNCS, vol. 493, pp. 338–358. Springer, Heidelberg (1991)
Prasad, K.V.S.: A calculus of broadcasting systems. Sci. Comput. Program. 25(2-3), 285–327 (1995)
Raabjerg, P., Åman Pohjola, J.: Broadcast psi-calculus formalisation. Isabelle/HOL-Nominal formalisation of the definitions, theorems and proofs (July 2011), http://www.it.uu.se/research/group/mobility/theorem/broadcastpsi
Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Singh, A., Ramakrishnan, C.R., Smolka, S.A.: A process calculus for mobile ad hoc networks. Sci. Comput. Program. 75(6), 440–469 (2010)
Tschudin, C., Gold, R., Rensfelt, O., Wibling, O.: LUNAR: a lightweight underlay network ad-hoc routing protocol and implementation. In: Proc. of NEW2AN 2004, St. Petersburg (February 2004)
Tschudin, C.F.: Lightweight underlay network ad hoc routing (LUNAR) protocol. Internet Draft, Mobile Ad Hoc Networking Working Group (March 2004)
Urban, C., Tasson, C.: Nominal techniques in isabelle/HOL. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 38–53. Springer, Heidelberg (2005)
Wibling, O.: SPIN and UPPAAL ad hoc routing protocol models. Models of LUNAR scenarios used in [28] (2004), http://www.it.uu.se/research/group/mobility/adhoc/gbt/other_examples
Wibling, O., Parrow, J., Pears, A.: Automatized verification of ad hoc routing protocols. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 343–358. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Borgström, J. et al. (2011). Broadcast Psi-calculi with an Application to Wireless Protocols. In: Barthe, G., Pardo, A., Schneider, G. (eds) Software Engineering and Formal Methods. SEFM 2011. Lecture Notes in Computer Science, vol 7041. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24690-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-24690-6_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24689-0
Online ISBN: 978-3-642-24690-6
eBook Packages: Computer ScienceComputer Science (R0)