Säkerhets- och livskraftsegenskaper

Egenskaper för en exekvering av ett datorprogram - särskilt för samtidiga och distribuerade system - har länge formulerats genom att ge säkerhetsegenskaper ("dåliga saker händer inte") och livlighetsegenskaper ("bra saker händer").

Ett enkelt exempel kommer att illustrera säkerhet och livlighet. Ett program är helt korrekt med avseende på ett previllkor $P$ och postcondition $Q$ om någon exekvering som startas i ett tillstånd som uppfyller $P$ slutar i ett tillstånd som uppfyller $Q$ . Total korrekthet är en konjunktion av en säkerhetsegenskap och en livlighetsegenskap:

Säkerhetsegenskapen förbjuder dessa "dåliga saker": körningar som börjar i ett tillstånd som uppfyller $P$ och avslutas i ett slutligt tillstånd som inte uppfyller $Q$ . För ett program $C$ skrivs denna säkerhetsegenskap vanligtvis med Hoare-trippel $\{P\}C\{Q\}$ .
Liveness-egenskapen, det "bra", är att exekveringen som börjar i ett tillstånd som uppfyller $P$ avslutas.

Observera att en dålig sak är diskret, eftersom det händer på en viss plats under utförandet. En "bra sak" behöver inte vara diskret, men uppsägningens livlighetsegenskap är diskret.

Formella definitioner som slutligen föreslogs för säkerhetsegenskaper och livskraftsegenskaper visade att denna nedbrytning inte bara är intuitivt tilltalande utan också är fullständig: alla egenskaper hos en utförande är en förening av säkerhets- och livskraftsegenskaper. Dessutom kan det vara till hjälp att genomföra nedbrytningen, eftersom de formella definitionerna möjliggör ett bevis på att olika metoder måste användas för att verifiera säkerhetsegenskaper jämfört med för att verifiera livskraftsegenskaper.

Säkerhet

En säkerhetsegendom förbjuder att diskreta dåliga saker inträffar under en avrättning. En säkerhetsegenskap kännetecknar alltså vad som är tillåtet genom att ange vad som är förbjudet. Kravet på att det dåliga ska vara diskret innebär att en dålig sak som inträffar under utförande nödvändigtvis inträffar vid någon identifierbar punkt.

Exempel på en diskret dålig sak som kan användas för att definiera en säkerhetsegenskap inkluderar:

En exekvering som startar i ett tillstånd som uppfyller ett givet förutsättningsvillkor avslutas, men det slutliga tillståndet uppfyller inte det erforderliga eftervillkoret;
En exekvering av två samtidiga processer, där programräknare för båda processerna anger satser inom en kritisk sektion ;
En exekvering av två samtidiga processer där varje process väntar på att en annan ska ändra tillstånd (känd som dödläge ).

En exekvering av ett program kan beskrivas formellt genom att ge den oändliga sekvensen av programtillstånd som uppstår när exekveringen fortskrider, där det sista tillståndet för ett avslutande program upprepas i oändlighet. För ett program av intresse, låt $S$ beteckna uppsättningen av möjliga programtillstånd, $S^{*}$ beteckna uppsättningen av ändliga sekvenser av programtillstånd, och $S^ {\omega }$ betecknar uppsättningen av oändliga sekvenser av programtillstånd. Relationen $\sigma \leq \tau$ gäller för sekvenserna $\sigma$ och $\tau$ iff $\sigma$ är ett prefix för $\ tau$ eller $\sigma$ är lika med $\tau$ .

En egenskap hos ett program är uppsättningen av tillåtna körningar.

Det väsentliga kännetecknet för en säkerhetsegenskap ${\displaystyle SP} är$ $SP$ Om någon exekvering $\sigma$ inte uppfyller så inträffar den avgörande dåliga saken för den säkerhetsegenskapen någon gång $\sigma$ . Lägg märke till att efter en så dålig sak , om ytterligare exekvering resulterar i en exekvering $\sigma ^{\prime }$ , så uppfyller ${\displaystyle \sigma ^{\prime }} inte heller$ $SP$ , eftersom det dåliga i $\sigma$ också förekommer i $\sigma ^{\prime }$ . Vi tar den här slutsatsen om dåliga sakers oförutsägbarhet som den definierande egenskapen för $SP$ som en säkerhetsegenskap. Att formalisera detta i predikatlogik ger en formell definition för att $\displaystyle SP}$ är en säkerhetsegenskap.

\forall \sigma \in S}^{\sigma \in S}^{\ notin SP\implicerar (\exists \beta \leq \sigma :(\forall \tau \in S^{\omega }:\beta \tau \notin SP))

Denna formella definition för säkerhetsegenskaper innebär att om en exekvering $\sigma$ uppfyller en säkerhetsegenskap $SP$ så uppfyller varje prefix för $\sigma$ (med det senaste tillståndet upprepat) $SP$ .

Livlighet

En livlighetsfastighet föreskriver goda saker för varje avrättning eller beskriver på motsvarande sätt något som måste ske under en avrättning. Det goda behöver inte vara diskret – det kan innebära ett oändligt antal steg. Exempel på en bra sak som används för att definiera en livlighetsegenskap inkluderar:

Avslutande av en avrättning som påbörjas i lämpligt tillstånd;
Icke-avslutande av en exekvering som startas i lämpligt tillstånd;
Garanterat eventuellt tillträde till en kritisk sektion när inträde görs;
Rättvis tillgång till en resurs i närvaro av tvister.

Det som är bra i det första exemplet är diskret men inte i de andra.

Att producera ett svar inom en specificerad realtidsgräns är en säkerhetsegenskap snarare än en livlighetsegenskap. Detta beror på att en diskret dålig sak förbjuds: en partiell exekvering som når ett tillstånd där svaret fortfarande inte har producerats och värdet på klockan (en tillståndsvariabel) bryter mot gränsen. Dödlägesfrihet är en säkerhetsegenskap: det "dåliga" är ett dödläge (som är diskret).

För det mesta är det inte tillfredsställande att veta att ett program så småningom gör någonting "bra"; vi vill veta att programmet utför det "bra" inom ett visst antal steg eller innan någon deadline. En egenskap som ger en specifik bunden till "det goda" är en säkerhetsegenskap (som nämnts ovan), medan den svagare egenskapen som bara hävdar att bunden existerar är en livlighetsegenskap. Att bevisa en sådan livlighetsegenskap är sannolikt lättare än att bevisa den snävare säkerhetsegenskapen eftersom bevisningen av livlighetsegenskapen inte kräver den typ av detaljerad redovisning som krävs för att bevisa säkerhetsegenskapen.

För att skilja sig från en säkerhetsegenskap kan inte en livlighetsegenskap $LP$ utesluta något ändligt prefix $\alpha \in S^{*}$ en exekvering (eftersom en sådan ${\ displaystyle \alpha }$ skulle vara en "dålig sak" och skulle därmed definiera en säkerhetsegenskap). Det leder till att en livlighetsegenskap ${\displaystyle LP} definieras$ som en egenskap som inte utesluter något ändligt prefix

\forall \alpha \in S^{*}:(\exists \tau \in S^{\omega }:\alpha \tau \i LP)

Denna definition begränsar inte en bra sak till att vara diskret – det goda kan involvera hela ${\displaystyle \tau } ,$ vilket är en oändlig längd exekvering.

Historia

Lamport använde termerna säkerhetsegenskap och livlighetsegenskap i sin uppsats från 1977 om att bevisa riktigheten av multiprocess (samtidiga) program . Han lånade termerna från Petri-nätteorin , som använde termerna livlighet och begränsning för att beskriva hur tilldelningen av ett Petri-näts "tokens" till dess "platser" kunde utvecklas; Petrinätsäkerhet var en specifik form av begränsning . Lamport utvecklade därefter en formell definition av säkerhet för en NATO-kortkurs om distribuerade system i München. Det antog att egenskaper är oföränderliga under stamning . Den formella definitionen av säkerhet som ges ovan finns i en artikel av Alpern och Schneider; sambandet mellan de två formaliseringarna av säkerhetsegenskaper framgår av en artikel av Alpern, Demers och Schneider.

Alpern och Schneider ger den formella definitionen av livlighet, åtföljd av ett bevis på att alla fastigheter kan konstrueras med hjälp av säkerhetsegenskaper och livlighetsegenskaper. Det beviset var inspirerat av Gordon Plotkins insikt att säkerhetsegenskaper motsvarar slutna mängder och livlighetsegenskaper motsvarar täta mängder i en naturlig topologi på mängden $S^{\omega }$ av oändliga sekvenser av programtillstånd. Därefter gav Alpern och Schneider inte bara en Büchi-automatkarakterisering för de formella definitionerna av säkerhetsegenskaper och livskraftsegenskaper utan använde dessa automatformuleringar för att visa att verifiering av säkerhetsegenskaper skulle kräva en invariant och verifiering av livskraftsegenskaper skulle kräva ett välgrundat argument. . Överensstämmelsen mellan typen av egendom (säkerhet vs livlighet) med typ av bevis (invarians vs välgrundad) var ett starkt argument för att nedbrytningen av egenskaper till säkerhet och livlighet (i motsats till någon annan uppdelning) var en användbar sådan - att veta vilken typ av egendom som skulle bevisas dikterade vilken typ av bevis som krävs.