Анализа на опфат

Анализата на опфат - решение за проблемот со достапноста во конкретниот контекст на дистрибуираните системи. Се користи за да се одреди до кои глобални држави може да се стигне со дистрибуиран систем кој се состои од одреден број локални субјекти кои комуницирале со размена на пораки.

Преглед

Анализата за достапност или опфатност е воведена во труд од 1978 година за анализа и верификација на протоколите за комуникација.^[1]. Овој труд бил инспириран од труд од Бартлет од 1968 година^[2] кој го претставил протоколот за наизменична бит со користење на моделирање на конечна состојба на субјектите на протоколот и исто така истакна дека сличен протокол опишан претходно имал недостаток на дизајнот. Овој протокол припаѓа на Link layer и според одредени претпоставки, обезбедува како услуга правилна испорака на податоци без загуба или удвојување, и покрај повременото присуство на оштетување или губење на пораката.

За анализа на достапност, локалните субјекти се моделираат според нивните состојби и транзиции. Ентитетот ја менува состојбата кога испраќа порака, троши примена порака или извршува интеракција на неговиот интерфејс за локални услуги. Глобалната држава ${\displaystyle s=(s_{1},s_{2},...,s_{n},medium)}$ на систем со n ентитети ^[3] го одредуваат државите ${\displaystyle s_{i}}$ (i = 1,...n) на ентитетите и состојбата на комуникацијата ${\displaystyle medium}$.Во наједноставниот случај, медиумот помеѓу два ентитета е моделиран од две редици на FIFO во спротивни насоки, кои ги содржат пораките во транзит (кои се испраќаат, но сè уште не се потрошени). Анализата за достигнување го разгледува можното однесување на дистрибуираниот систем со анализа на сите можни низи на состојби на транзиции на ентитетите, а соодветните глобални состојби достигнаа ^[4]

Резултатот од анализата на достапност е глобален график на државна транзиција (исто така наречен графикон на достапност) кој ги прикажува сите глобални состојби на дистрибуираниот систем кои се достапни од почетната глобална состојба и сите можни низи на интеракција на испраќање, консумирање и услуга извршени од субјекти. Меѓутоа, во многу случаи, овој график на транзиција е неограничен и не може да се истражи целосно. Графиконот за преод може да се користи за проверка на општите недостатоци на протоколот во дизајнот (види подолу), но исто така и за проверка дали низите на интеракции на услугите од страна на субјектите одговараат на барањата дадени со глобалната спецификација на услугата на системот.^[1]

Пример

Дијаграмот прикажува два протоколни ентитети и пораките разменети меѓу нив.

Дијаграмот прикажува две машини со конечна состојба што го дефинираат динамичкото однесување на соодветните субјекти на протоколот.

Овој дијаграм прикажува модел на државна машина на глобалниот систем кој се состои од два протоколни ентитети и два канали FIFO што се користат за размена на пораки меѓу нив.

Како пример, го разгледуваме системот на два протоколни ентитети кои ги разменуваат пораките ma, mb, mc и md едни со други, како што е прикажано на првиот дијаграм. Протоколот е дефиниран со однесувањето на двата ентитета, што е дадено на вториот дијаграм во форма на две државни машини. Тука симболот "!" значи испраќање порака и „?“ значи трошење на примена порака. Првичните состојби се државите "1".

Третиот дијаграм го покажува резултатот од анализата за достапност на овој протокол во форма на глобална државна машина. Секоја глобална држава има четири компоненти: состојба на протоколскиот ентитет А (лево), состојбата на ентитетот Б (десно) и пораките во транзит во средината (горниот дел: од А до Б; долниот дел: од Б до А ) Секоја транзиција на оваа глобална машинска состојба одговара на една транзиција на протоколскиот ентитет А или ентитетот Б. Почетната состојба е [1, - -, 1] (нема пораки во транзит).

Се гледа дека овој пример има ограничен глобален државен простор - максималниот број на пораки што можат да бидат во транзит истовремено е две. Овој протокол има глобален ќор-сокак, што е држава [2, - -, 3]. Ако се отстрани преминот на А во состојба 2 за конзумирање порака mb, ќе има неодреден прием во глобалните држави [2, ма mb, 3] и [2, - mb, 3].

Пренос на порака

Дизајнот на протокол треба да се прилагоди на својствата на основниот медиум за комуникација, на можноста партнерот за комуникација да не успее и на механизмот што го користи субјектот за да ја избере следната порака за потрошувачка. Комуникацискиот медиум за протоколите на ниво на врската нормално не е сигурен и овозможува погрешен прием и губење порака (моделиран како состојба на транзиција на медиумот). Протоколите што користат Интернет-IP услуга исто така треба да се занимаваат со можноста за испорака надвор од нарачката. Протоколите на повисоко ниво вообичаено користат услуга за транспорт насочена кон сесија што значи дека медиумот обезбедува сигурен пренос на пораки од FIFO помеѓу кој било пар ентитети. Меѓутоа, при анализата на дистрибуираните алгоритми, честопати се зема предвид можноста некој субјект целосно да не успее, што нормално се открива (како губење на порака во медиумот) со механизам за тајмаут кога не пристигнува очекуваната порака.

Направени се различни претпоставки за тоа дали субјектот може да избере одредена порака за потрошувачка кога пристигнале неколку пораки и се подготвени за потрошувачка. Основни модели се следниве:

• Ред за единечен влез: Секој ентитет има единствена редица FIFO каде што се зачувуваат дојдовните пораки сè додека не се потрошат. Тука субјектот нема моќ за избор и треба да ја потроши првата порака во редот.

• Повеќе редови: Секој субјект има повеќе редови на FIFO, по една за секој партнер што комуницира. Тука субјектот има можност да одлучи, во зависност од неговата состојба, од која редица (или редици) треба да се потроши следната влезна порака.

• Базен за прием: Секој субјект има единствен базен каде што се чуваат примените пораки сè додека не се потрошат. Тука субјектот има моќ да одлучи, во зависност од неговата состојба, кој тип на порака треба да се потроши следно (и да чека порака ако сè уште не е примена), или евентуално да консумира една од множеството типови пораки (со цел да се занимаваат со алтернативи).

Оригиналниот труд со кој се идентификуваше проблемот со неодредени приеми^[5] и поголемиот дел од последователната работа, претпоставуваше единствена влезна редица ^[6] . Понекогаш, неодредените приеми се воведуваат со услов за трка, што значи дека се добиваат две пораки и не е дефиниран нивниот редослед (што често се случува ако доаѓаат од различни партнери). Многу од овие недостатоци во дизајнот исчезнуваат кога се користат повеќе редици или базени за прием^[7] . Со систематско користење на базени за прием, анализата на достапноста треба да провери дали има делумни ќор-сокаци и пораки што остануваат засекогаш во базенот (без да бидат потрошени од субјектот) ^[8]

Практични прашања

Повеќето работи за моделирање на протоколи користат машини со конечна состојба (FSM) за моделирање на однесувањето на дистрибуираните ентитети (видете исто така Комуницирање машини со конечна состојба ). Сепак, овој модел не е доволно моќен за моделирање на параметрите на пораката и локалните променливи. Затоа, често се користат таканаречени проширени модели на FSM, како што се поддржани од јазици како што се машини за SDL или UML . За жал, анализата за достапност станува многу посложена за ваквите модели.

Практично прашање на анализа на достапност е таканаречената „државна експлозија на вселената“. Ако двата ентитета на протоколот имаат по 100 состојби, а медиумот може да вклучува 10 типа на пораки, до две во секоја насока, тогаш бројот на глобални состојби во графиконот за достапност е врзан за бројот 100 x 100 x (10 x 10) x (10 x 10) што е 100 милиони. Затоа, развиени се бројни алатки за автоматско извршување на анализа на достапност и проверка на моделот на графиконот за достапност. Споменуваме само два примери: Проверувачот на моделот СПИН и полето со алатки за изградба и анализа на дистрибуирани процеси .

Наводи

1. Bochmann, G.v. „Finite State Description of Communication Protocols, Computer Networks, Vol. 2 (1978), pp. 361-372“.
2. K.A. Bartlett, R.A. Scantlebury and P.T. Wilkinson, A note on reliable full-duplex transmission over half- duplex links, C.ACM 12, 260 (1969).
3. Note: In the case of protocol analysis, there are normally only two entities.
4. Note: The corruption or loss of a message is modeled as a state transition of the ${\displaystyle medium}$.
5. P. Zafiropulo, C. West, H. Rudin, D. Cowan, D. Brand : Towards analyzing and synthesizing protocols, IEEE Transactions on Communications ( Volume: 28, Issue: 4, Apr 1980 )
6. Note: The SAVE construct of SDL can be used to indicate that certain types of messages should not be consumed in the current state, but saved for future processing.
7. M.F. Al-hammouri and G.v. Bochmann : Realizability of service specifications, Proc. System Analysis and Modelling (SAM) conference 2018, Copenhagen, LNCS, Springer
8. C. Fournet, T. Hoare, S. K. Rajamani, and J. Rehof : Stuck-free Conformance, Proc. 16th Intl. Conf. on Computer Aided Verification (CAV’04), LNCS, vol. 3114, Springer, 2004

Библиографија

• Протоколи за комуникација
• Eraералд Холцман: Дизајн и валидација на компјутерски протоколи, Прентис Хол, 1991 година.
• G.v. Bochmann, D. Rayner and C.H. West: Some notes on the history of protocol engineering, Весник за компјутерски мрежи, 54 (2010), стр. 3197–3209.