This paper describes a modelling and analysis experience concerning time synchronization in wireless sensor networks (WSN). A fully distributed algorithm is formally modelled and its properties assessed through statistical model checking. The described work is based on the THEATRE framework which rests on actors and asynchronous message passing. THEATRE can be reduced to the UPPAAL Statistical Model Checker (SMC). The paper discusses the chosen time synchronization algorithm, outlines the THEATRE modelling features and its mapping on to UPPAAL SMC, and shows a THEATRE model for the selected time synchronization algorithm enhanced with a new adaptation mechanism for energy saving. The model is then analyzed through simulations.

Time synchronization in wireless sensor networks: A modelling and analysis experience using Theatre

Libero Nigro
Membro del Collaboration Group
;
SCIAMMARELLA, PAOLO FRANCESCO
Membro del Collaboration Group
2018-01-01

Abstract

This paper describes a modelling and analysis experience concerning time synchronization in wireless sensor networks (WSN). A fully distributed algorithm is formally modelled and its properties assessed through statistical model checking. The described work is based on the THEATRE framework which rests on actors and asynchronous message passing. THEATRE can be reduced to the UPPAAL Statistical Model Checker (SMC). The paper discusses the chosen time synchronization algorithm, outlines the THEATRE modelling features and its mapping on to UPPAAL SMC, and shows a THEATRE model for the selected time synchronization algorithm enhanced with a new adaptation mechanism for energy saving. The model is then analyzed through simulations.
2018
Wireless sensor networks, time synchronization, asynchronous messages, actors, statistical model checking, UPPAAL
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11770/285358
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact