Abstract
The Stop-and-Wait protocol (SWP) has two (unbounded) parameters: the maximum sequence number (MaxSeqNo) and the maximum number of retransmissions (MaxRetrans). This paper presents an algebraic method for analysis of the SWP for all possible values of these parameters. Model checking such a system requires considering an infinite family of models, one for each combination of parameter values, and thus an infinite family of state spaces (reachability graphs). These reachability graphs are represented symbolically by a set of algebraic formulas in MaxSeqNo and MaxRetrans. This result is significant as it provides a complete characterisation of the infinite set of reachability graphs of our SWP model in both parameters, allowing properties to be verified for the infinite class. Verification of a number of properties is described.
Partially supported by an Australian Research Council (ARC) Discovery Grant, DP0559927, and a University of South Australia Divisional Small Grant, SP04.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Aziz Abdulla, P., Collomb-Annichini, A., Bouajjani, A., Jonsson, B.: Using Forward Reachability Analysis for Verification of Lossy Channel Systems. Formal Methods in System Design 25(1), 39–65 (2004)
Billington, J.: Formal specification of protocols: Protocol Engineering. In: Encyclopedia of Microcomputers, vol. 7, pp. 299–314. Marcel Dekker, New York (1991)
Billington, J., Díaz, M., Rozenberg, G. (eds.): APN 1999. LNCS, vol. 1605. Springer, Heidelberg (1999)
Billington, J., Gallasch, G.E.: How Stop and Wait Protocols Can Fail Over The Internet. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, pp. 209–223. Springer, Heidelberg (2003)
Billington, J., Gallasch, G.E.: An Investigation of the Properties of Stopand- Wait Protocols over Channels which can Re-order messages. Technical Report CSEC-15, Computer Systems Engineering Centre Report Series, University of South Australia (May 2004)
Billington, J., Gallasch, G.E., Han, B.: A Coloured Petri Net Approach to Protocol Verification. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 210–290. Springer, Heidelberg (2004)
Billington, J., Gallasch, G.E., Petrucci, L.: FAST Verification of the Class of Stop-and-Wait Protocols modelled by Coloured Petri Nets. Nordic Journal of Computing 12(3), 251–274 (2005)
Billington, J., Gallasch, G.E., Petrucci, L.: Transforming Coloured Petri Nets to Counter Systems for Parametric Verification: A Stop-and-Wait Protocol Case Study. In: Proceedings of 2nd International Workshop on Model-Based Methodologies for Pervasive and Embedded Software (MOMPES 2005), Rennes, France, vol. 39, May 2005, pp. 37–55. TUCS General Publication (May 2005)
FAST - Fast Acceleration of Symbolic Transition systems, http://www.lsv.ens-cachan.fr/fast/
Gallasch, G.E., Billington, J.: Towards the Parametric Verification of the Class of Stop-and-Wait Protocols over Ordered Channels. Technical Report CSEC-21, Computer Systems Engineering Centre Report Series, University of South Australia, March 2005 (revised June 2005)
Gallasch, G.E., Billington, J.: Parametric Verification of the Class of Stop-and- Wait Protocols over Ordered Channels. Technical Report CSEC-23, Computer Systems Engineering Centre Report Series, University of South Australia, Draft (January 2006)
Gallasch, G.E., Billington, J.: Using Parametric Automata for the Verification of the Stop-and-Wait Class of Protocols. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 457–473. Springer, Heidelberg (2005)
Han, B.: Formal Specification of the TCP Service and Verification of TCP Connection Management. PhD thesis, Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, Adelaide, Australia (December 2004)
Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, 2nd edn. Basic Concepts, vol. 1. Springer, Heidelberg (1997)
Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Practical Use, vol. 3. Springer, Heidelberg (1997)
Kristensen, L.M., Christensen, S., Jensen, K.: The Practitioner’s Guide to Coloured Petri Nets. International Journal on Software Tools for Technology Transfer 2(2), 98–132 (1998)
Kristensen, L.M., Westergaard, M., Nørgaard, P.C.: Model-Based Prototyping of an Interoperability Protocol for Mobile Ad-Hoc Networks. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 266–286. Springer, Heidelberg (2005)
Liu, L., Billington, J.: Tackling the Infinite State Space of a Multimedia Control Protocol Service Specification. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 273–293. Springer, Heidelberg (2002)
Postel, J.: Transmission Control Protocol. RFC 793 (September 1981)
Stallings, W.: Data and Computer Communications, 7th edn. Prentice-Hall, Englewood Cliffs (2004)
Standard ML of New Jersey, http://cm.bell-labs.com/cm/cs/what/smlnj/
Tanenbaum, A.: Computer Networks, 4th edn. Prentice-Hall, Englewood Cliffs (2003)
Valmari, A.: The State Explosion Problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)
Valmari, A., Kokkarinen, I.: Unbounded Verification Results by Finite-State Compositional Techniques: 10 any States and Beyond. In: Proceedings of International Conference on Application of Concurrency to System Design, March 1998, pp. 75–85. IEEE Computer Society, Los Alamitos (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gallasch, G.E., Billington, J. (2006). A Parametric State Space for the Analysis of the Infinite Class of Stop-and-Wait Protocols. In: Valmari, A. (eds) Model Checking Software. SPIN 2006. Lecture Notes in Computer Science, vol 3925. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691617_12
Download citation
DOI: https://doi.org/10.1007/11691617_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33102-5
Online ISBN: 978-3-540-33103-2
eBook Packages: Computer ScienceComputer Science (R0)