Correctness of stop wait with integer SN, RN Assume, for a to( from)B transmission, that All errors are detected as errors Initially no frames are on link, SN=0, RN=O Frames may be arbitrarily delayed or lost Each frame is correctly received with at least some probability q>0 Split proof of correctness into two parts SAFETY: show that no packet is ever released out of order or more than once LIVENESS: show that every packet is eventually released Eytan modianoCorrectness of stop & wait with integer SN, RN • Assume, for A to (from) B transmission, that – All error s are detected as errors – Initially no frames are on link, SN=0, RN=0 – Frames may be arbitrarily delayed or lost – E a ch frame is correctly recei ved with at least some probability q>0. • Split proof of correctness into two parts: – SAFETY: show that no packet i s ever r eleased out o f order o r m ore than once – LIVENESS: show that every packet is eventually released Eyt an Modiano 8