Formal verification of a TDMA protocol start-up mechanism
- 22 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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.Keywords
This publication has 5 references indexed in Scilit:
- Automata for modeling real-time systemsPublished by Springer Nature ,2005
- DACAPO: a distributed computer architecture for safety-critical control applicationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Synchronisation in safety-critical distributed control systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Verification of an Audio Protocol with bus collision using UppaalPublished by Springer Nature ,1996
- TTP-a protocol for fault-tolerant real-time systemsComputer, 1994