Data link layer protocol correctness in FDDI networks

Author

Alvarez, A.M. ; Qureshi, Z.H. ; Teck, Er Chuan

Author_Institution

Sch. of Electr. & Electron. Eng., Nanyang Technol. Univ., Singapore

fYear

1995

fDate

3-7 Jul 1995

Firstpage

304

Lastpage

308

Abstract

This paper is concerned with the application of formal methods for the specification and verification of the data link layer protocol in FDDI networks. The formal specification language PROMELA is used to formally specify the FDDI MAC protocol. Validation is done by using a simulator and validator tool called SPIN. The validation of FDDI MAC protocol is done in a few stages. The strategy used is to build an FDDI MAC validation model with two stations communicating with each other on the FDDI ring, and the safety and liveness properties. The incremental composition method is used as the complexity management technique for the validation of the FDDI MAC protocol. The process of increasing the complexity of the validation model reveals the problems and limitations of automated validation using reachability analysis

Keywords

FDDI; access protocols; computer network management; digital simulation; formal specification; formal verification; network topology; reachability analysis; simulation; software tools; token networks; FDDI MAC protocol; FDDI MAC validation model; FDDI networks; FDDI ring; PROMELA; SPIN; automated validation; complexity management technique; data link layer protocol; formal methods; formal specification language; incremental composition method; protocol specification; protocol verification; reachability analysis; simulator; token ring architecture; validator tool; Computer languages; Concurrent computing; FDDI; Formal specifications; Intelligent networks; Media Access Protocol; Reachability analysis; Safety; Testing; Vocabulary;

fLanguage

English

Publisher

ieee

Conference_Titel

Networks, 1995. Theme: Electrotechnology 2000: Communications and Networks. [in conjunction with the] International Conference on Information Engineering., Proceedings of IEEE Singapore International

Print_ISBN

0-7803-2579-6

Type

conf

DOI

10.1109/SICON.1995.526067

Filename

526067