Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Barrett, W.A., Bates, R.M., Gustafson, D.A., Couch, J.D.: Compiler Construction: Theory and Practice. 2nd edn. Science Research Associates (1986)
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., 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)
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)
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)
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)
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)
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)
Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. 2nd edn. Addison-Wesley, Reading (2001)
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)
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)
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)
Sabnani, K.: An Algorithmic Technique for Protocol Verification. IEEE Transactions on Communications 36(8), 924–931 (1988)
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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gallasch, G.E., Billington, J. (2008). Parametric Language Analysis of the Class of Stop-and-Wait Protocols. In: van Hee, K.M., Valk, R. (eds) Applications and Theory of Petri Nets. PETRI NETS 2008. Lecture Notes in Computer Science, vol 5062. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68746-7_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-68746-7_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68745-0
Online ISBN: 978-3-540-68746-7
eBook Packages: Computer ScienceComputer Science (R0)