Abstract
Numerous specialized ad hoc routing protocols are currently proposed for use, or being implemented. Few of them have been subjected to formal verification. This paper evaluates two model checking tools, SPIN and UPPAAL, using the verification of the Lightweight Underlay Network Ad hoc Routing protocol (LUNAR) as a case study. Insights are reported in terms of identifying important modeling considerations and the types of ad hoc protocol properties that can realistically be verified.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-3-540-30232-2_24
Chapter PDF
Similar content being viewed by others
References
Barnat, J., Brim, L., Stribrna, J.: Distributed LTL model-checking in SPIN. Technical report, Masaryk University (December 2000)
Behrmann, G., Hune, T., Vaandrager, F.: Distributed timed model checking - how the search order matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)
Chiyangwa, S., Kwiatkowska, M.: Analysing timed properties of AODV with UPPAAL. Technical report, University of Birmingham, Technical Report CSR-04-4 (March 2004)
Clausen, T., Jacquet, P.: Request for Comments: Optimized link state routing protocol (OLSR) (October 2003), http://www.ietf.org/rfc/rfc3626.txt
Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Formal Methods in Computer-Aided Design, November 2002, Springer, Heidelberg (2002)
Engler, D., Musuvathi, M.: Static analysis versus software model checking for bug finding. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 191–210. Springer, Heidelberg (2004)
Holzmann, G.J.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)
Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Proc. FORTE Conference (1994)
IETF MANET Working Group. MANET charter (2004), http://www.ietf.org/html.charters/manet-charter.html
Information Sciences Institute. The network simulator – ns-2 home page (2004), http://www.isi.edu/nsnam/ns
Johnson, D.B.: Routing in ad hoc networks of mobile hosts. In: Proc. IEEE Workshop on Mobile Computing Systems and Applications, December 1994, pp. 158–163 (1994)
Johnson, D.B., Maltz, D.A., Hu, Y.-C.: Internet draft: The dynamic source routing protocol for mobile ad hoc networks (DSR) (April 2003), http://www.ietf.org/internet-drafts/draft-ietf-manet-dsr-09.txt
Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Proc. Second Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification, July 2002, pp. 169–187 (2002)
Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: Compact data structures and state-space reduction. In: Proc. 18th IEEE Real-Time Systems Symposium (RTSS), December 1997, pp. 14–24 (1997)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer 1(1–2), 134–152 (1997)
Lundgren, H.: Implementation and Real-world Evaluation of Routing Protocols for Wireless Ad hoc Networks. Licentiate thesis, Uppsala University (2002)
Lundgren, H., Lundberg, D., Nielsen, J., Nordström, E., Tschudin, C.: A large-scale testbed for reproducible ad hoc protocol evaluations. In: Proc. 3rd annual IEEE Wireless Communications and Networking Conference (WCNC), March 2002, pp. 412–418. IEEE, Los Alamitos (2002)
Obradovic, D.: Formal Analysis of Routing Protocols. Phd thesis, University of Pennsylvania (2002)
Ogier, R., Templin, F., Lewis, M.: Internet draft: Topology dissemination based on reverse-path forwarding (TBRPF) (October 2003), http://www.ietf.org/internet-drafts/draft-ietf-manet-tbrpf-11.txt
Perkins, C., Belding-Royer, E., Das, S.: Request for Comments: Ad hoc ondemand distance vector (AODV) routing (July 2003), http://www.ietf.org/rfc/rfc3561.txt
Perkins, C.E., Royer, E.M.: Ad hoc on-demand distance vector routing. In: Proc. 2nd IEEE Workshop on Mobile Computing Systems and Applications, February 1999, pp. 90–100 (1999)
Ruys, T.C.: Towards Effective Model Checking. Phd thesis, University of Twente (March 2001)
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)
University of Cambridge Computer Laboratory. Automated reasoning group HOL page (2004), http://www.cl.cam.ac.uk/Research/HVG/HOL/
Uppsala University and Aalborg University. UPPAAL home page (2004), http://www.uppaal.com
Verinet group. Verinet home page (2004), http://www.cis.upenn.edu/verinet
Oskar Wibling. LUNAR pseudo code description (2004), http://user.it.uu.se/oskarw/lunar_pseudo_code/
Wikipedia. Ad hoc protocol list (2004), http://en.wikipedia.org/wiki/Ad_hoc_protocol_list
Xiong, C., Murata, T., Tsai, J.: Modelling and simulation of routing protocol for mobile ad hoc networks using coloured Petri nets. In: Proc. Workshop on Formal Methods Applied to Defence Systems in Formal Methods in Software Engineering and Defence Systems (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 IFIP International Federation for Information Processing
About this paper
Cite this paper
Wibling, O., Parrow, J., Pears, A. (2004). Automatized Verification of Ad Hoc Routing Protocols. In: de Frutos-Escrig, D., Núñez, M. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2004. FORTE 2004. Lecture Notes in Computer Science, vol 3235. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30232-2_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-30232-2_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23252-0
Online ISBN: 978-3-540-30232-2
eBook Packages: Springer Book Archive