For the most recent entries see the Petri Nets Newsletter.

A Parametric State Space for the Analysis of the Infinite Class of Stop-and-Wait Protocols.

Gallasch, Guy; Billington, Jonathan

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.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography