# 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.

## Key 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.