IEEE 802.3 CSMA/CD Protocol

// Modest model for the IEEE 802.3 CSMA/CD protocol
action send, send1, send2;
action end, end1, end2;
action busy, busy1, busy2;
action cd;

const int RED = 2; // reduction factor
const int PD = (int)(26 / RED); // signal propagation delay
const int TD = (int)(808 / RED); // packet transmission delay
const int ST = 2 * PD; // backoff time slot length
const int BCMAX = 1; // 1 or 2

// Properties
// Probabilistic reachability
// "with probability 1, eventually both stations send their packet correctly"
property P_1 = P(<> did(end1) && did(end2)) >= 1.0;

// Probabilistic time-bounded reachability
// "the minimum/maximum probability of both stations
// correctly delivering their packets by the deadline D"
const int D = (int)(1800 / RED);
property D_max = Pmax(<> did(end1) && did(end2) && time <= D);
property D_min = Pmin(<> did(end1) && did(end2) && time <= D);

// Expected reachability
// "the minimum/maximum expected time until both stations correctly deliver their packets"
property E_min = Tmin(did(end1) && did(end2));
property E_max = Tmax(did(end1) && did(end2));


process Medium()
{
   clock c;

   do {
      :: alt { :: send1 {= c=0 =} :: send2 {= c=0 =} };
         do {
            :: alt { :: end1 {= c=0 =} :: end2 {= c=0 =} }; // transfer finished
               urgent break
            :: when(c <= PD)
               alt { :: send1 {= c=0 =} :: send2 {= c=0 =} }; // collision
               invariant(c <= PD) cd {= c=0 =}; // collision detection
               urgent break
            :: when(c >= PD)
               alt { :: busy1 :: busy2 } // carrier is sensed busy
         }
   }
}

process Station()
{
   clock c;
   int bc limit [0..BCMAX];
   int backoff limit [0..pow(2, BCMAX + 1) - 1];

   invariant(c <= 0) send {= c=0 =};
   do {
      :: invariant(c <= TD) alt {
         :: when(c == TD) end {= c=0 =};
            urgent break
         :: cd {= c=0, bc=min(bc + 1, BCMAX) =};
            do {
               :: urgent {= backoff=DiscreteUniform(0, pow(2, bc + 1) - 1) =};
                  invariant(c <= backoff * ST) when(c == backoff * ST) alt {
                     :: send {= c=0 =}; urgent break
                     :: busy {= c=0, bc=min(bc + 1, BCMAX) =}
                  }
            }
         }
   }
}


par {
   :: Medium()
   :: relabel { send, end, busy } by { send1, end1, busy1 } Station()
   :: relabel { send, end, busy } by { send2, end2, busy2 } Station()
}