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:

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.

• Model file (BOFF=3)
• Model file (BOFF=4)
• Property 1 file
• Property 2 file

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:

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.

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.

• Model file
• Property qp file
• Property to file