Ad hoc routing protocol validation
We explore and evaluate methods for validation of ad hoc routing protocols which are used to set up forwarding paths in spontaneous networks of mobile devices. The focus is automatic formal verification but we also make an initial account of a protocol performance comparison using structured live te...
| Main Author: | |
|---|---|
| Format: | Others |
| Language: | English |
| Published: |
Uppsala universitet, Avdelningen för datorteknik
2005
|
| Subjects: | |
| Online Access: | http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-86360 |
| Summary: | We explore and evaluate methods for validation of ad hoc routing protocols which are used to set up forwarding paths in spontaneous networks of mobile devices. The focus is automatic formal verification but we also make an initial account of a protocol performance comparison using structured live testing. State explosion is a major problem in algorithmic verification of systems with concurrently executing components. We comment on some of the best reduction methods and their applicability to our work. For reactively operating ad hoc routing protocols we provide a broadcast abstraction which enables us to prove correct operation of the Lightweight Underlay Network Ad hoc Routing protocol (LUNAR) in scenarios of realistic size. Our live testing effort has thus far uncovered significant problems in the inter-operation between TCP and ad hoc routing protocols. Severe performance degradation results in networks of just a few nodes when very little mobility is introduced. This indicates that verification for smaller network sizes is also interesting since those configurations may be the only useful ones for certain types of applications. |
|---|