Verification of Ad Hoc Networks with Node and Communication Failures - Formal Techniques for Distributed Systems
Conference Papers Year : 2012

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.
Fichier principal
Vignette du fichier
978-3-642-30793-5_15_Chapter.pdf (218.57 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-00909367 , version 1 (29-05-2017)

Licence

Identifiers

  • HAL Id : hal-00909367 , version 1

Cite

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⟩
315 View
67 Download

Share

More