Statistical Model Checking of a Clock Synchronization Protocol for Sensor Networks

Abstract : This paper uses the statistical model checking tool in the UPPAAL toolset to test the robustness of a distributed clock synchronization algorithm for wireless sensor networks (WSN), in the case of lossy communication, i.e., when the WSN is deployed in an environment with significant multi-path propagation, leading to interference. More precisely, the robustness of the gMAC protocol included in the Chess WSN platform is tested on two important classes of regular network topologies: cliques (networks with full connectivity) and small grids (where all nodes have the same degree). The paper extends previous work by Hedaraian et al. that only analyzed this algorithm in the ideal case of non-lossy communication, and only in the case of cliques and line topologies. The main contribution is to show that the original clock synchronization algorithm is not robust to changing the quality of communication between sensors. More precisely, with high probability the algorithm fails to synchronize the nodes when considering lossy communication over cliques of arbitrary size, as well as over small grid topologies.
Type de document :
Communication dans un congrès
Farhad Arbab; Marjan Sirjani. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. Springer Berlin Heidelberg, Lecture Notes in Computer Science, LNCS-8161, pp.168-182, 2013, Fundamentals of Software Engineering. 〈10.1007/978-3-642-40213-5_11〉
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01514659
Contributeur : Hal Ifip <>
Soumis le : mercredi 26 avril 2017 - 15:21:58
Dernière modification le : mercredi 26 avril 2017 - 15:26:39
Document(s) archivé(s) le : jeudi 27 juillet 2017 - 12:55:00

Fichier

978-3-642-40213-5_11_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Luca Battisti, Damiano Macedonio, Massimo Merro. Statistical Model Checking of a Clock Synchronization Protocol for Sensor Networks. Farhad Arbab; Marjan Sirjani. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. Springer Berlin Heidelberg, Lecture Notes in Computer Science, LNCS-8161, pp.168-182, 2013, Fundamentals of Software Engineering. 〈10.1007/978-3-642-40213-5_11〉. 〈hal-01514659〉

Partager

Métriques

Consultations de la notice

26

Téléchargements de fichiers

30