Nåbarhetsanalys

Nåbarhetsanalys är en lösning på nåbarhetsproblemet i det speciella sammanhanget för distribuerade system. Det används för att bestämma vilka globala stater som kan nås av ett distribuerat system som består av ett visst antal lokala enheter som kommunicerade genom utbyte av meddelanden.

Översikt

Tillgänglighetsanalys introducerades i ett dokument från 1978 för analys och verifiering av kommunikationsprotokoll . Detta papper har inspirerats av ett papper av Bartlett et al. från 1968 som presenterade det alternerande bitprotokollet med användning av finita-tillståndsmodellering av protokollenheterna, och påpekade också att ett liknande protokoll som beskrivits tidigare hade ett designfel. Detta protokoll tillhör länklagret och tillhandahåller, under vissa antaganden, som tjänst korrekt dataleverans utan förlust eller duplicering, trots att meddelanden ibland är korrupta eller förluster.

För nåbarhetsanalys modelleras de lokala enheterna av deras tillstånd och övergångar. En enhet ändrar tillstånd när den skickar ett meddelande, konsumerar ett mottaget meddelande eller utför en interaktion vid sitt lokala tjänstgränssnitt. Det globala tillståndet för ett system med n enheter bestäms av tillstånden (i=1, ... n) för enheterna och tillståndet för kommunikationen . I det enklaste fallet modelleras mediet mellan två enheter av två FIFO-köer i motsatta riktningar, som innehåller meddelanden på väg (som skickas, men som ännu inte förbrukats). Tillgänglighetsanalys tar hänsyn till det distribuerade systemets möjliga beteende genom att analysera alla möjliga sekvenser av tillståndsövergångar för enheterna och motsvarande globala tillstånd som uppnåtts.

Resultatet av nåbarhetsanalys är en global tillståndsövergångsgraf (även kallad nåbarhetsgraf) som visar alla globala tillstånd i det distribuerade systemet som är nåbara från det initiala globala tillståndet, och alla möjliga sekvenser av sändnings-, konsumtions- och serviceinteraktioner utförda av den lokala enheter. Men i många fall är denna övergångsgraf obegränsad och kan inte utforskas helt. Övergångsdiagrammet kan användas för att kontrollera allmänna konstruktionsbrister hos protokollet (se nedan), men också för att verifiera att sekvenserna av tjänsteinteraktioner av enheterna motsvarar de krav som ställs av den globala tjänstespecifikationen för systemet.

Protokollegenskaper

Begränsadhet: Den globala tillståndsövergångsgrafen är begränsad om antalet meddelanden som kan vara på väg är begränsat och antalet tillstånd för alla entiteter är begränsat. Frågan om antalet meddelanden förblir begränsat i fallet med finita tillståndsenheter är i allmänhet inte avgörbar . Man trunkerar vanligtvis utforskningen av övergångsgrafen när antalet meddelanden i transit når en given tröskel.

Följande är designfel:

  • Globalt dödläge: Systemet är i ett globalt dödläge om alla enheter väntar på konsumtion av ett meddelande och inget meddelande är på väg. Frånvaron av globala dödlägen kan verifieras genom att kontrollera att inget tillstånd i nåbarhetsdiagrammet är ett globalt dödläge.
  • Partiellt låst läge: En enhet är i låst läge om den väntar på konsumtion av ett meddelande och systemet är i ett globalt tillstånd där ett sådant meddelande inte är på väg och aldrig kommer att skickas i något globalt läge som kan nås i framtida. En sådan icke-lokal egenskap kan verifieras genom att utföra modellkontroll på nåbarhetsgrafen.
  • Ospecificerad mottagning: En enhet har en ospecificerad mottagning om nästa meddelande som ska konsumeras inte förväntas av entitetens beteendespecifikation i dess nuvarande tillstånd. Frånvaron av detta villkor kan verifieras genom att kontrollera alla tillstånd i nåbarhetsdiagrammet.

Ett exempel

Diagrammet visar två protokollenheter och de meddelanden som utbyts mellan dem.
Diagrammet visar två finita tillståndsmaskiner som definierar det dynamiska beteendet för respektive protokollentiteter.
Detta diagram visar en tillståndsmaskinmodell av det globala systemet som består av de två protokollenheterna och två FIFO-kanaler som används för utbyte av meddelanden mellan dem.

Som ett exempel betraktar vi systemet med två protokollenheter som utbyter meddelanden ma , mb , mc och md med varandra, som visas i det första diagrammet. Protokollet definieras av beteendet hos de två enheterna, vilket ges i det andra diagrammet i form av två tillståndsmaskiner. Här symbolen "!" betyder att skicka ett meddelande och "?" innebär att konsumera ett mottaget meddelande. De initiala tillstånden är tillstånden "1".

Det tredje diagrammet visar resultatet av nåbarhetsanalysen för detta protokoll i form av en global tillståndsmaskin. Varje global stat har fyra komponenter: tillståndet för protokollentitet A (vänster), tillståndet för entitet B (höger) och meddelanden på väg i mitten (övre delen: från A till B; nedre delen: från B till A ). Varje övergång av denna globala tillståndsmaskin motsvarar en övergång av protokollentitet A eller entitet B. Det initiala tillståndet är [1, - - , 1] (inga meddelanden pågår).

Man ser att detta exempel har ett avgränsat globalt tillståndsutrymme - det maximala antalet meddelanden som kan vara på väg samtidigt är två. Detta protokoll har ett globalt dödläge, vilket är tillståndet [2, - - , 3]. Om man tar bort övergången av A i tillstånd 2 för att konsumera meddelande mb kommer det att bli en ospecificerad mottagning i de globala tillstånden [2, ma mb ,3] och [2, - mb ,3].

Meddelandeöverföring

Utformningen av ett protokoll måste anpassas till egenskaperna hos det underliggande kommunikationsmediet, till möjligheten att kommunikationspartnern misslyckas och till den mekanism som används av en enhet för att välja nästa meddelande för konsumtion. Kommunikationsmediet för protokoll på länknivån är normalt inte tillförlitligt och tillåter felaktig mottagning och meddelandeförlust (modellerad som en tillståndsövergång för mediet). Protokoll som använder IP-tjänsten på Internet bör också hantera möjligheten till leverans i urdrift. Protokoll på högre nivå använder normalt en sessionsorienterad transporttjänst, vilket innebär att mediet tillhandahåller tillförlitlig FIFO-överföring av meddelanden mellan valfritt par av enheter. Men i analysen av distribuerade algoritmer tar man ofta hänsyn till möjligheten att någon enhet misslyckas helt, vilket normalt detekteras (som en förlust av meddelande i mediet) av en timeout -mekanism när ett förväntat meddelande inte kommer fram.

Olika antaganden har gjorts om huruvida en enhet kan välja ett visst meddelande för konsumtion när flera meddelanden har kommit in och är redo för konsumtion. Grundmodellerna är följande:

  • Enkel ingångskö: Varje enhet har en enda FIFO-kö där inkommande meddelanden lagras tills de förbrukas. Här har enheten ingen valkraft och måste konsumera det första meddelandet i kön.
  • Flera köer: Varje enhet har flera FIFO-köer, en för varje kommunicerande partner. Här har enheten möjlighet att bestämma, beroende på dess tillstånd, från vilken kö (eller köer) nästa ingångsmeddelande ska konsumeras.
  • Mottagningspool: Varje enhet har en enda pool där mottagna meddelanden lagras tills de förbrukas. Här har enheten befogenhet att, beroende på dess tillstånd, bestämma vilken typ av meddelande som ska konsumeras härnäst (och vänta på ett meddelande om inget har tagits emot ännu), eller eventuellt konsumera ett från en uppsättning meddelandetyper (för att ta itu med alternativ).

Det ursprungliga papper som identifierade problemet med ospecificerade mottagningar, och mycket av det efterföljande arbetet, antog en enda ingångskö. Ibland introduceras ospecificerade mottagningar av ett rasvillkor , vilket innebär att två meddelanden tas emot och deras ordning inte definieras (vilket ofta är fallet om de kommer från olika partners). Många av dessa designfel försvinner när flera köer eller mottagningspooler används. Med systematisk användning av mottagningspooler bör nåbarhetsanalys kontrollera om det finns partiella låsningar och meddelanden som för alltid finns kvar i poolen (utan att konsumeras av enheten)

Praktiska frågor

Det mesta av arbetet med protokollmodellering använder finita-tillståndsmaskiner (FSM) för att modellera beteendet hos de distribuerade enheterna (se även Kommunicera finita-tillståndsmaskiner ) . Denna modell är dock inte tillräckligt kraftfull för att modellera meddelandeparametrar och lokala variabler. Därför används ofta så kallade utökade FSM-modeller, som till exempel stöds av språk som SDL- eller UML-tillståndsmaskiner . Tyvärr blir nåbarhetsanalys mycket mer komplex för sådana modeller.

En praktisk fråga för nåbarhetsanalys är den så kallade "tillståndsrymdexplosionen". Om de två enheterna i ett protokoll har 100 tillstånd vardera och mediet kan innehålla 10 typer av meddelanden, upp till två i varje riktning, är antalet globala tillstånd i nåbarhetsgrafen bundet av talet 100 x 100 x (10 x 10) x (10 x 10) vilket är 100 miljoner. Därför har ett antal verktyg utvecklats för att automatiskt utföra nåbarhetsanalys och modellkontroll på nåbarhetsgrafen. Vi nämner bara två exempel: SPIN-modellkontrollen och en verktygslåda för konstruktion och analys av distribuerade processer .

Vidare läsning

Referenser och anteckningar

Hämtad från " https://en.wikipedia.org/w/index.php?title=Reachability_analysis&oldid=1071747198 "