|
Published Articles >> Table of Contents >> Abstract
Fourth International Conference on Network Protocols (ICNP'96)
p. 208
Protocol Specification Using Parameterized Communicating Extended Finite Stte Machines - A Case Study of The ATM ABR Rate Control Scheme
David Lee, Bell Laboratories
K. K. Ramakrishnan, AT&T Research
W. Melody Moh, San Jose State University
Udaya Shankar, University of Maryland
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICNP.1996.564943
Send link to a friend
| Abstract |
|
Formal specification is indispensable for computer-aided verification and testing of communication protocols. However, a large number of the practical protocols, including ATM, only has informal specifications, mostly in English, from which there are no general procedures to derive formal specifications.As a case study, we consider an important ATM protocol - the Available Bit Rate (ABR). The ABR source/destination policies have been specified using an 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 insight to the derivation of the formal specification. Furthermore, we introduce a scheduler to meet the minimal requirements from the source and destination protocols, that is involved in transmitting queued cells at the allowed cell rate for the source. We present the transitions for the source/destination/scheduler machines, primarily for transmitting cells in-rate.
|
 Additional Information
|
Index Terms- protocol, formal specification, extended finite state machine, ATM, ABR, source, destination, scheduler
Citation:
David Lee, K. K. Ramakrishnan, W. Melody Moh, Udaya Shankar,
"Protocol Specification Using Parameterized Communicating Extended Finite Stte Machines - A Case Study of The ATM ABR Rate Control Scheme,"
icnp,
p. 208,
Fourth International Conference on Network Protocols (ICNP'96),
1996
|
|
