Abstract

This major report specifies and verifies the ATM Available Bit Rate (ABR) control protocol using a standard network specification language, Estelle. This verification is based on the English description of ABR protocol in the ATM Traffic Management Specification Version 4.0, and the published PEFSM model of ABR protocol. The Estelle simulation model that we used to verify the ATM ABR protocol consists of two identical module instances of network station module. Connections between the two station nodes make a closed-loop feedback control system. We have defined Estelle observers to observe the behavior of the ABR protocol. Seven test cases have been designed and carried out. The results of all these test cases have shown that the protocol meets the functional specification for ABR protocol outlined in the ATM Traffic Management Specification.