Modeling and efficient verification of wireless ad hoc networks
From MaRDI portal
Abstract: Wireless ad hoc networks, in particular mobile ad hoc networks (MANETs), are growing very fast as they make communication easier and more available. However, their protocols tend to be difficult to design due to topology dependent behavior of wireless communication, and their distributed and adaptive operations to topology dynamism. Therefore, it is desirable to have them modeled and verified using formal methods. In this paper, we present an actor-based modeling language with the aim to model MANETs. We address main challenges of modeling wireless ad hoc networks such as local broadcast, underlying topology, and its changes, and discuss how they can be efficiently modeled at the semantic level to make their verification amenable. The new framework abstracts the data link layer services by providing asynchronous (local) broadcast and unicast communication, while message delivery is in order and is guaranteed for connected receivers. We illustrate the applicability of our framework through two routing protocols, namely flooding and AODVv2-11, and show how efficiently their state spaces can be reduced by the proposed techniques. Furthermore, we demonstrate a loop formation scenario in AODV, found by our analysis tool.
Recommendations
Cites work
- scientific article; zbMATH DE number 1487862 (Why is no real title available?)
- scientific article; zbMATH DE number 2182600 (Why is no real title available?)
- scientific article; zbMATH DE number 1903348 (Why is no real title available?)
- scientific article; zbMATH DE number 1390069 (Why is no real title available?)
- A Calculus for Mobile Ad Hoc Networks
- A calculus for mobile ad-hoc networks with static location binding
- A framework for security analysis of mobile wireless networks
- A process algebra for wireless mesh networks
- A process calculus for mobile ad hoc networks
- Actor-based slicing techniques for efficient reduction of Rebeca models
- An observational theory for mobile ad hoc networks (full version)
- Branching time and abstraction in bisimulation semantics
- Broadcast psi-calculi with an application to wireless protocols
- Delta modeling and model checking of product families
- Efficient on-the-fly model-checking for regular alternation-free \(\mu\)-calculus
- Formal Techniques for Networked and Distributed Systems - FORTE 2005
- Formal Techniques for Networked and Distributed Systems – FORTE 2004
- Formal verification of standards for distance vector routing protocols
- Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols
- Higher-order psi-calculi
- Model checking MANETs with arbitrary mobility
- Modelling and verifying the AODV routing protocol
- On the Verification of Timed Ad Hoc Networks
- On the complexity of parameterized reachability in reconfigurable broadcast networks
- On the power of cliques in the parameterized verification of ad hoc networks
- Symbolic Counter Abstraction for Concurrent Software
- Symmetry and partial order reduction techniques in model checking Rebeca
- The abstract MAC layer
- Tools and algorithms for the construction and analysis of systems. 21st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11--18, 2015. Proceedings
- Towards a calculus for wireless systems
- Verification of mobile ad hoc networks: an algebraic approach
Cited in
(13)- On the Verification of Timed Ad Hoc Networks
- Formal Techniques for Networked and Distributed Systems - FORTE 2005
- Automated Generation of Performance and Dependability Models for the Assessment of Wireless Sensor Networks
- Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude
- Model checking mobile ad hoc networks
- Parameterized verification of time-sensitive models of ad hoc network protocols
- Modeling and analyzing mobile ad hoc networks in Real-Time Maude
- Modeling Routing Protocols in Adhoc Networks
- A framework for mobile ad hoc networks in Real-Time Maude
- Formal analysis of leader election in MANETs using Real-Time Maude
- Actor-based model checking for software-defined networks
- Modeling and verifying ad hoc routing protocols
- scientific article; zbMATH DE number 1982205 (Why is no real title available?)
This page was built for publication: Modeling and efficient verification of wireless ad hoc networks
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1688557)
