Abstract
We provide a framework for modeling and analyzing both qualitative and quantitative aspects of mobile ad hoc network (MANET) protocols above the data-link layer. We extend Restricted Broadcast Process Theory [11,9]: delay functions are assigned to actions, while the semantics captures the interplay of a MANET protocol with stochastic behavior of the data-link and physical layer, and the dynamic topology. A continuous-time Markov chain is derived from our semantic model by resolving non-determinism, using the notion of weak Markovian network bisimilarity. The framework is applied to a leader election algorithm.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.: On the logical characterisation of performability properties. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 780–792. Springer, Heidelberg (2000)
Bernardo, M., Gorrieri, R.: A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time. Theoretical Computer Science 202(1-2), 1–54 (1998)
Blom, S., van de Pol, J.: State space reduction by proving confluence. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 596–609. Springer, Heidelberg (2002)
Daws, C., Kwiatkowska, M., Norman, G.: Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. Software Tools for Technology Transfer 5(2), 221–236 (2004)
Duflot, M., Kwiatkowska, M., Norman, G., Parker, D.: A formal analysis of Bluetooth device discovery. In: Proc. ISOLA 2004, pp. 268–275 (2004)
Ehrich, H., Loeckx, J., Wolf, M.: Specification of Abstract Data Types. John Wiley, Chichester (1996)
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)
Fehnker, A., Fruth, M., McIver, A.K.: Graphical modelling for simulation and formal analysis of wireless network protocols. In: Butler, M., Jones, C., Romanovsky, A., Troubitsyna, E. (eds.) Methods, Models and Tools for Fault Tolerance. LNCS, vol. 5454, pp. 1–24. Springer, Heidelberg (2009)
Ghassemi, F., Fokkink, W., Movaghar, A.: Equational reasoning on mobile ad hoc networks. Fundamenta Informaticae 103, 1–41 (2010)
Ghassemi, F., Fokkink, W., Movaghar, A.: Verification of mobile ad hoc networks: An algebraic approach. Theoretical Computer Science 412(28), 3262–3282 (2011)
Ghassemi, F., Fokkink, W.J., Movaghar, A.: Restricted broadcast process theory. In: Proc. SEFM 2008, pp. 345–354. IEEE, Los Alamitos (2008)
Ghassemi, F., Fokkink, W.J., Movaghar, A.: Towards performance evaluation of mobile ad hoc network protocols. In: Proc. ACSD 2010, pp. 98–105. IEEE, Los Alamitos (2010)
Ghassemi, F., Talebi, M.: Fokkink, W., Movaghar, A.: Stochastic restricted broadcast process theory. Tech. rep., Sharif University of Technology (2011), http://mehr.sharif.edu/fghassemi/srbpt-web.pdf
van Glabbeek, R., Weijland, W.: Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), 555–600 (1996)
Groote, J.F., Ponse, A.: Syntax and semantics of μ-CRL. In: Proc. ACP 1994. Workshops in Computing, pp. 26–62. Springer, Heidelberg (1995)
Hermanns, H., Herzog, U., Katoen, J.P.: Process algebra for performance evaluation. Theoretical Computer Science 274(1-2), 43–87 (2002)
Hermanns, H., Rettelbach, M., Weiss, T.: Formal characterisation of immediate actions in spa with nondeterministic branching. The Computer Journal 38(7), 530–541 (1995)
Hillston, J.: A Compositional Approach to Performance Modelling. Ph.D. thesis, Cambridge University (1996)
Khabbazian, M., Kuhn, F., Kowalski, D.R., Lynch, N.A.: Decomposing broadcast algorithms using abstract mac layers. In: Proc. DIALM-PODC, pp. 13–22. ACM, New York (2010)
Kloul, L., Valois, F.: Investigating unfairness scenarios in manet using 802.11b. In: Proc. PE-WASUN, pp. 1–8. ACM, New York (2005)
Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design 29, 33–78 (2006)
Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399, pp. 169–187. Springer, Heidelberg (2002)
Lin, T.: Mobile Ad-hoc Network Routing Protocols: Methodologies and Applications. Ph.D. thesis, Virginia Polytechnic Institute and State University (2004)
Oliveira, R., Bernardo, L., Pinto, P.: Modelling delay on IEEE 802.11 MAC protocol for unicast and broadcast nonsaturated traffic. In: Proc. WCNC 2007, pp. 463–467. IEEE, Los Alamitos (2007)
Razafindralambo, T., Valois, F.: Performance evaluation of backoff algorithms in 802.11 ad-hoc networks. In: Proc. PE-WASUN 2006, pp. 82–89. ACM, New York (2006)
Timmer, M.: Scoop: A tool for symbolic optimisations of probabilistic processes. In: QEST 2011 (to appear, 2011)
Vasudevan, S., Kurose, J., Towsley, D.: Design and analysis of a leader election algorithm for mobile ad hoc networks. In: Proc. ICNP 2004, pp. 350–360. IEEE, Los Alamitos (2004)
Zuniga, M., Krishnamachari, B.: Analyzing the transitional region in low power wireless links. In: Proc. SECON 2004, pp. 517–526. IEEE, Los Alamitos (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
Ghassemi, F., Talebi, M., Movaghar, A., Fokkink, W. (2011). Stochastic Restricted Broadcast Process Theory. In: Thomas, N. (eds) Computer Performance Engineering. EPEW 2011. Lecture Notes in Computer Science, vol 6977. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24749-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-24749-1_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24748-4
Online ISBN: 978-3-642-24749-1
eBook Packages: Computer ScienceComputer Science (R0)