Parametric Language Analysis of the Class of Stop-and-Wait Protocols
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.
KeywordsTransmission Control Protocol Algebraic Expression Finite State Automaton Reachability Graph Service Language
Unable to display preview. Download preview PDF.
- 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.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.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.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
- 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.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
- 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