`PASS`

Case Studies

## Wireless LAN

The IEEE 802.11 Wireless LAN protocol uses a randomized algorithm to
avoid collisions on the transmission channel. Further, the wireless
medium loses messages with a certain probability. The considered
model is parameterized with an *exponential* back-off counter
limit *BOFF* and a maximal package send time of T *mu s*.
We checked the property: "The maximum probability that either
station's back-off counter reaches *k*" for *k=3*
and *k=6*. Increasing *BOFF* from *5* to *6* leads
to an exponential increase in model size and running time
in `PRISM`

, while in `PASS 1.0`

the row is
identical for *BOFF=5* and *BOFF=6*. It was observed
in [HermannsWZ08] that states with back-off
counter higher than three can reach a goal state (via a reset),
however they do not lie on paths with maximal probability. Hence
refinement never splits blocks with respect to back-offs beyond three
which is somewhat similar to the motivating example. It also turns out
that the computed lower and upper bounds are precise (lower and upper
bound agree). The discrepancy in the number of blocks
between `PASS 1.0`

and `PASS`

is caused by more
aggressive qualitative preprocessing before the quantitative analysis.

In addition, we used `PASS`

to compute the minimal
reachability probability for reaching a backoff counter value of
6. `PASS`

computed the precise probability. Note
that `PASS 1.0`

does not support minimal reachability.

- Model file (
*BOFF=5, T=315*) - Model file (
*BOFF=6, T=315*) - Model file (
*BOFF=6, T=9500*) - Property file (
*k=3*) - Property file (
*k=6*) - Property file (minimal probability,
*k=3*)

## CSMA/CD

Similar to the WLAN protocol, the IEEE 802.3 CSMA/CD protocol is
parameterized with an *exponential* back-off counter limit
*BOFF*. We analyzed the properties:

`Property` |
`Description` |

` p1: Pmax=? [true U s1=4 &s 2=4]` |
"The maximum probability that both stations deliver" |

` p2: Pmin=? [true U bc1=5 | bc2=5]` |
"The message of any station eventually delivered before 1 backoff" |

For both properties, the abstract state space is significantly
smaller. Consider property `p2`

. Similar to the WLAN
protocol, the size of the abstraction does not change with respect to
the size of *BOFF*. However, the counterexample analysis
of `PASS 1.0`

explores a larger number of paths explored
with increasing *BOFF*. The reason is that for greater values of
*BOFF*, there is more branching in the probabilistic model, thus
in the abstraction there are more abstract paths being
explored. Refinement for probabilistic game abstraction explores one
path per refinement step. Therefore this problem does not arise.

## Bounded Retransmission Protocol

The Bounded Retransmission Protocol (BRP) protocol has two parameters:
*N* denotes the length of the file to be transmitted,
and *MAX* denotes the maximal number of retransmissions. We have
studied the following properties:

`Property` |
`Description` |

` p1: Pmax=? [F s=5 & T ]` |
"Eventually the sender does not report a successful transmission" |

` p4: Pmax=? [F srep!=0 & T & !recv]` |
"Eventually the receiver does not receive any chunk and the sender tried to send a chunk" |

As observed in [HermannsWZ08], there is
little leeway for abstraction for `p1`

if precise
probabilities are required. The modeled has to be fully reconstructed
by refinement.

However, `p4`

can be analyzed for an infinite parameter
range with `PASS 1.0`

: it is an invariant property with
respect to the file length *N*. The constraint *N>16*
allows us to verify the property for any possible file length greater
than *16*. While `PASS 1.0`

computed safe upper
bounds, we are able to compute the precise probability. We can thus
confirm that the bounds previously computed are tight indeed.

- Model file (
*N=16, MAX=3*) - Model file (
*N=32, MAX=5*) - Model file (
*N=infinite, MAX=3*) - Model file (
*N=infinite, MAX=4*) - Model file (
*N=infinite, MAX=5*) - Property 1 file
- Property 4 file

## Sliding Window

The sliding window protocol (SW) is the standard protocol with lossy
channels over an unbounded domain of sequence numbers. Due to the
sequence numbers, the model is infinite and hence there can be no
comparison to `PRISM`

.
Two properties were checked.

`Property` |
`Description` |

` gp: Pmax=? [true U sent>expected+2 ]` |
"goodput property" |

` to: Pmax=? [true U clock >= TIMEOUT]` |
"timeout" |

A goodput property which considers the difference between the number
of sent and received packages. The goal is to compute probability that
the number of sent packages exceeds the number of received packages by
a particular constant. `PASS 1.0`

established that, at
any time, the probability of the difference exceeding three is at most
three percent for windows size four. Using `PASS`

, we
computed the precise probability which is actually smaller than three
percent. The second property concerns the probability of a protocol
timeout. Here we could also compute the precise probability. The
number of blocks used by the game-based tool is significantly smaller
than those computed by `PASS 1.0`

. This is
because `PASS 1.0`

unnecessarily unrolled the value domain
of timer variable, which the novel tool did not do.