Лекция 4. Коммуникационный протокол. Устройство_ корректность и модификации протокола с таймером (1185654), страница 4
Текст из файла (страница 4)
ýòî äåéñòâèå íåâëèÿåò íà ïåðåìåííûå ýòèõ ñîîòíîøåíèé.Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Rq : { hdata, s, i, w , ρi ∈ Mq }begin receive hdata, s, i, w , ρi ;if crtheni = Exp then begin Rt := R ; Exp := i + 1 ; deliver w endelse if s = true then begin create (Rt, Exp) ; (* cr := true *)Rt := R ; Exp := i + 1 ; deliver w endifendcr ⇒ 0 < Rt ≤ R∧ ∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µ∧ hdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + R∧ cr ⇒ cs ∧ St ≥ Rt + µ(2)(4)(5)(6)Ñîîòíîøåíèå (2) ñîõðàíÿåòñÿ, ò.ê.
ïåðåìåííîé Rt âñåãäàïðèñâàèâàåòñÿ çíà÷åíèå R (åñëè ïðèñâàèâàíèå èìååò ìåñòî).Ñîîòíîøåíèå (6) ñîõðàíÿåòñÿ, ò.ê. ïåðåìåííîé Rtïðèñâàèâàåòñÿ çíà÷åíèå R òîëüêî ïðè ïîëó÷åíèè ïàêåòàhdata, s, i, w , ρi, à èç (4) è (5) ñëåäóåò, ÷òî â ýòîì ñëó÷àåâûïîëíÿåòñÿ ôîðìóëà cs ∧ St ≥ R + µ .Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Sq :(* Îòïðàâèòü ïîäòâåðæäåíèå *){ cr }begin send hack, Exp, µi endP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèÿ (1-3),(5-6) è (8) ñîõðàíÿþòñÿ, ò.ê.
ýòî äåéñòâèå íåâëèÿåò íà ïåðåìåííûå ýòèõ ñîîòíîøåíèé.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Sq :(* Îòïðàâèòü ïîäòâåðæäåíèå *){ cr }begin send hack, Exp, µi endP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèå (4) ñîõðàíÿåòñÿ, ò.ê.
ïðè îòïðàâëåíèè êàæäîãîïàêåòà îñòàâøååñÿ âðåìÿ åãî æèçíè ïîëàãàåòñÿ ðàâíûì µ .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Sq :(* Îòïðàâèòü ïîäòâåðæäåíèå *){ cr }begin send hack, Exp, µi endP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèå (7) ñîõðàíÿåòñÿ, ò.ê. ïðè îòïðàâëåíèè ïàêåòàhack, i, ρi â ñëó÷àå, êîãäà cr èìååò çíà÷åíèå true, âûïîëíÿåòñÿðàâåíñòâî ρ = µ , è ïîýòîìó èç ñîîòíîøåíèé (2) è (6) ñëåäóåòSt > µ .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Loss:{m∈M }(* M ýòî ëèáî Mp , ëèáî Mq *)remove m from M endbeginP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèÿ (1-3) è (6) ñîõðàíÿþòñÿ, ò.ê.
ýòî äåéñòâèå íåâëèÿåò íà ïåðåìåííûå ýòèõ ñîîòíîøåíèé. Ñîîòíîøåíèÿ (4-5) è(7-8) ñîõðàíÿþòñÿ, ò.ê. èçúÿòèå ïàêåòà ìîæåò ïðèâåñòè ëèøü êòîìó, ÷òî íàðóøàòñÿ ïðåäïîñûëêè ýòèõ ñîîòíîøåíèé.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Dupl:{ m ∈ M }(* M ýòî ëèáî Mp , ëèáî Mq *)begin insert m in M endP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèÿ (1-3) è (6) ñîõðàíÿþòñÿ, ò.ê. ýòî äåéñòâèå íåâëèÿåò íà ïåðåìåííûå ýòèõ ñîîòíîøåíèé.
Ñîîòíîøåíèÿ (4-5) è(7-8) ñîõðàíÿþòñÿ, ò.ê. äóáëèðóþùàÿ âñòàâêà ïàêåòà mâîçìîæíà òîëüêî òîãäà, êîãäà ïàêåò m óæå ñîäåðæèòñÿ âêàíàëå; îòñþäà ñëåäóåò, ÷òî ñëåäñòâèÿ ñîîòâåòñòâóþùèõñîîòíîøåíèé óæå áûëè âûïîëíåíû óæå ïåðåä ñàìîé âñòàâêîé.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0:i do Ut[i] := Ut[i] − δ ; St := St − δ ; Rt := Rt − δif Rt ≤ 0 then delete (Rt, Exp); (* cr := false *)forall h.., ρi ∈ Mp , Mq dobegin ρ := ρ − δ ; if ρ ≤ 0 then remove packet endTime begin forallendP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèÿ (1), (2) è (3) ñîõðàíÿþåòñÿ, ò.ê. çíà÷åíèÿïåðåìåííûõ St , Rt è Ut[i] ìîãóò ëèøü óìåíüøèòüñÿ, è ñåàíññâÿçè ïîëó÷àòåëÿ çàêðûâàåòñÿ, êîãäà çíà÷åíèå Rt ñòàíîâèòñÿðàâíûì 0 .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0:i do Ut[i] := Ut[i] − δ ; St := St − δ ; Rt := Rt − δif Rt ≤ 0 then delete (Rt, Exp); (* cr := false *)forall h.., ρi ∈ Mp , Mq dobegin ρ := ρ − δ ; if ρ ≤ 0 then remove packet endTime begin forallendP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèå (4) ñîõðàíÿåòñÿ, ò.ê.
çíà÷åíèå ρ ìîæåò ëèøüóìåíüøèòüñÿ, è ïàêåò èçûìàåòñÿ, êîãäà çíà÷åíèå åãî ïîëÿ ρñòàíîâèòñÿ ðàâíûì 0 .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0:i do Ut[i] := Ut[i] − δ ; St := St − δ ; Rt := Rt − δif Rt ≤ 0 then delete (Rt, Exp); (* cr := false *)forall h.., ρi ∈ Mp , Mq dobegin ρ := ρ − δ ; if ρ ≤ 0 then remove packet endTime begin forallendP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Äåéñòâèå Time óìåíüøàåò çíà÷åíèÿ âñåõ òàéìåðîâ (è òåõ,êîòîðûå ñîäåðæàòñÿ â ïîëå ρ ïàêåòîâ) íà îäíó è òó æåâåëè÷èíó.
Ïîýòîìó ñîõðàíÿþòñÿ âñå ñîîòíîøåíèÿ âèäàXt ≥ Yt + C , ãäå Xt è Yt òàéìåðû, à C êîíñòàíòà.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0:i do Ut[i] := Ut[i] − δ ; St := St − δ ; Rt := Rt − δRt ≤ 0 then delete (Rt, Exp); (* cr := false *)forall h.., ρi ∈ Mp , Mq dobegin ρ := ρ − δ ; if ρ ≤ 0 then remove packet endTime begin forallifendP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High) ñîîòíîøåíèè (8) íåò òàéìåðîâ, è ïîýòîìó îíî ñîõðàíÿåòñÿ.(1)(2)(3)(4)(5)(6)(7)(8)Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÏåðâîå òðåáîâàíèå, êîòîðîå ïðåäúÿâëÿåòñÿ êðàññìàòðèâàåìîìó ïðîòîêîëó, ñîñòîèò â òîì, ÷òî êàæäîå ñëîâîäîëæíî áûòü ðàíî èëè ïîçäíî äîñòàâëåíî ïî íàçíà÷åíèþ èëèçàíåñåíî â îò÷åò êàê óòðà÷åííîå.
Îïðåäåëèì ïðåäèêàò Ok(i)ñëåäóþùåé ôîðìóëîéOk(i) ⇔ error [i] = true ∨ ïðîöåññó q áûëî äîñòàâëåíî ñëîâî inp [i].Ïîêàæåì, ÷òî ïðîòîêîë íå òåðÿåò íè îäíîãî ñëîâà, íå îòìåòèâýòîãî ôàêòà.Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÒåîðåìà 4.2.Ñëåäóþùåå óòâåðæäåíèå ÿâëÿåòñÿ èíâàðèàíòîì ïðîòîêîëà ñòàéìåðàìè.P1 ≡∧∧∧∧∧P0¬ cs =⇒ ∀i < B : Ok(i)(9)cs =⇒ ∀i < B + Low : Ok(i)(10)hdata, true, I , w , ρi ∈ Mq =⇒ ∀i < B + I : Ok(i) (11)cr =⇒ ∀i < B + Exp : Ok(i)(12)hack, I , ρi ∈ Mp =⇒ ∀i < B + I : Ok(i)(13)Äîêàçàòåëüñòâî.ÑÀÌÎÑÒÎßÒÅËÜÍÎ.Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÑäåëàâ äîïîëíèòåëüíîå äîïóùåíèå, ìû ìîæåì äîêàçàòü òåïåðüïåðâóþ ÷àñòü ñïåöèôèêàöèè ïðîòîêîëà. Áåç ýòîãî äîïóùåíèÿîòïðàâèòåëü ìîæåò îêàçàòüñÿ ÷åðåñ÷óð ¾ëåíèâûì¿ ïðèñîñòàâëåíèè îò÷åòà î ïîòåðÿííûõ ñëîâàõ, à â àëãîðèòìå âñåãîëèøü óêàçàíî, ÷òî ñîîáùåíèå î ïîòåðå íå ìîæåò áûòüñôîðìèðîâàíî â òå÷åíèå 2µ + R åäèíèö âðåìåíè, ñëåäóþùèõçà îêîí÷àíèåì èíòåðâàëà îòïðàâëåíèÿ ñëîâà, íî òàì íå ñêàçàíîî òîì, ÷òî ýòî ñîîáùåíèå ðàíî èëè ïîçäíî îáÿçàíî áûòüñôîðìèðîâàíî.Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÑäåëàâ äîïîëíèòåëüíîå äîïóùåíèå, ìû ìîæåì äîêàçàòü òåïåðüïåðâóþ ÷àñòü ñïåöèôèêàöèè ïðîòîêîëà.
Áåç ýòîãî äîïóùåíèÿîòïðàâèòåëü ìîæåò îêàçàòüñÿ ÷åðåñ÷óð ¾ëåíèâûì¿ ïðèñîñòàâëåíèè îò÷åòà î ïîòåðÿííûõ ñëîâàõ, à â àëãîðèòìå âñåãîëèøü óêàçàíî, ÷òî ñîîáùåíèå î ïîòåðå íå ìîæåò áûòüñôîðìèðîâàíî â òå÷åíèå 2µ + R åäèíèö âðåìåíè, ñëåäóþùèõçà îêîí÷àíèåì èíòåðâàëà îòïðàâëåíèÿ ñëîâà, íî òàì íå ñêàçàíîî òîì, ÷òî ýòî ñîîáùåíèå ðàíî èëè ïîçäíî îáÿçàíî áûòüñôîðìèðîâàíî. Ïîýòîìó ñäåëàåì äîïîëíèòåëüíîå äîïóùåíèå îòîì, ÷òî äåéñòâèå Ep ðàíî èëè ïîçäíî áóäåò âûïîëíåíîïðîöåññîì p â ðàçóìíûå ñðîêè, ñêàæåì, äî òîãî , êàêUt[B + Low ] ñòàíåò ðàâíûì −2µ − R − λ .Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÒåîðåìà 4.3.
(îá îòñóòñòâèè ïîòåðü)Êàæäîå ñëîâà ìàññèâà inp ëèáî äîñòèãàåò ïðîöåññà q , ëèáîîòìå÷àåòñÿ ïðîöåññîì p êàê óòðà÷åííîå â òå÷åíèåU + 2µ + R + λ åäèíèö âðåìåíè ïîñëå ïîñòóïëåíèÿ ýòîãî ñëîâàïðîöåññó p .Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÄîêàçàòåëüñòâîÏðè ïîñòóïëåíèè ñëîâà inp [I ] âûïîëíÿåòñÿ íåðàâåíñòâîB + High > I , è îíî ïðîäîëæàåò âûïîëíÿòüñÿ äàëåå.Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÄîêàçàòåëüñòâîÏðè ïîñòóïëåíèè ñëîâà inp [I ] âûïîëíÿåòñÿ íåðàâåíñòâîB + High > I , è îíî ïðîäîëæàåò âûïîëíÿòüñÿ äàëåå. Åñëè ñåàíññâÿçè çàêðûâàåòñÿ ñïóñòÿ ïðåäïèñàííûé ïåðèîä âðåìåíè ïîñëåïîñòóïëåíèÿ ñëîâà inp [I ] , òî B > I , è óòâåðæäåíèå òåîðåìûñëåäóåò èç ñîîòíîøåíèÿ (9): ¬ cs =⇒ ∀i < B : Ok(i) .Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÄîêàçàòåëüñòâîÏðè ïîñòóïëåíèè ñëîâà inp [I ] âûïîëíÿåòñÿ íåðàâåíñòâîB + High > I , è îíî ïðîäîëæàåò âûïîëíÿòüñÿ äàëåå. Åñëè ñåàíññâÿçè çàêðûâàåòñÿ ñïóñòÿ ïðåäïèñàííûé ïåðèîä âðåìåíè ïîñëåïîñòóïëåíèÿ ñëîâà inp [I ] , òî B > I , è óòâåðæäåíèå òåîðåìûñëåäóåò èç ñîîòíîøåíèÿ (9): ¬ cs =⇒ ∀i < B : Ok(i) .Åñëè ñåàíñ ñâÿçè îñòàåòñÿ îòêðûòûì, è B + Low ≤ I , òî âñåñëîâà ñ íîìåðàìè èç îòðåçêå B + Low · · · I áóäóò îòìå÷åíû âîò÷åòå ñïóñòÿ 2µ + R åäèíèö âðåìåíè ïî îêîí÷àíèè èíòåðâàëàâðåìåíè, îòâåäåííîãî äëÿ îòïðàâëåíèÿ ñëîâà inp [I ] .Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÄîêàçàòåëüñòâîÏðè ïîñòóïëåíèè ñëîâà inp [I ] âûïîëíÿåòñÿ íåðàâåíñòâîB + High > I , è îíî ïðîäîëæàåò âûïîëíÿòüñÿ äàëåå.
Åñëè ñåàíññâÿçè çàêðûâàåòñÿ ñïóñòÿ ïðåäïèñàííûé ïåðèîä âðåìåíè ïîñëåïîñòóïëåíèÿ ñëîâà inp [I ] , òî B > I , è óòâåðæäåíèå òåîðåìûñëåäóåò èç ñîîòíîøåíèÿ (9): ¬ cs =⇒ ∀i < B : Ok(i) .Åñëè ñåàíñ ñâÿçè îñòàåòñÿ îòêðûòûì, è B + Low ≤ I , òî âñåñëîâà ñ íîìåðàìè èç îòðåçêå B + Low · · · I áóäóò îòìå÷åíû âîò÷åòå ñïóñòÿ 2µ + R åäèíèö âðåìåíè ïî îêîí÷àíèè èíòåðâàëàâðåìåíè, îòâåäåííîãî äëÿ îòïðàâëåíèÿ ñëîâà inp [I ] .
Ïîýòîìóçàïèñü â îò÷åòå áóäóò ñäåëàíà 2µ + R + λ åäèíèö âðåìåíè ïîñëåîêîí÷àíèÿ ñðîêà, îòâåäåííîãî äëÿ îòïðàâëåíèÿ ñîîáùåíèÿ, ò.å.ñïóñòÿ U + 2µ + R + λ åäèíèö âðåìåíè ïîñëå ïîñòóïëåíèÿñëîâà.Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÄîêàçàòåëüñòâîÏðè ïîñòóïëåíèè ñëîâà inp [I ] âûïîëíÿåòñÿ íåðàâåíñòâîB + High > I , è îíî ïðîäîëæàåò âûïîëíÿòüñÿ äàëåå. Åñëè ñåàíññâÿçè çàêðûâàåòñÿ ñïóñòÿ ïðåäïèñàííûé ïåðèîä âðåìåíè ïîñëåïîñòóïëåíèÿ ñëîâà inp [I ] , òî B > I , è óòâåðæäåíèå òåîðåìûñëåäóåò èç ñîîòíîøåíèÿ (9): ¬ cs =⇒ ∀i < B : Ok(i) .Åñëè ñåàíñ ñâÿçè îñòàåòñÿ îòêðûòûì, è B + Low ≤ I , òî âñåñëîâà ñ íîìåðàìè èç îòðåçêå B + Low · · · I áóäóò îòìå÷åíû âîò÷åòå ñïóñòÿ 2µ + R åäèíèö âðåìåíè ïî îêîí÷àíèè èíòåðâàëàâðåìåíè, îòâåäåííîãî äëÿ îòïðàâëåíèÿ ñëîâà inp [I ] .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
