In: Valmari (Ed.) , Springer-Verlag: LNCS, Vol 3925: Model Checking Software, pages 201-218. 2006.
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 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.
Keywords: Stop and Wait Protocols: Infinite Families of Systems: Parametric Reachability Graphs: Coloured Petri Nets.