IEEE 802.3 CSMA/CD Protocol

Introduction
Prototype Implementation of [KNSW04, KNSW07]
Probabilistic Timed Automata Model
Analysis Results
- Probabilistic reachability
- Time-bounded probabilistic reachability

Related publications: [KNSW04, KNSW07]

Introduction

This case study concerns probabilistic model checking of certain aspects of the IEEE 802.3 CSMA/CD (Carrier Sense, Multiple Access with Collision Detection) protocol. The CSMA/CD protocol is designed for networks with a single channel and specifies the behaviour of stations with the aim of minimising simultaneous use of the channel (data collision).

The basic structure of the protocol is as follows: when a station has data to send, it listens to the medium, after which, if the medium was free (no one transmitting), the station starts to send its data. On the other hand, if the medium was sensed busy, the station waits a random amount of time and then repeats this process.

This case study is used to test the feasibility of the symbolic (zone based) model checking algorithms introduced in [KNSW04, KNSW07] for checking probabilistic timed automata against PTCTL (Probabilistic Timed Computation Tree Logic) specifications. For comparison we also include the results obtained with the integer semantics approach in PRISM [KNS03b, KNPS03].

Prototype Implementation of [KNSW04, KNSW07]

We now briefly summarise our prototype implementation of the model checking algorithms of [KNSW04, KNSW07]. It is important to note that the aim of our implementation is to validate the algorithms presented for model checking probabilistic timed automata against PTCTL, rather that to devise an efficient implementation; the latter will be the subject of future work.

The main step in the implementation of our techniques is the representation of (sets of) symbolic states and the operations required on them; more precisely, since a symbolic state is a pair (l,ζ) where l is a location of the probabilistic timed automaton and ζ is a zone (polyhedron), we require a method for representing zones and performing operations on zones.

Difference Bound Matrices (DBMs) [Dil89] are a well known data-structure for the representation of convex zones and are used in the model checkers UPPAAL and KRONOS. As the operations required by our algorithm can introduce non-convexity, we must represent non-convex zones. Following the approach presented in [Tri98], we represent non-convex zones by lists of DBMs, that is, we represent a non-convex zone ζ by a list of convex zones ζ₁,...,ζ_n such that ζ= ζ₁ ∪ ... ∪ ζ_n. It thus follows that a symbolic state can be represented by a location and a list of DBMs.

This representation is clearly not canonical: there are many ways of decomposing a non-convex zone into a set of convex zones. However, [Tri98] presents algorithms for the operations we require when zones are represented as lists of DBMs. Based on [Tri98], we have implemented, in Java, a prototype DBM package and the operations on lists of DBMs required by the model checking algorithms of [KNSW04, KNSW07].

Probabilistic Timed Automata Model

The model we consider here is a probabilistic extension of the timed automata model given in [NSY92]. We consider the case when there are two stations trying to send data at the same time, and the overall model is given by the parallel composition of three probabilistic timed automata representing the medium and two stations trying to send data.

The medium:

The probabilistic timed automaton representing the medium is given below.

The medium is initially ready to accept data from any station (event send). Once a station starts sending its data there is an interval of time (at most σ), representing the time it takes for a signal to propagate between the stations, in which the medium will accept data from the other station (resulting in a collision). After this interval, if the other station tries to send data it will get the busy signal (busy). When a collision occurs, there is a delay (again at most σ) before the stations realize there has been a collision, after which the medium will become free (represented by the event cd). If the stations do not collide, then when a station finishes sending it data (event end) the medium becomes idle.

The stations

The probabilistic timed automaton representing a single station is given below. Note that, as in [NSY92] we assume that only packets of equal length are sent and we denote by λ the time to send a data packet.

A station starts by sending is data (we are modelling the case when initially the stations collide). If there is no collision, then, after λ time units, the station finishes sending its data (event end). On the other hand, if there is a collision (event cd), the station attempts to retransmit the packet where the scheduling of the retransmission is determined by a truncated binary exponential backoff process. The delay before retransmitting is an integer number of time slots (each of length slotTime). The number of slots that the station waits after the nth transmission failure is chosen as a uniformly distributed random integer in the range:

0 , 1 , 2 , ... , 2^k+1-1

where k=min(n,bcmax). Once this time has elapsed, if the medium appears free the station resends the data (event send), while if the medium is sensed busy (event busy) the station repeats this process.

Note that, to simplify the model, we have removed the limit on the number of times a station attempts to retransmit a packet as specified in the standard. For our experiments we consider the cases when bcmax is either 1 or 2.

Parameters:

The following parameters are taken from the IEEE standard 802.3 for 10 Mbps Ethernet.

Propagation delay σ=26μs.
Time to send a data packet (plus the propagation delay) λ=808μs.
Length of one time slot (used in the truncated binary exponential backoff process) slotTime=2σs.

Analysis results

We now report on the model checking results obtained using our prototype implementation for the following performance measures:

probabilistic reachability
time-bounded probabilistic reachability

Since the algorithms work via backwards reachability and the model is constructed as the parallel composition of subcomponents, the prototype tool first performs a forwards reachability step to find the set of reachable locations (taking 19.77 seconds).

Due to the size of the deadline models, all experiments concerning the digital clocks approach were performed with PRISM's MTBDD engine.

Probabilistic reachability

The following probabilistic reachability property has been verified.

"With probability 1, eventually both stations send their packet correctly."

In PTCTL this is expressed by: P_≥1[ true U done ]

Model checking times:

The algorithm MaxV_≥1 of [KNSW04, KNSW07]returns no symbolic states, which implies that the minimum probability is 1. Below we give the model checking statistics for MaxV_≥1 as we vary the parameter c.

bcmax=1

c:	time (s):	MaxV_≥1 iters:	MaxU_≥1 iters:
1	1,048	966	7,409
10	106.7	99	755
26	48.38	40	321
30	44.31	35	281
40	34.06	27	218
50	29.88	22	184
60	88.01	21	168
70	79.83	18	150
80	72.39	16	141
90	72.17	15	123
100	66.20	13	121
200	57.18	7	87
808	474.9	4	89

In contrast when using the digital clocks approach and PRISM, the model has 5,240 states, it takes 25.46 seconds to construct the model and 12.99 seconds to perform the verification.

bcmax=2

c:
c:	time (s):	MaxV_≥1 iters:	MaxU_≥1 iters:
1	2,058	1,070	7,830
10	223.1	109	800
26	126.6	44	347
30	142.4	38	303
40	109.6	29	237
50	94.77	24	201
60	213.6	22	177
70	179.3	19	157
80	149.5	16	136
90	158.3	16	130
100	115.6	14	117
200	232.6	9	93
808	21,682	5	147

In contrast when using the digital clocks approach and PRISM, the model has 17,763 states, it takes 46.22 seconds to construct the model and 21.67 seconds to perform the verification.

Time-bounded probabilistic reachability

We consider the following time-bounded probabilistic reachability property:

"the minimum/maximum probability of both stations correctly delivering their packets by the deadline D".

In PTCTL this is expressed by: z.P_~λ[ true U done & z≤D ]

Computing maximum probabilities

Maximum probabilities are computed through the algorithm MaxU (see [KNSW04, KNSW07]), where the final step requires the calculation of maximum reachability probabilities on a finite state system which we perform with PRISM.

bcmax=1

D:	MaxU			PRISM			maximum probability:
	time (s):	iters:	states:	construction time (s):	model checking
	time (s):	iters:	states:	construction time (s):	time (s):	iters:
1000	1.177	9	71	-	-	-	0.0
1200	11.70	13	191	-	-	-	0.0
1400	26.51	17	311	-	-	-	0.0
1600	55.65	21	431	-	-	-	0.0
1800	76.68	32	617	7.633	0.075	47	0.729165
2000	84.33	38	725	9.112	0.123	58	0.929361
2200	98.82	48	861	13.54	0.192	71	0.988106
2400	120.5	58	997	17.98	0.259	84	0.997999
2600	145.3	68	1,129	26.50	0.362	92	0.999663
2800	174.2	78	1,263	35.59	0.446	99	0.999941
3000	239.8	88	1,399	42.36	0.534	99	0.999988

Below are the model checking statistics for the digital clocks approach when verifying this property with PRISM.

D:	construction		model checking		maximum probability:
D:	time (s):	states:	time (s):	iters:	maximum probability:
1000	141.7	1,876,105	0.074	0	0.0
1200	243.3	2,671,305	0.099	0	0.0
1400	307.8	3,546,505	0.12	0	0.0
1600	391.8	4,501,705	0.14	0	0.0
1800	445.5	5,528,692	291.1	1,846	0.729165
2000	513.8	6,570,692	612.5	2,013	0.929361
2200	583.5	7,612,692	847.1	2,234	0.988106
2400	658.2	8,654,692	969.1	2,455	0.997999
2600	670.2	9,696,692	1,229	2,673	0.999663
2800	700.2	10,738,692	1,486	2,886	0.999941
3000	764.3	11,780,692	1,703	3,097	0.999988

bcmax=2

D:	MaxU			PRISM			maximum probability:
	time (s):	iters:	states:	construction time (s):	model checking
	time (s):	iters:	states:	construction time (s):	time (s):	iters:
1000	2.176	9	91	-	-	-	0.0
1200	178.0	11	423	-	-	-	0.0
1400	833.4	13	759	-	-	-	0.0
1600	192.6	15	1,095	-	-	-	0.0
1800	337.8	21	1,834	90.31	0.065	39	0.580428
2000	600.6	24	2,615	232.9	0.161	44	0.903011
2200	655.9	29	3,019	323.4	0.262	50	0.986651
2400	706.7	34	3,415	437.1	0.349	55	0.998157
2600	773.9	39	3,795	541.7	0.459	58	0.999743
2800	8,762	44	4,183	740.9	0.570	61	0.999961
3000	9,852	49	4,579	901.7	0.700	61	0.999990

Below are the model checking statistics for the digital clocks approach when verifying this property with PRISM.

D:	construction		model checking		maximum probability:
D:	time (s):	states:	time (s):	iters:	maximum probability:
1000	238.8	4,170,287	0.118	0	0.0
1200	331.5	5,813,169	0.152	0	0.0
1400	442.3	7,535,969	0.185	0	0.0
1600	532.8	9,338,769	0.219	0	0.0
1800	639.3	11,211,180	483.5	1,838	0.580428
2000	727.9	13,072,580	953.2	1,998	0.903011
2200	818.8	14,930,180	1,409	2,213	0.986651
2400	1,036	16,787,780	3,028	2,425	0.998157
2600	1,379	18,645,380	3,313	2,635	0.999743
2800	1,973	20,502,980	2,931	2,843	0.999961
3000	1,261	22,360,580	4,304	2,999	0.999990

Computing minimum probabilities

Minimum probabilities are computed through the algorithms MaxV_≥1 and MaxU, where the final step of the MaxU requires the calculation of maximum reachability probabilities which we again perform with PRISM.

For comparison we also consider an alternative approach for calculating minimum probabilities if deadline properties which reduces the problem to computing maximum probabilities on a modified model. More precisely, since eventually both stations send their packet correctly with probability 1, we can use the technique given in [KNS03b] and instead compute the minimum probability of satisfying the property

z.P_~λ[ true U done & z≤D ]

as 1 minus the maximum probability of satisfying the formula

P_~λ[ true U exceeded ]

on the probabilistic timed automaton after the following modifications have been performed.

-	States in which done is true are forced to make a transition to a sink-location.
-	Add a transition to a different, ``deadline exceeded'' sink-location, denoted exceeded, as soon as the value of the clock z exceeds D in all states which do not satisfy done).

bcmax=1.

We first consider the affect that the parameter c has on the performance of the MaxV_≥1 algorithm when D=2000 and D=3000.

c:	D=2000			D=3000
c:	time (s):	MaxV_≥1 iters:	MaxU_≥1 iters:	time (s):	MaxV_≥1 iters:	MaxU_≥1 iters:
1	269.6	132	1,062	274.5	132	1,062
10	31.94	15	126	33.14	15	126
26	21.60	9	94	23.85	9	94
30	27.75	9	94	28.87	9	94
40	18.20	7	78	22.14	7	78
50	18.67	6	70	19.56	6	70
60	201.2	8	91	191.8	8	91
70	199.3	8	91	217.3	8	91
80	182.4	7	84	186.1	7	84
90	179.5	7	84	198.6	7	84
100	189.3	7	84	186.5	7	84
200	83.67	6	90	96.07	6	90
808	659.5	5	115	587.8	5	115

We now give the overall model checking time of our implementation in the case the parameter c of the algorithm MaxV_≥1 is set equal to 50.

D:	MaxV_≥1		MaxU			PRISM			minimum probability:
	time (s):	iters:	time (s):	iters:	states:	construction time (s):	model checking
	time (s):	iters:	time (s):	iters:	states:	construction time (s):	time (s):	iters:
1000	15.61	70	25.35	23	351	2.072	0.021	-	0.0
1200	15.71	70	25.58	23	351	1.842	0.021	-	0.0
1400	16.04	70	25.94	23	351	1.834	0.02	-	0.0
1600	15.92	70	25.72	23	351	1.836	0.021	-	0.0
1800	15.69	70	29.96	27	441	2.992	0.057	42	0.583332
2000	18.67	70	38.85	37	591	6.454	0.073	52	0.869791
2200	15.64	70	54.03	46	783	11.63	0.098	65	0.966390
2400	15.59	70	82.11	53	975	18.69	0.134	75	0.991279
2600	15.58	70	118.1	61	1,143	29.08	0.153	86	0.997256
2800	15.63	70	172.5	68	1,335	40.12	0.206	98	0.999298
3000	19.56	70	258.7	77	1,527	53.69	0.228	108	0.999819

Next we give model checking statistics for the approach for computing the maximum probability of satisfying P_~λ[ true U exceeded ] on the modified automaton.

D:	MaxU			PRISM			maximum probability:
	time (s):	iters:	states:	construction time (s):	model checking
	time (s):	iters:	states:	construction time (s):	time (s):	iters:
1000	11.44	29	362	2.843	0.065	-	1
1200	11.49	29	362	2.704	0.039	-	1
1400	11.48	29	362	2.682	0.044	-	1
1600	11.46	29	362	2.675	0.038	-	1
1800	14.76	33	440	4.147	0.097	42	0.416668
2000	20.08	43	562	8.234	0.127	52	0.130209
2200	37.24	52	722	13.28	0.184	65	0.033610
2400	75.31	59	882	20.04	0.177	75	0.008720
2600	103.0	67	1,022	27.09	0.205	86	0.002744
2800	182.7	74	1,182	41.27	0.241	98	7.012e-4
3000	261.2	83	1,342	53.06	0.281	108	1.799e-4

Below are the model checking statistics for the digital clocks approach.

D:	construction		model checking		minimum probability:
D:	time (s):	states:	time (s):	iters:	minimum probability:
1000	141.7	1,876,105	0.269	0	0.0
1200	243.3	2,671,305	0.321	0	0.0
1400	307.8	3,546,505	0.441	0	0.0
1600	391.8	4,501,705	0.473	0	0.0
1800	445.5	5,528,692	333.3	1,841	0.583332
2000	513.8	6,570,692	746.2	2,030	0.869791
2200	583.5	7,612,692	1,052	2,252	0.966390
2400	658.2	8,654,692	1,159	2,468	0.991279
2600	670.2	9,696,692	1,472	2,657	0.997256
2800	700.2	10,738,692	1,737	2,873	0.999298
3000	764.3	11,780,692	2,020	3,089	0.999819

bcmax=2