4 Коммуникационный протокол с таймером - устройство и обоснование корректности (1185642), страница 5

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 5)

(î ñîõðàíåíèè ïîðÿäêà âðó÷åíèÿ)Ñëîâà, äîñòàâëåííûå ïðîöåññîì q ïîòðåáèòåëþ, ðàñïîëîæåíû âñòðîãî âîçðàñòàþùåì ïîðÿäêå â ìàññèâå inp .ÄîêàçàòåëüñòâîÏðåäïîëîæèì, ÷òî ïðîöåññ q ïîëó÷àåò ïàêåò hdata, s, i1 , w , ρi èâðó÷àåò ïîòðåáèòåëþ ñëîâî w .Åñëè ïåðåä ñåàíñ ñâÿçè åùå íå áûë îòêðûò (ò.å. cr = false ), òîèç ñîîòíîøåíèÿ âñïîìîãàòåëüíîé ëåììûhdata, s, i1 , w , ρi ∈ Mq =⇒ (cr ∨ B + i1 > pr )ñëåäóåò B + i1 > pr , ò.å. ñëîâî w ïîñòóïèëî â ìàññèâ inp ïîñëåòîãî, êàê â íåì áûëà çàíÿòà ïîçèöèÿ ñ íîìåðîì pr .Åñëè ñåàíñ ñâÿçè áûë îòêðûò (ò.å.

cr = true ), òî i1 = Exp .Òîãäà èç ñîîòíîøåíèÿ (18): cr =⇒ B + Exp = pr + 1 ñëåäóåòðàâåíñòâî B + i1 = pr + 1. Ïîýòîìó w = inp [pr + 1] .Êà÷åñòâåííûé àíàëèç ïðîòîêîëàÕîðîøèì ñ÷èòàåòñÿ òàêîå ðåøåíèå, êîòîðîå íå òîëüêîóäîâëåòâîðÿåò òðåáîâàíèÿì Îòñóòñòâèÿ ïîòåðü è Ñîõðàíåíèåïîðÿäêà âðó÷åíèÿ , íî òàêæå ñîîáùàåò îá óòðàòå êàê ìîæíîìåíüøåãî ÷èñëà ñëîâ. ×òîáû äîñòè÷ü ýòîé öåëè ìû äîëæíûñíàáäèòü ïðîòîêîë, îïèñàííûé â ýòîì ðàçäåëå, íåêîòîðûììåõàíèçìîì, êîòîðûé ïîçâîëÿë áû îòïðàâëÿòü êàæäîå ñëîâîïîâòîðíî (íà ïðîòÿæåíèè èíòåðâàëà îòïðàâëåíèÿ ñëîâà) äî òåõïîð, ïîêà íå áóäåò ïîëó÷åíî ïîäòâåðæäåíèå î åãî äîñòàâêå.Èíòåðâàë îòïðàâëåíèÿ äîëæåí áûòü äîñòàòî÷íî ïðîòÿæåííûì,÷òîáû ïîçâîëèòü îñóùåñòâëÿòü ìíîãîêðàòíóþ ïåðåäà÷óîïðåäåëåííûõ ñëîâ è ñäåëàòü òåì ñàìûì âåðîÿòíîñòü óòðàòûñëîâà êàê ìîæíî ìåíüøåé.Îãðàíè÷åííûå ïîðÿäêîâûå íîìåðàÏîðÿäêîâûå íîìåðà, èñïîëüçóåìûå â ïðîòîêîëå, ìîæíîîãðàíè÷èòü, äîêàçàâ óòâåðæäåíèå, àíàëîãè÷íîå Òåîðåìå 3.8 äëÿñèììåòðè÷íîãî ïðîòîêîëà ðàçäâèæíîãî îêíà.Äëÿ ýòîãî íåîáõîäèìî ââåñòè äîïóùåíèå î òîì, ÷òî ñêîðîñòüïîñòóïëåíèÿ ñëîâ íà âõîä ïðîöåññà p îãðàíè÷åíà òàêèìîáðàçîì, ÷òîáû î÷åðåäíîå ñëîâî ïîñòóïàëî ñïóñòÿ íå ìåíååU + 2µ + R åäèíèö âðåìåíè ïîñëå ïîñòóïëåíèÿ L -ãî ïîïîðÿäêó ïðåäøåñòâóþùåãî ñëîâà.Äëÿ ýòîãî äåéñòâèå Ap íóæíî ñíàáäèòü ïðåäîõðàíèòåëåì{(High < L) ∨ (Ut[B + High − L] < −R − 2µ)}.Òîãäà ïîðÿäêîâûå íîìåðà ïîëó÷åííûõ ïàêåòîâ äàííûõ îòñòîÿòíå áîëåå, ÷åì íà 2L îò îæèäàåìîãî íîìåðà Exp , à ïîðÿäêîâûåíîìåðà â ïîäòâåðæäàþùèõ ñîîáùåíèÿõ îòñòîÿò íå áîëåå, ÷åìíà L îò íîìåðà High .

Ñëåäîâàòåëüíî, ïðè ïåðåäà÷å óâåëè÷åíèåïîðÿäêîâûõ íîìåðîâ ìîæíî ïðîâîäèòü ïî ìîäóëþ 2L .Íåñêîëüêî ñëîâ îá èíâàðèàíòàõÂñå ñîîòíîøåíèÿ (äèçúþíêòû), âõîäÿùèå â ñîñòàâðàññìîòðåííûõ íàìè èíâàðèàíòîâ è êàñàþùèåñÿ ïàêåòîâ,èìåþò ñëåäóþùèé îáùèé âèä:∀m ∈ M : A(m),Íåòðóäíî óáåäèòüñÿ, ÷òî âûïîëíèìîñòü ñîîòíîøåíèé òàêîãîâèäà ñîõðàíÿåòñÿ ïðè äóáëèðîâàíèè èëè ïîòåðå ïàêåòîâ.Èíîãäà ïðèõîäèòñÿ èñïîëüçîâàòü èíâàðèàíòû áîëåå îáùåãîâèäà, íàïðèìåðXf (m) = Kèëèm∈Mïðåäóñëîâèå =⇒ ∃m ∈ M : A(m).Ïðåäëîæåíèÿ òàêîãî âèäà ìîãóò óòðàòèòü èñòèííîñòü â ñëó÷àåïîòåðè èëè äóáëèðîâàíèÿ ïàêåòîâ, è ïîýòîìó èõ íåëüçÿèñïîëüçîâàòü ïðè äîêàçàòåëüñòâå êîððåêòíîñòè àëãîðèòìîâ, îòêîòîðûõ òðåáóåòñÿ óñòîé÷èâîñòü ê ïîäîáíûì ñáîÿì.Çàäà÷èÇàäà÷à 1. ïðîòîêîëå ñ òàéìåðàìè îòïðàâèòåëü ìîæåò çàíåñòè â îò÷åòñëîâî êàê âîçìîæíî óòðà÷åííîå, â òî âðåìÿ êàê ýòî ñëîâî áûëîáëàãîïîëó÷íî äîñòàâëåíî ïîëó÷àòåëþ.1.

Îïèøèòå âûïîëíåíèå ýòîãî ïðîòîêîëà, â õîäå êîòîðîãîïðîèñõîäèò ïîäîáíûé ýôôåêò.2. Ìîæíî ëè ðàçðàáîòàòü òàêîé ïðîòîêîë, â êîòîðîìîòïðàâèòåëü çà îãðàíè÷åííîå âðåìÿ ñîñòàâëÿåò îò÷åò îáîøèáêå â òîì è òîëüêî òîì ñëó÷àå, êîãäà ñëîâî íåäîñòàâëÿåòñÿ ïîëó÷àòåëþ?Çàäà÷èÇàäà÷à 2.Ïðåäïîëîæèì, ÷òî â ñâÿçè ñ âûõîäîì èç ñòðîÿ ÷àñîâîãîìåõàíèçìà, ïîëó÷àòåëü íå ìîæåò çàêðûòü ñåàíñ ñâÿçè âîâðåìÿ.Îïèøèòå âû÷èñëåíèå ïðîòîêîëà ñ òàéìåðàìè, â õîäå êîòîðîãîñëîâî áóäåò óòðà÷åíî, íî îòïðàâèòåëü íå ñìîæåò îòìåòèòü ýòî âîò÷åòå.Çàäà÷à 3.Îïèøèòå òàêîå âû÷èñëåíèå ïðîòîêîëà ñ òàéìåðàìè, â õîäåêîòîðîãî ïîëó÷àòåëü îòêðûâàåò ñåàíñ ñâÿçè ïîñëå ïîëó÷åíèÿïàêåòà ñ ïîðÿäêîâûì íîìåðîì áîëüøèì íóëÿ.Çàäà÷èÇàäà÷à 4.Ïðîåêòèðîâùèê ñåòè õîòåë áû âîñïîëüçîâàòüñÿ ïðîòîêîëîì ñòàéìåðàìè, íî ïðè ýòîì æåëàåò, ÷òîáû î âîçìîæíî óòðà÷åííûõñëîâàõ çàïèñü â îò÷åòå îñóùåñòâëÿëàñü ïîðàíüøå.

Äëÿ ýòîãî îíìîäèôèöèðóåò äåéñòâèå Ep ñëåäóþùèì îáðàçîì:Ep : (* Ñôîðìèðîâàòü îò÷åò îá îøèáêåäëÿ âîçìîæíî óòðà÷åííîãî ñëîâà *){ Ut[B + Low ] < 0 }begin error [B + Low ] := true ; Low := Low + 1endÁóäåò ëè ìîäèôèöèðîâàííûé òàêèì îáðàçîì ïðîòîêîëóäîâëåòâîðÿòü òðåáîâàíèÿì Îòñóòñòâèÿ ïîòåðü èÑîõðàíåíèÿ ïîðÿäêà âðó÷åíèÿ èëè äëÿ ýòîãî íåîáõîäèìîâíåñòè òàêæå äðóãèå èçìåíåíèÿ?Êàêîâû, ïî Âàøåìó ìíåíèþ, ïðåèìóùåñòâà è íåäîñòàòêèóêàçàííîé ìîäèôèêàöèè.ÊÎÍÅÖ ËÅÊÖÈÈ 4..

Характеристики

Список файлов лекций