In: Antti Valmari (Eds.): Lecture Notes in Computer Science, 3925: Model Checking Software: 13th International SPIN Workshop, Vienna, Austria, March 30 - April 1, 2006., pages 201-218. Springer-Verlag, January 2006. URL: http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/1169161712,.
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.
Keywords: Stop and Wait Protocols, Infinite Families of Systems, Parametric Reachability Graphs, Coloured Petri Nets..