Title :
Formal verification of a TDMA protocol start-up mechanism
Author :
Lönn, Henrik ; Pettersson, Paul
Author_Institution :
Dept. of Comput. Sci., Chalmers Univ. of Technol., Goteborg, Sweden
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 :
access protocols; fault tolerant computing; formal verification; synchronisation; time division multiple access; DACAPO protocol; TDMA protocol start-up mechanism; clock drift; communicating stations; ensemble; formal verification; symbolic model checker UPPAAL; system model; time division multiple access bus arbitration; timed automata; Access protocols; Automata; Broadcasting; Clocks; Computer architecture; Computer networks; Formal verification; Real time systems; Synchronization; Time division multiple access;
Conference_Titel :
Fault-Tolerant Systems, 1997. Proceedings., Pacific Rim International Symposium on
Conference_Location :
Taipei
Print_ISBN :
0-8186-8212-4
DOI :
10.1109/PRFTS.1997.640153
