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

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.