4 Коммуникационный протокол с таймером - устройство и обоснование корректности (1185642), страница 2
Текст из файла (страница 2)
. High − 1 , è ñîîòâåòñòâóþùèå ýòèì ñëîâàì òàéìåðûèìåþò ïîëîæèòåëüíûå çíà÷åíèÿ.Îòïðàâëåíèå ñîîáùåíèÿ(ïðîöåññîòïðàâèòåëü)Sp :(* Îòïðàâèòü i -å ñëîâî òåêóùåãî ñåàíñà ñâÿçè *){ cs ∧ Low ≤ i < High ∧ Ut[B + i] > 0 }begin sendhdata, (i = Low ), i, inp [B + i], µi ; St := SendÏàêåòû äàííûõ, êîòîðûå îòïðàâëÿþòñÿ ïî õîäó ðàáîòûðàññìàòðèâàåìîãî ïðîòîêîëà ñîñòîÿò èç îñîáîãî áèòà (ò.í.ïðèçíàêà íà÷àëà ïîñëåäîâàòåëüíîñòè ), ïîðÿäêîâîãî íîìåðà èñëîâà. ×òîáû ïðîâîäèòü àíàëèç ïðîòîêîëà, â êàæäîì ïàêåòåâûäåëÿåòñÿ ÷åòâåðòîå (èñêóññòâåííîå) ïîëå, êîòîðîåíàçûâàåòñÿ îñòàâøèìñÿ ñðîêîì æèçíè ïàêåòà .  ýòîì ïîëåóêàçûâàåòñÿ ìàêñèìàëüíîå âðåìÿ, íà ïðîòÿæåíèè êîòîðîãîïàêåò ìîæåò îñòàâàòüñÿ â êàíàëå äî òîãî, êàê îí áóäóòäîñòàâëåí ïî íàçíà÷åíèþ èëè ïîòåðÿí â ñèëó ïðåäïîëîæåíèÿîá îãðàíè÷åííîì âðåìåíè æèçíè ïàêåòà.Îòïðàâëåíèå ñîîáùåíèÿ(ïðîöåññîòïðàâèòåëü)Sp :(* Îòïðàâèòü i -å ñëîâî òåêóùåãî ñåàíñà ñâÿçè *){ cs ∧ Low ≤ i < High ∧ Ut[B + i] > 0 }begin sendhdata, (i = Low ), i, inp [B + i], µi ; St := SendÏðèçíàê íà÷àëà ïîñëåäîâàòåëüíîñòè èñïîëüçóåòñÿ ïîëó÷àòåëåìâ òîì ñëó÷àå, êîãäà ïàêåò ïîëó÷åí ïðè çàêðûòîì ñåàíñå ñâÿçè,äëÿ òîãî, ÷òîáû ðåøèòü, ìîæíî ëè îòêðûòü ñåàíñ ñâÿçè (èïðèíÿòü ñîäåðæàùååñÿ â ïàêåòå ñëîâî).
Îòïðàâèòåëüóñòàíàâëèâàåò â ýòîì áèòå çíà÷åíèå true , êîãäà âñåïðåäûäóùèå ñëîâà óæå ïîëó÷èëè ïîäòâåðæäåíèå èëè áûëèçàíåñåíû â îò÷åò (êàê âåðîÿòíî óòðà÷åííûå).Îòïðàâëåíèå ñîîáùåíèÿ(ïðîöåññîòïðàâèòåëü)Sp :(* Îòïðàâèòü i -å ñëîâî òåêóùåãî ñåàíñà ñâÿçè *){ cs ∧ Low ≤ i < High ∧ Ut[B + i] > 0 }begin sendhdata, (i = Low ), i, inp [B + i], µi ; St := SendÒàéìåð îòïðàâèòåëÿ óñòàíàâëèâàåòñÿ òàê, ÷òîáû èçáåæàòüñèòóàöèè, ïðè êîòîðîé ïîäòâåðæäåíèå ïîñòóïàåò ïðè çàêðûòîìñåàíñå ñâÿçè. Äëÿ ýòîãî ñîåäèíåíèå ïîääåðæèâàåòñÿ ïîìåíüøåé ìåðå S åäèíèö âðåìåíè ïîñëå îòïðàâëåíèÿ î÷åðåäíîãîïàêåòà, ãäå S ≥ R + 2µ . Âñÿêèé ðàç, êîãäà îòïðàâëÿåòñÿíåêîòîðûé ïàêåò, íà òàéìåðå St óñòàíàâëèâàåòñÿ âðåìÿ S .Ïðèåì ïîäòâåðæäåíèÿ (ïðîöåññîòïðàâèòåëü)Rp :(* Ïîëó÷èòü ïîäòâåðæäåíèå *){ cs ∧ hack, i, ρi ∈ Mp }begin receive hack, i, ρi ; Low := max (Low , i)endÏðè îòêðûòîì ñåàíñå ñâÿçè ïðîöåññ-îòïðàâèòåëü îæèäàåò îòïðîöåññà-ïîëó÷àòåëÿ ïîäòâåðæäåíèÿ îá óñïåøíîé ïåðåäà÷åêàæäîãî îòïðàâëåííîãî ñëîâà.Ïðèåì ïîäòâåðæäåíèÿ (ïðîöåññîòïðàâèòåëü)Rp :(* Ïîëó÷èòü ïîäòâåðæäåíèå *){ cs ∧ hack, i, ρi ∈ Mp }begin receivehack, i, ρi ; Low := max (Low , i)end ïàêåò ñ ïîäòâåðæäåíèåì âêëàäûâàåòñÿ òîëüêî ñëåäóþùèéïîðÿäêîâûé íîìåð ñîîáùåíèÿ, îæèäàåìîãîïðîöåññîìïîëó÷àòåëåì q .
Êàê è â ïðåäûäóùåì ñëó÷àå, äëÿïðîâåäåíèÿ àíàëèçà ìû áóäåì ñ÷èòàòü, ÷òî â ïàêåòå ñïîäòâåðæäåíèåì òàêæå óêàçûâàåòñÿ îñòàâøååñÿ âðåìÿ æèçíèýòîãî ïàêåòà.Ïðèåì ïîäòâåðæäåíèÿ (ïðîöåññîòïðàâèòåëü)Rp :(* Ïîëó÷èòü ïîäòâåðæäåíèå *){ cs ∧ hack, i, ρi ∈ Mp }begin receivehack, i, ρi ; Low := max (Low , i)endÏîñëå ïîëó÷åíèÿ ïîäòâåðæäåíèÿ èçìåíÿåòñÿ ïîëîæåíèåíèæíåé ñòâîðêè îêíà ïåðåäà÷è Low . Íîìåð i ïîñòóïèâøåãîïîäòâåðæäåíèÿ îçíà÷àåò, ÷òî âñå ñëîâà ñ íîìåðàìè ìåíüøèìè ióæå áûëè óñïåøíî äîñòàâëåíû.Ôîðìèðîâàíèå çàïèñè î ïîòåðå ñëîâà(ïðîöåññîòïðàâèòåëü)Ep :(* Ñôîðìèðîâàòü ñîîáùåíèå îá îøèáêåâ ñâÿçè ñ âîçìîæíîé ïîòåðåé ñëîâà *){ cs ∧ Ut[B + Low ] ≤ −2µ − R }begin error [B + Low ] := true ; Low := Low + 1endÇàìåòèì, ÷òî ïðè ïîñòóïëåíèè ñëîâà ñ íîìåðîì Low çíà÷åíèåñîîòâåòñòâóþùåãî òàéìåðà Ut[B + Low ] áûëî óñòàíîâëåíîðàâíûì U (ïðîòÿæåííîñòü èíòåðâàëà îòïðàâëåíèÿ).
Ïîýòîìóçàïèñü î ïîòåðå ñëîâà ôîðìèðóåòñÿ â òîì ñëó÷àå, êîãäàèñòåêëî âðåìÿ U , îòâåäåííîå íà îòïðàâëåíèå ýòîãî ñëîâà,âðåìÿ, îòâåäåííîå íà åãî ïðèåì R , âðåìÿ æèçíè ñîîáùåíèÿ µè âðåìÿ æèçíè ïîäòâåðæäåíèÿ î ïîëó÷åíèè ñîîáùåíèÿ µ .Ôîðìèðîâàíèå çàïèñè î ïîòåðå ñëîâà(ïðîöåññîòïðàâèòåëü)Ep :(* Ñôîðìèðîâàòü ñîîáùåíèå îá îøèáêåâ ñâÿçè ñ âîçìîæíîé ïîòåðåé ñëîâà *){ cs ∧ Ut[B + Low ] ≤ −2µ − R }begin error [B + Low ] := true ; Low := Low + 1end çàïèñè îá îøèáêå ðåãèñòðèðóåòñÿ, ÷òî ñëîâî ñ íîìåðîì Lowèëè ïîäòâåðæäåíèå î åãî óñïåøíîé äîñòàâêå áûëî ïîòåðÿíî, èíå ñëåäóåò áîëåå îæèäàòü îò ïðîöåññàïîëó÷àòåëÿ ïîñòóïëåíèÿïîäòâåðæäåíèÿ î åãî äîñòàâêå. Òàêîå ñëîâî ñ÷èòàåòñÿ¾âåðîÿòíî ïîòåðÿííûì¿.Çàêðûòèå ñåàíñà ñâÿçè (ïðîöåññîòïðàâèòåëü)Cp :(* Çàêðûòü ñåàíñ ñâÿçè *){ cs ∧ St < 0 ∧ Low = High }begin B := B + High ; delete(St, High, Low )(* cs := false *)endÇàêðûòèå ñåàíñà ñâÿçè ïðîöåññîìîòïðàâèòåëåì ïðîèñõîäèòïîñëå òîãî, êàêÇàêðûòèå ñåàíñà ñâÿçè (ïðîöåññîòïðàâèòåëü)Cp :(* Çàêðûòü ñåàíñ ñâÿçè *)∧ St < 0 ∧}{begin B := B + High ; delete(St, High, Low )(* cs := false *)endÇàêðûòèå ñåàíñà ñâÿçè ïðîöåññîìîòïðàâèòåëåì ïðîèñõîäèòïîñëå òîãî, êàêIèñòåêëî âðåìÿ îòïðàâëåíèÿ âñåõ ïîñòóïèâøèõ ñëîâ èÇàêðûòèå ñåàíñà ñâÿçè (ïðîöåññîòïðàâèòåëü)Cp :(* Çàêðûòü ñåàíñ ñâÿçè *)∧∧ Low = High }{begin B := B + High ; delete(St, High, Low )(* cs := false *)endÇàêðûòèå ñåàíñà ñâÿçè ïðîöåññîìîòïðàâèòåëåì ïðîèñõîäèòïîñëå òîãî, êàêIâñå ïîñòóïèâøèå ñëîâà áûëè ëèáî óñïåøíî äîñòàâëåíû,ëèáî çàðåãèñòðèðîâàíû êàê ¾âåðîÿòíî ïîòåðÿííûå¿.Çàêðûòèå ñåàíñà ñâÿçè (ïðîöåññîòïðàâèòåëü)Cp :(* Çàêðûòü ñåàíñ ñâÿçè *){ cs ∧ St < 0 ∧ Low = High }begin B := B + High ; delete(St, High, Low )(* cs := false *)endÇàêðûòèå ñåàíñà ñâÿçè ïðîöåññîìîòïðàâèòåëåì ïðîèñõîäèòïîñëå òîãî, êàêIèñòåêëî âðåìÿ îòïðàâëåíèÿ âñåõ ïîñòóïèâøèõ ñëîâ èIâñå ïîñòóïèâøèå ñëîâà áûëè ëèáî óñïåøíî äîñòàâëåíû,ëèáî çàðåãèñòðèðîâàíû êàê ¾âåðîÿòíî ïîòåðÿííûå¿.Çàêðûòèå ñåàíñà ñâÿçè (ïðîöåññîòïðàâèòåëü)Cp :(* Çàêðûòü ñåàíñ ñâÿçè *){ cs ∧ St < 0 ∧ Low = High }begin B := B + High ; delete(St, High, Low )(* cs := false *)endB ýòî âñïîìîãàòåëüíàÿ ïåðåìåííàÿ, êîòîðàÿ ââåäåíà òîëüêîäëÿ äîêàçàòåëüñòâà êîððåêòíîñòè ïðîòîêîëà.
Îòïðàâèòåëü âêàæäîì ñåàíñå ñâÿçè ïðîâîäèò íóìåðàöèþ ñëîâ, íà÷èíàÿ ñ 0 , è÷òîáû ïðè àíàëèçå ïðîòîêîëà ïðîâîäèòü ðàçëè÷èå ìåæäóñëîâàìè â ðàçíûõ ñåàíñàõ ñâÿçè, ìû íóìåðóåì ïîäðÿä âñåñëîâà.  òîì ñëó÷àå, êîãäà îòïðàâèòåëü äàåò íåêîòîðîìó ñëîâóíîìåð i , ¾àáñîëþòíûé¿ íîìåð ýòîãî ñëîâà áóäåò ðàâåí B + i ,ãäå B ýòî ñóììàðíîå ÷èñëî ïàêåòîâ, ïîñòóïèâøèõ ïðîöåññó pâ ïðåäûäóùèå ñåàíñû ñâÿçè. Ïðè ðåàëèçàöèè ïðîòîêîëà äëÿïåðåìåííîé B ïàìÿòè íå îòâîäèòñÿ, è îòïðàâèòåëü ¾çàáûâàåò¿îáî âñåõ ñëîâàõ inp [0..B − 1] .Çàêðûòèå ñåàíñà ñâÿçè (ïðîöåññîòïðàâèòåëü)Ñëîâà ïåðâîãî Ñëîâà âòîðîãîñåàíñà ñâÿçèñåàíñà ñâÿçè0Òåêóùèé ñåàíñ ñâÿçèB B + Low B + High? ??îêíîîòïðàâ.6 60 LowÈíäåêñàöèÿ ñëîâ â ïðîòîêîëå:6HighÎïèñàíèå ïðîòîêîëà ñ òàéìåðàìè(ïðîöåññïîëó÷àòåëü)Rq : { hdata, s, i, w , ρi ∈ Mq }begin receivehdata, s, i, w , ρi ;if crtheni = Exp thenbegin Rt := R ; Exp := i + 1 ; deliver welse if s = true thenbegin create (Rt, Exp) ; (* cr := true *)Rt := R ; Exp := i + 1 ; deliver wifendendSq : {cr}beginsend hack, Exp, µiendendÏîëó÷åíèå ñîîáùåíèÿ (ïðîöåññïîëó÷àòåëü)Rq : (* Ïðèíÿòü ïàêåò äàííûõ *){ hdata, s, i, w , ρi ∈ Mq }begin receivehdata, s, i, w , ρi ;if crtheni = Exp thenbegin Rt := R ; Exp := i + 1 ; deliver welse if s = true thenbegin create (Rt, Exp) ; (* cr := true *)Rt := R ; Exp := i + 1 ; deliver wifendendendÏðîöåññïîëó÷àòåëü ïðèíèìàåò ïîñòóïèâøåå ñîîáùåíèå.Ïîëó÷åíèå ñîîáùåíèÿ (ïðîöåññïîëó÷àòåëü)Rq : (* Ïðèíÿòü ïàêåò äàííûõ *){ hdata, s, i, w , ρi ∈ Mq }begin receivehdata, s, i, w , ρi ;ifcrtheni = Exp thenRt := R ; Exp := i + 1 ; deliver welse if s = true thenbegin create (Rt, Exp) ; (* cr := true *)Rt := R ; Exp := i + 1 ; deliver wifbeginendendendè ïðîâåðÿåò, áûë ëè óæå îòêðûò ñåàíñ ñâÿçè äëÿ ïðèåìàñîîáùåíèé.Ïîëó÷åíèå ñîîáùåíèÿ (ïðîöåññïîëó÷àòåëü)Rq : (* Ïðèíÿòü ïàêåò äàííûõ *){ hdata, s, i, w , ρi ∈ Mq }begin receivehdata, s, i, w , ρi ;if crtheni = Exp thenbegin Rt := R ; Exp := i + 1 ; deliver welse if s = true thenbegin create (Rt, Exp) ; (* cr := true *)Rt := R ; Exp := i + 1 ; deliver wifendendendÅñëè ñåàíñ ñâÿçè áûë îòêðûò, òî ïðîöåññïîëó÷àòåëü âûÿñíÿåò,èìååò ëè ïîëó÷åííîå ñëîâî îæèäàåìûé íîìåð Exp .
Åñëè íîìåðïîëó÷åííîãî ñëîâà íå ñîâïàäàåò ñ òåì íîìåðîì, êîòîðûéîæèäàåòñÿ, òî ýòî ñëîâî èãíîðèðóåòñÿ.Ïîëó÷åíèå ñîîáùåíèÿ (ïðîöåññïîëó÷àòåëü)Rq : (* Ïðèíÿòü ïàêåò äàííûõ *){ hdata, s, i, w , ρi ∈ Mq }begin receivehdata, s, i, w , ρi ;if crtheni = Exp thenbegin Rt := R ; Exp := i + 1 ; deliver welse if s = true thenbegin create (Rt, Exp) ; (* cr := true *)Rt := R ; Exp := i + 1 ; deliver wifendendendÅñëè íîìåð ïîëó÷åííîãî ñëîâà ðàâåí îæèäàåìîìó íîìåðó Exp ,òî ñëîâî âðó÷àåòñÿ ïîòðåáèòåëþ, è îæèäàåìûé íîìåðóâåëè÷èâàåòñÿ.Ïîëó÷åíèå ñîîáùåíèÿ (ïðîöåññïîëó÷àòåëü)Rq : (* Ïðèíÿòü ïàêåò äàííûõ *){ hdata, s, i, w , ρi ∈ Mq }begin receive hdata, s, i, w , ρi ;if crtheni = Exp thenRt := R ; Exp := i + 1 ; deliver welse if s = true thenbegin create (Rt, Exp) ; (* cr := true *)Rt := R ; Exp := i + 1 ; deliver wifbeginendendendÅñëè ñåàíñ ñâÿçè íå îòêðûò, òî ïðîöåññ-ïîëó÷àòåëü âûÿñíÿåò,ÿâëÿåòñÿ ëè ïîñòóïèâøåå ñëîâî ïåðâûì ñëîâîì â ïåðåäàâàåìîéïîñëåäîâàòåëüíîñòè ñëîâ (ïðîâåðÿåò ïðèçíàê íà÷àëàïîñëåäîâàòåëüíîñòè s ).
Åñëè ýòî íå ïåðâîå ñëîâîïîñëåäîâàòåëüíîñòè, òî îíî èãíîðèðóåòñÿ.Ïîëó÷åíèå ñîîáùåíèÿ (ïðîöåññïîëó÷àòåëü)Rq : (* Ïðèíÿòü ïàêåò äàííûõ *){ hdata, s, i, w , ρi ∈ Mq }begin receive hdata, s, i, w , ρi ;if crtheni = Exp thenbegin Rt := R ; Exp := i + 1 ; deliver welse if s = true thenbegin create(Rt, Exp) ; (* cr := true *)Rt := R ; Exp := i + 1 ; deliver wifendendendÅñëè ïîëó÷åííîå ñëîâî ÿâëÿåòñÿ ïåðâûì ñëîâîìïîñëåäîâàòåëüíîñòè, òî îòêðûâàåòñÿ ñåàíñ ñâÿçè,óñòàíàâëèâàåòñÿ òàéìåð ïðèåìà Rt , è ïîëó÷åííîå ñëîâîâðó÷àåòñÿ ïîòðåáèòåëþ.Îòïðàâëåíèå ïîäòâåðæäåíèé(ïðîöåññïîëó÷àòåëü)Sq :(* Îòïðàâèòü ïîäòâåðæäåíèå *){ cr }begin send hack, Exp, µi endÎòïðàâëÿåìîå ïîäòâåðæäåíèå ñâèäåòåëüñòâóåò î òîì, ÷òî âñåñëîâà òåêóùåãî ñåàíñà ñâÿçè ñ íîìåðàìè, ìåíüøèìèîæèäàåìîãî íîìåðà Exp , áûëè óñïåøíî äîñòàâëåíûïîòðåáèòåëþ.Îïèñàíèå ïðîòîêîëà ñ òàéìåðàìè(êîììóíèêàöèîííàÿ ñðåäà è âðåìÿ)Loss:{m∈M }(* M ýòî ëèáî Mp , ëèáî Mq *)remove m from M endbeginDuplTime: {m∈M }(* M ýòî ëèáî Mp , ëèáî Mq *)begin insert m in M end: (* δ > 0 *)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 packetbegin forallendendÊîììóíèêàöèîííàÿ ñðåäàLoss:{m∈M }(* M ýòî ëèáî Mp , ëèáî Mq *)remove m from M endbeginDupl: {m∈M }(* M ýòî ëèáî Mp , ëèáî Mq *)begin insert m in M endÊîììóíèêàöèîííàÿ ïîäñèñòåìà ïðåäñòàâëåíà äâóìÿìóëüòèìíîæåñòâàìè: Mp äëÿ ïàêåòîâ, àäðåñîâàííûõ ïðîöåññó p, è Mq äëÿ ïàêåòîâ, àäðåñîâàííûõ ïðîöåññó q .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
