Protocol specification using parameterized communicating extended finite state machines - A case study of the ATM ABR rate control scheme

Formal specifications are indispensable for computer-aided verification and resting of communication protocols However, a large number of the practical protocols, including ATM, have only informal specifications, mostly in English. There are no general procedures to derive formal specifications from such informal specifications. As a case study, we consider an important protocol specification - ATM's Available Bit Rate (ABR) service specification. The ABR source/destination policies have been specified using mt English description in the main body of the ATM Forum's draft Traffic Management specification from which it is hard to conduct a formal analysis. Furthermore, while considerable energy has been spent in providing a reasonably precise specification, while allowing for appropriate implementation latitude an English description still has the potential for different interpretations. We model the protocol by parameterized communicating extended finite state machines with timers, which is often called a transitions system, and present a formal specification by transitions of the system We also provide insights gained in the derivation of the formal specification Furthermore, we introduce a scheduler involved in transmitting queued cells at the allowed cell rare to meet the minimal requirements from the source and destination protocols. We present the transitions for the source/destination/scheduler machines, primarily for transmitting cells in-rate.