In this paper we presents a formal analysis of the start-up algorithm
of the DACAPO protocol. The protocol uses TDMA (Time Division Multiple
Access) bus arbitration. It is checked that a system of four
communicating stations becomes synchronized and operational within a
bounded time from an arbitrary initial state. The system model
included a clock drift corresponding to $\pm$10$^{-3}$. The protocol
is modeled as a network of timed automata, and analysis is performed
using the symbolic model-checking tool \uppaal.