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

fYear

1997

fDate

15-16 Dec 1997

Firstpage

235

Lastpage

242

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Fault-Tolerant Systems, 1997. Proceedings., Pacific Rim International Symposium on

Conference_Location

Taipei

Print_ISBN

0-8186-8212-4

Type

conf

DOI

10.1109/PRFTS.1997.640153

Filename

640153