Modelling Clock Synchronization in the Chess gMAC WSN Protocol

TL;DR

This paper models the clock synchronization algorithm of the Chess gMAC wireless sensor network protocol using timed automata and Uppaal, revealing potential issues with long-term synchronization stability.

Contribution

It provides a detailed formal model of the protocol and analyzes its stability, highlighting scenarios where synchronization may fail over time.

Findings

Static networks can become unsynchronized over time.

The current algorithm may fail even with minimal clock drifts.

Formal verification uncovers potential long-term synchronization issues.

Abstract

We present a detailled timed automata model of the clock synchronization algorithm that is currently being used in a wireless sensor network (WSN) that has been developed by the Dutch company Chess. Using the Uppaal model checker, we establish that in certain cases a static, fully synchronized network may eventually become unsynchronized if the current algorithm is used, even in a setting with infinitesimal clock drifts.