Data link layer protocol correctness in FDDI networks

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