Säkerhetsegenskaper

Säkerhetsegenskaper är en klass av egenskaper hos ett system som säger att oönskade tillstånd eller händelser aldrig inträffar under en körning. De står i kontrast till livslängdsegenskaper (liveness), som handlar om att systemet fortsätter att göra framsteg över tiden. Tillsammans används de ofta i formella metoder och systemdesign för att beskriva vad som får ske och vad som måste undvikas.

Formellt definieras en säkerhetsegenskap ofta som en invariant eller ett krav som begränsar vilka sekvenser av tillstånd som är tillåtna. En central insikt är att en säkerhetsegenskap bryts av ett ändligt dåligt prefix – en kort körning där ett felaktigt tillstånd uppstår, varefter egenskapen inte längre hålls.

Exempel på säkerhetsegenskaper är att ett system aldrig får tillåta tillgång till en kritisk resurs utan korrekt synkronisering (ömsesidig uteslutning), att en variabel alltid ligger inom ett visst intervall, eller att kommunikationen inte förväxlar meddelanden. Dessa egenskaper kan verifieras genom invarianter, assertionskontroll och modellkontroll (ofte kallat modellbaserad verifiering).

Användningsområden inkluderar programvaru- och hårdvarudesign, säkerhet och tillförlitlighet i kritiska system samt realtidssäkerhet. Verifikationsmetoderna kräver ofta exakt modell av beteendet; säkerhetsegenskaper kan kombineras med livslängdsegenskaper där systemet både ska undvika dåliga tillstånd och säkerställa progression över tid. Begränsningar inkluderar att arbete med abstraktioner och att vissa egenskaper är svåra att isolera i praktiken.