Formal verification of a TDMA protocol start-up mechanism

Abstract

This paper presents a formal verification of the start-up algorithm of the DACAPO protocol. The protocol uses TDMA (Time Division Multiple Access) bus arbitration. It was verified that an ensemble 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 ±10 -3 . The protocol was modeled using a network of timed automata, and verification was performed using the symbolic model checker UPPAAL. 1. Introduction Distributed real-time systems are increasingly used in embedded applications, many of them safety-critical systems, such as cars, aircraft and industrial robots. The computer architecture of such systems must meet several stringent requirements in terms of cost, reliability, testability, etc., and has therefore recently been the object of much research. One crucial component of the distributed architecture is the communication system. This is the backbone of...