Parametric Language Analysis of the Class of Stop-and-Wait Protocols

  • Guy Edward Gallasch
  • Jonathan Billington
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5062)


Model checking a parametric system when one or more of its parameters is unbounded requires considering an infinite family of models. The Stop-and-Wait Protocol (SWP) has two (unbounded) parameters: the maximum sequence number and the maximum number of retransmissions. Previously, we presented a novel method for the parametric analysis of the SWP by developing algebraic formulas in the two parameters that symbolically represent the corresponding infinite class of reachability graphs. Properties were then verified directly from these expressions. This paper extends this analysis to the verification of the SWP using language equivalence. From the algebraic expressions developed previously, a parametric Finite State Automaton (FSA) representing all sequences of user-observable events (i.e. the protocol language) is derived. We then perform determinisation and minimisation directly on the parametric FSA. The result is a simple, non-parametric FSA that is isomorphic to the service language of alternating send and receive events. This result is significant as it verifies conformance of the SWP to its service for all values of the two unbounded parameters.


Transmission Control Protocol Algebraic Expression Finite State Automaton Reachability Graph Service Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Barrett, W.A., Bates, R.M., Gustafson, D.A., Couch, J.D.: Compiler Construction: Theory and Practice. 2nd edn. Science Research Associates (1986)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Billington, J., Saboo, S.: An investigation of credit-based flow control protocols. In: Proceedings of the 1st International Conference on Simulation Tools and Techniques for Communications, Networks and Systems (SIMUTools 2008), Marseille, France, 3-7 March 2008, 10 pages (2008) (CD ROM), ACM International Conference Proceedings series (to appear)Google Scholar
  4. 4.
    Gallasch, G.E.: Parametric Verification of the Class of Stop-and-Wait Protocols. PhD thesis, Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, Adelaide, Australia (May 2007)Google Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    Gallasch, G.E., Billington, J.: A Parametric State Space for the Analysis of the Infinite Class of Stop-and-Wait Protocols. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 201–218. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  7. 7.
    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 (2006)Google Scholar
  8. 8.
    Gallasch, G.E., Billington, J.: Language Analysis of the Class of Stop-and-Wait Protocols. Technical Report CSEC-31, Computer Systems Engineering Centre Report Series, University of South Australia (2008)Google Scholar
  9. 9.
    Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. 2nd edn. Addison-Wesley, Reading (2001)zbMATHGoogle Scholar
  10. 10.
    Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, Volume 1: Basic Concepts. 2nd edn. Monographs in Theoretical Computer Science. Springer, Heidelberg (1997)Google Scholar
  11. 11.
    Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems. International Journal on Software Tools for Technology Transfer 9(3-4), 213–254 (2007)CrossRefGoogle Scholar
  12. 12.
    Mohri, M.: Generic Epsilon-Removal and Input Epsilon-Normalisation Algorithms for Weighted Transducers. Internation Journal of Foundations of Computer Science 13(1), 129–143 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Sabnani, K.: An Algorithmic Technique for Protocol Verification. IEEE Transactions on Communications 36(8), 924–931 (1988)zbMATHCrossRefGoogle Scholar
  14. 14.
    Wolper, P.: Expressing Interesting Properties of Programs in Propositional Temporal Logic. In: Proceedings of the 13th Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 184–193. ACM Press, New York (1986)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Guy Edward Gallasch
    • 1
  • Jonathan Billington
    • 1
  1. 1.Computer Systems Engineering CentreUniversity of South AustraliaAustralia

Personalised recommendations