Verification of Directed Acyclic Ad Hoc Networks

Abstract : We study decision problems for parameterized verification of a formal model of ad hoc networks. We consider a model in which the network is composed of a set of processes connected to each other through a directed acyclic graph. Vertices of the graph represent states of individual processes. Adjacent vertices represent single-hop neighbors. The processes are finite-state machines with local and synchronized broadcast transitions. Reception of a broadcast is restricted to the immediate neighbors of the sender process. The underlying connectivity graph constrains communication pattern to only one direction. This allows to model typical communication patterns where data is propagated from a set of central nodes to the rest of the network, or alternatively collected in the other direction. For this model, we consider decidability of the control state reachability (coverability) problem, defined over two classes of architectures, namely the class of all acyclic networks (for which we show undecidability) and that of acyclic networks with a bounded depth (for which we show decidability). The decision problems are parameterized both by the size and by the topology of the underlying network.
Complete list of metadatas

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-01515235
Contributor : Hal Ifip <>
Submitted on : Thursday, April 27, 2017 - 10:46:41 AM
Last modification on : Thursday, April 27, 2017 - 2:43:59 PM
Long-term archiving on : Friday, July 28, 2017 - 12:39:50 PM

File

978-3-642-38592-6_14_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Parosh Abdulla, Mohamed Atig, Othmane Rezine. Verification of Directed Acyclic Ad Hoc Networks. 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2013, Florence, Italy. pp.193-208, ⟨10.1007/978-3-642-38592-6_14⟩. ⟨hal-01515235⟩

Share

Metrics

Record views

241

Files downloads

168