Model Checking Techniques for State Space Reduction in MANET Protocol Verification
| Autor: | Yuta Nagashima, Tatsuhiro Tsuchiya, Hideharu Kojima |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Delay-tolerant networking
Routing protocol Dynamic Source Routing Computer science Wireless ad hoc network Distributed computing Wireless Routing Protocol 02 engineering and technology Network topology Ad hoc On-Demand Distance Vector Routing 0202 electrical engineering electronic engineering information engineering Destination-Sequenced Distance Vector routing Vehicular ad hoc network Adaptive quality of service multi-hop routing business.industry ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS 020206 networking & telecommunications Mobile ad hoc network Ad hoc wireless distribution service Optimized Link State Routing Protocol Link-state routing protocol Geocast 020201 artificial intelligence & image processing Communications protocol business Computer network |
| Zdroj: | IPDPS Workshops |
| DOI: | 10.1109/ipdpsw.2016.122 |
| Popis: | A Mobile Ad hoc Network (MANET) is a network that consists of mobilenodes and is autonomously managed without infrastructure base stationssuch as access points. MANETs have started being used as part of safetycritical applications. A Vehicular Ad hoc Network (VANET) used inautomated driving systems is such an example. In such applications, defects in the network protocol may cause serious social problems. Model checking, a state search-based verification technique, has provento be effective in finding faults in complex system designs, such ascommunication protocols. However it is challenging to apply thistechnique to MANET protocols, because a MANET can have a number ofdifferent network topologies, thus resulting in the state explosionproblem very easily. In this paper we propose a modeling technique tomitigate this problem using the AODV protocol as a running example. MANET protocols, such as AODV, typically enforce a source node thatwishes to establish a route to the destination to retry the routeestablishing process some fixed number of times in face of failures. Weshow that to model check the protocol's behavior in these retries itsuffices to consider only the last trial. The results of preliminaryexperiments using the SPIN model checker show that using the proposedtechnique significantly reduced the time and memory used in model checking. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|