An investigation of credit-based flow control protocols

ABSTRACT

Credit-based flow control mechanisms, such as those used in the Transmission Control Protocol, allow flow control and error control procedures of data transfer protocols to operate independently. We create a Coloured Petri Net model of a class of data transfer protocols, which uses retransmissions and acknowledgements for error control and "credits" for flow control. This model is characterized by 3 parameters: the maximum sequence number, the maximum number of retransmissions and the maximum receiver buffer size. From the analysis results, we derive expressions in these parameters for the channel bounds and the number of terminal states. These expressions are verified for a range of values of the parameters.

REFERENCES

• 1: J. Billington and G. E. Gallasch. How Stop and Wait protocols Can Fail Over the Internet. In Proceedings of FORTE '03, volume 2767 of Lecture Notes in Computer Science, volume 2000, pages 209--223. Springer-Verlag, 2003.
• 2: J. Billington, G. E. Gallasch, and B. Han. A Coloured Petri Net Approach to Protocol Verication. In Lectures on Concurrency and Petri Nets, Advances in Petri Nets, volume 3098 of Lecture Notes in Computer Science, pages 210--290. Springer-Verlag, 2004.
• 3: D. Chkliaev, J. Hooman, and E. Vink. Verification and Improvement of the Sliding Window Protocol. In Tools and Algorithms for the Construction and Analysis of Systems, volume 2619 of Lecture Notes in Computer Science, pages 148--163. Springer-Verlag, 2004.
• 4: CPN Tools Online. http://www.daimi.au.dk/CPNTools/.
• 5: W. Fokkink, J. F. Groote, J. Pang, B. Badban, and J. Pol. Verifying a Sliding Window Protocol in μCRL. In Tools and Algorithms for the Construction and Analysis of Systems, volume 2619 of Lecture Notes in Computer Science, pages 113--127. Springer-Verlag, 2003.
• 6: G. E. Gallasch and J. Billington. Using Parametric Automata for the Verification of the Stop-and-Wait Class of Protocols. In Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA 2005), Taipei, Taiwan, Volume 3707 of Lecture Notes in Computer Science, pages 457--473. Springer.
• 7: G. E. Gallasch and J. Billington. A Parametric State Space for the Analysis of the Infinite Class of Stop-and-Wait Protocols. In 13th International SPIN Workshop on Model Checking of Software, volume 3925 of Lecture Notes in Computer Science. Springer, May 2006.
• 8: J. Billington, M. Diaz, and G. Rozenberg, editors. Application of Petri Nets to Communication Networks, volume 1605 of Lecture Notes in Computer Science. Springer, 1999.
• 9: Kurt Jensen, Coloured Petri nets: basic concepts, analysis methods and practical use, volume 3, Springer-Verlag New York, Inc., New York, NY, 1997
• 10: Kurt Jensen , Lars Michael Kristensen , Lisa Wells, Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems, International Journal on Software Tools for Technology Transfer (STTT), v.9 n.3, p.213-254, May 2007 [doi>10.1007/s10009-007-0038-x]
• 11: J. Postel. Transmission Control Protocol. IETF, September 1981.
• 12: Mark A. Smith , Nils Klarlund, Verification of a Sliding Window Protocol Using IOA and MONA, Proceedings of the FIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XIII) and Protocol Specification, Testing and Verification (PSTV XX), p.19-34, October 10-13, 2000
• 13: Karsten Stahl , Kai Baukus , Yassine Lakhnech , Martin Steffen, Divide, Abstract, and Model-Check, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, p.57-76, September 21-24, 1999
• 14: W. Stallings. Data and Computer Communications. Prentice Hall, 8 edition, 2007.
• 15: N. Stenning. A Data Transfer Protocol. Computer Networks 1, pages 99--110, 1976.
• 16: Andrew S. Tanenbaum, Computer Networks, Prentice Hall PTR, Upper Saddle River, NJ, 1985

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols

Additional Classification:
  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.5 Model Development

General Terms:
Experimentation, Verification

Keywords:
coloured petri nets, exhaustive simulation, flow control