Cited By
View all- Ghassemi FFokkink W(2016)Model checking mobile ad hoc networksFormal Methods in System Design10.1007/s10703-016-0254-749:3(159-189)Online publication date: 1-Dec-2016
Ad hoc routing protocol verification through broadcast abstraction
Pages 128 - 142
Abstract
We present an improved method for analyzing route establishment in ad hoc routing protocols. An efficient abstraction for Propagating Localized Broadcast with Dampening (PLBD) is developed. Applying this result we are able to verify networks and topology changes for ad hoc networks up to the limits currently envisaged for operational mobile ad hoc networks (MANETS). Results are reported for route discovery in the Lightweight Underlay Network Ad hoc Routing protocol (LUNAR) using UPPAAL and we provide an outline of how similar verifications can be conducted for DSR.
References
[1]
Tschudin, C., Gold, R., Rensfelt, O., Wibling, O.: LUNAR: a lightweight underlay network ad-hoc routing protocol and implementation. In: Proc. Next Generation Teletraffic and Wired/Wireless Advanced Networking (NEW2AN). (2004)
[2]
Johnson, D. B., Maltz, D. A., Hu, Y.C.: Internet draft: The dynamic source routing protocol for mobile ad hoc networks (DSR). http://www.ietf.org/ internet-drafts/draft-ietf-manet-dsr-10.txt (2004)
[3]
Larsen, K. G., Pettersson, P., Yi, W.: Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer 1 (1997) 134-152
[4]
Wibling, O., Parrow, J., Pears, A.: Automatized verification of ad hoc routing protocols. In: Proc. 24th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE). (2004)
[5]
Ni, S.Y., Tseng, Y.C., Chen, Y. S., Sheu, J. P.: The broadcast storm problem in a mobile ad hoc network. In: Proc. ACM MobiCom. (1999) 151-162
[6]
Wibling, O.: LUNAR pseudo code description. http://user.it.uu.se/~oskarw/ lunar_pseudo_code/ (2005)
[7]
Xiao, Y., Rosdahl, J.: Throughput and delay limits of IEEE 802.11. IEEE Communications Letters 6 (2002) 355-357
[8]
Lundgren, H.: Implementation and Experimental Evaluation of Wireless Ad Hoc Routing Protocols. Phd thesis, Uppsala University (2005)
[9]
Chiyangwa, S., Kwiatkowska, M.: A timing analysis of AODV. In: Proc. Formal Methods for Open Object-Based Distributed Systems: 7th IFIP WG 6.1 International Conference (FMOODS). (2005)
[10]
Perkins, C. E., Royer, E. M.: Ad hoc on-demand distance vector routing. In: Proc. 2nd IEEE Workshop on Mobile Computing Systems and Applications. (1999) 90- 100
[11]
Obradovic, D.: Formal Analysis of Routing Protocols. Phd thesis, University of Pennsylvania (2002)
[12]
Holzmann, G.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading, Massachusetts (2003)
[13]
University of Cambridge Computer Laboratory: Automated reasoning group HOL page. http://www.cl.cam.ac.uk/Research/HVG/HOL/ (2005)
[14]
Das, S., Dill, D. L.: Counter-example based predicate discovery in predicate abstraction. In: Formal Methods in Computer-Aided Design, Springer-Verlag (2002)
[15]
de Renesse, R., Aghvami, A.: Formal verification of ad-hoc routing protocols using SPIN model checker. In: 12th Mediterranean Electrotechnical Conference (IEEE MELECON). (2004)
[16]
Xiong, C., Murata, T., Tsai, J.: Modeling and simulation of routing protocol for mobile ad hoc networks using colored Petri nets. In: Proc. Workshop on Formal Methods Applied to Defence Systems in Formal Methods in Software Engineering and Defence Systems. (2002)
[17]
Xiong, C., Murata, T., Leigh, J.: An approach to verifying routing protocols in mobile ad hoc networks using Petri nets. In: Proc. IEEE 6th CAS Symposium on Emerging Technologies: Frontiers of Mobile and Wireless Communication. (2004)
- Ad hoc routing protocol verification through broadcast abstraction
Recommendations
A weight-based clustering multicast routing protocol for mobile ad hoc networks
In mobile ad hoc networks, the mobile nodes can move arbitrarily without any centralised management mechanism. The topology of these networks can be very dynamic due to the mobility of mobile nodes. Under such changeable network topology, multicasting ...
Performance analysis of AODV and DSR routing protocols for ad-hoc networks
ADCONS'11: Proceedings of the 2011 international conference on Advanced Computing, Networking and SecurityMobile Ad-hoc Networks are a collection of two or more devices equipped with wireless communications and multi-hop networking capability. We compare the performance of two prominent on demand routing protocols for mobile ad hoc networks--Dynamic Source ...
Performance Evaluation of Hybrid Routing Protocols in Mobile Ad Hoc Networks
ACCT '12: Proceedings of the 2012 Second International Conference on Advanced Computing & Communication TechnologiesMobile ad hoc network is a collection of wireless mobile nodes that creates a dynamically wireless network among them without using any fixed infrastructure. Nodes are mobile and free to move, independent of each other which makes routing much ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sponsors
- Ministry of Education, Taiwan
- Inst. of Inf. Science, Academia Sinica, Taiwan, ROC: Institute of Information Science, Academia Sinica, Taiwan, ROC
- National Science Council, Taiwan
- Center for Information and Electronic Technologies, NTU: Center for Information and Electronic Technologies, NTU
- Graduate Inst. of Communication Eng., NTU: Graduate Institute of Communication Engineering, NTU
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 02 October 2005
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 31 Dec 2024
Other Metrics
Citations
Cited By
View all- Ghassemi FFokkink W(2016)Model checking mobile ad hoc networksFormal Methods in System Design10.1007/s10703-016-0254-749:3(159-189)Online publication date: 1-Dec-2016