Abstract
Broadcast semantics poses significant challenges over point-to-point communication when it comes to formal modelling and analysis. Current approaches to analysing broadcast networks have focused on fixed connectivities, but this is unsuitable in the case of wireless networks where the dynamically changing network topology is a crucial ingredient. In this paper we develop a static analysis that automatically constructs an abstract transition system, labelled by actions and connectivity information, to yield a mobility-preserving finite abstraction of the behaviour of a network expressed in a process calculus with asynchronous local broadcast. Furthermore, we use model checking based on a 3-valued temporal logic to distinguish network behaviour which differs under changing connectivity patterns.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bettini, L., et al.: The Klaim project: theory and practice. In: Priami, C. (ed.) GC 2003. LNCS, vol. 2874, Springer, Heidelberg (2003)
Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. Journal of the ACM 49(4), 538–576 (2002)
Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Principles of Programming Languages (POPL 1979), pp. 269–282. ACM Press, New York (1979)
Ene, C., Muntean, T.: A broadcast-based calculus for communicating systems. In: Formal Methods for Parallel Programming: Theory and Applications (FMPPTA 2003) (2001)
Hansen, R.R., Probst, C.W., Nielson, F.: Sandboxing in myKlaim. In: Availability, Reliability and Security (ARES 2006), pp. 174–181. IEEE Computer Society Press, Los Alamitos (2006)
Kleene, S.C.: Introduction to Metamathematics. Biblioteca Mathematica, vol. 1. North-Holland, Amsterdam (1952)
Larsen, K.G., Thomsen, B.: A modal process logic. In: Logic in Computer Science (LICS 1988), pp. 203–210. IEEE Computer Society Press, Los Alamitos (1988)
Merro, M.: An observational theory for mobile ad hoc networks. In: Mathematical Foundations of Programming Semantics (MFPS 2007). Electronic Notes in Theoretical Computer Science, vol. 173, pp. 275–293 (2007)
Nanz, S.: Specification and Security Analysis of Mobile Ad-Hoc Networks. PhD thesis, Imperial College London (2006)
Nanz, S., Hankin, C.: A framework for security analysis of mobile wireless networks. Theoretical Computer Science 367(1-2), 203–227 (2006)
Nanz, S., Nielson, F., Nielson, H.R.: Topology-dependent abstractions of broadcast networks. Technical report IMM-TR-2007-11, Technical University of Denmark (2007)
Nicola, R.D., Vaandrager, F.W.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) Semantics of Systems of Concurrent Processes. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)
Nielson, F., Nielson, H.R., Sagiv, M.: A Kleene analysis of mobile ambients. In: Smolka, G. (ed.) ESOP 2000 and ETAPS 2000. LNCS, vol. 1782, pp. 305–319. Springer, Heidelberg (2000)
Nielson, F., Nielson, H.R., Sagiv, M.: Kleene’s logic with equality. Information Processing Letters 80, 131–137 (2001)
Nielson, H.R., Nielson, F.: A monotone framework for CCS. (submitted for publication, 2006)
Nielson, H.R., Nielson, F.: Data flow analysis for CCS. In: Program Analysis and Compilation. Theory and Practice. LNCS, vol. 4444, Springer, Heidelberg (2007)
Prasad, K.V.S.: A calculus of broadcasting systems. Science of Computer Programming 25(2-3), 285–327 (1995)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Principles of Programming Languages (POPL 1999), pp. 105–118. ACM Press, New York (1999)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nanz, S., Nielson, F., Nielson, H.R. (2007). Topology-Dependent Abstractions of Broadcast Networks. In: Caires, L., Vasconcelos, V.T. (eds) CONCUR 2007 – Concurrency Theory. CONCUR 2007. Lecture Notes in Computer Science, vol 4703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74407-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-74407-8_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74406-1
Online ISBN: 978-3-540-74407-8
eBook Packages: Computer ScienceComputer Science (R0)