Verification of Ad Hoc Networks with Node and Communication Failures

Abstract : We investigate the impact of node and communication failures on the decidability and complexity of parametric verification of a formal model of ad hoc networks. We start by considering three possible types of node failures: intermittence, restart, and crash. Then we move to three cases of communication failures: nondeterministic message loss, message loss due to conflicting emissions, and detectable conflicts. Interestingly, we prove that the considered decision problem (reachability of a control state) is decidable for node intermittence and message loss (either nondeterministic or due to conflicts) while it turns out to be undecidable for node restart/crash, and conflict detection.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/hal-00909367
Contributor : Davide Sangiogi <>
Submitted on : Monday, May 29, 2017 - 4:00:51 PM
Last modification on : Friday, January 4, 2019 - 5:32:57 PM
Long-term archiving on : Wednesday, September 6, 2017 - 11:32:04 AM

File

978-3-642-30793-5_15_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

  • HAL Id : hal-00909367, version 1

Citation

Giorgio Delzanno, Arnaud Sangnier, Gianluigi Zavattaro. Verification of Ad Hoc Networks with Node and Communication Failures. 14th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 32nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2012, Stockholm, Sweden. pp.235-250. ⟨hal-00909367⟩

Share

Metrics

Record views

470

Files downloads

99