Linjär tidsegenskap

Inom modellkontroll , en gren av datavetenskap , används linjära tidsegenskaper för att beskriva kraven på en modell av ett datorsystem . Exempel på egenskaper inkluderar "varuautomaten serverar inte en drink förrän pengar har matats in" (en säkerhetsegenskap ) eller "datorprogrammet avslutas så småningom" (en livlighetsegenskap ). Rättvisa egenskaper kan användas för att utesluta orealistiska vägar för en modell. Till exempel, i en modell av två trafikljus, kan livlighetsegenskapen "båda trafikljusen är gröna oändligt ofta" bara vara sann under den ovillkorliga rättvisa begränsningen "varje trafikljus ändrar färg oändligt ofta" (för att utesluta fallet där ett trafikljus är "oändligt mycket snabbare" än den andra).

Formellt är en linjär tidsegenskap ett ω-språk över kraftmängden av "atomära propositioner". Det vill säga, egenskapen innehåller sekvenser av uppsättningar av propositioner, varje sekvens känd som ett "ord". Varje egenskap kan skrivas om som " P och Q förekommer båda" för vissa säkerhetsegenskapen P och livlighetsegenskapen Q . En invariant för ett system är något som är sant eller falskt för ett visst tillstånd. Invarianta egenskaper beskriver en invariant som varje nåbart tillstånd i en modell måste uppfylla, medan persistensegenskaper är av formen "till sist för alltid några invarianta".

Temporal logik som linjär temporal logik beskriver typer av linjära tidsegenskaper med hjälp av formler.

Den här artikeln handlar om propositionella linjärtidsegenskaper och kan inte hantera predikat om programtillstånd, så den kan inte definiera en egenskap som: det aktuella värdet på y bestämmer antalet gånger som x växlar mellan 0 och 1 före avslutning. Den mer allmänna formalismen som används i Säkerhets- och livlighetsegenskaper kan hantera detta.

Definition

Låt AP vara en uppsättning atomära propositioner. Ett ord över $2^{AP}$ ( potensmängden för AP ) är en oändlig sekvens av uppsättningar av propositioner, såsom ${\displaystyle w:=\{a\}\{a,b\}\emptyset \{a,b\}^{\omega }} (för atompropositionerna A$ P $displaystyle AP=\{a,b\}}$ ). En linjär tidsegenskap (LT) över AP är en delmängd av $(2^{AP})^{\omega }$ dvs en uppsättning ord. Ett exempel på en LT-egenskap över mängden $\{a,b\}$ är "uppsättningen ord som innehåller en oändligt ofta". Ordet w finns i denna mängd, eftersom a finns i $\{a,b\}$ , vilket förekommer oändligt ofta. Ett ord som inte ingår i denna uppsättning är ${\displaystyle x:=\{a\}(\{b\}\emptyset )^{\omega }} ,$ som en enda inträffar en gång (i den första uppsättningen).

En LT-egenskap är ett ω-språk över alfabetet $\Sigma =2^{AP}$ (och vice versa).

Vi betecknar med pref ( w ) de ändliga prefixen för w (dvs $\{\{a \},\{a\}\{a,b\},\{a\}\{a,b\}\emptyset ,...\}$ i ovanstående fall). Stängningen av en LT-egenskap P är:

closure(P):=\{\ sigma \in (2^{AP})^{\omega }\mid pref(\sigma )\subseteq pref(P)\}

Ansökningar

En Kripke-struktur över

\{p,q\}

. Den uppfyller inte LT-egenskapen "oändligt ofta q ", på grund av sökvägen

s_{1}s_{2}s_{3}^{\omega }

. Den uppfyller egenskapen "oändligt ofta p ", eftersom alla möjliga sökvägar anger

s_{1}

eller

s_{3}

oändligt ofta.

Med hjälp av teorin om finita-tillståndsmaskiner kan ett program eller datorsystem modelleras av en Kripke-struktur . LT-egenskaper beskriver sedan restriktioner för spåren (utgångarna) av en Kripke-struktur. Till exempel, om två trafikljus vid en korsning representeras av en Kripke-struktur kan atomförslagen vara de möjliga färgerna för varje ljus och det kan vara önskvärt att spåren uppfyller LT-egenskapen "trafikljusen kan inte båda vara gröna vid samtidigt" (för att undvika bilkollisioner).

Om varje spår av Kripke-strukturen TS är ett spår av TS ' så uppfylls varje LT-egenskap som TS ' uppfyller av TS . Detta är användbart vid modellkontroll för att tillåta abstraktion: om en förenklad modell av systemet uppfyller en LT-egenskap kommer den faktiska modellen av systemet också att uppfylla den.

Klassificering av linjära tidsegenskaper

Säkerhetsegenskaper

En säkerhetsegendom är informellt av formen "en dålig sak händer inte". Till exempel, om ett system modellerar en automat (ATM) är en sådan egenskap "pengar ska inte lämnas ut om inte en PIN-kod har angetts". Formellt är en säkerhetsegenskap en LT-egenskap så att varje ord som bryter mot egenskapen har ett "dåligt prefix", för vilket inget ord med det prefixet uppfyller egenskapen. Det är,

\forall \sigma \}in (2^{ )^{\omega }\setminus P\ \exists {\text{ ett ändligt prefix}}\ {\hat {\sigma }}:P\cap \{\sigma '\mid {\hat {\sigma }}\ {\text{är ett prefix till}}\ \sigma '\}=\emptyset

I ATM-exemplet är ett minimalt dåligt prefix en ändlig uppsättning steg som utförs där pengar utmatas i det sista steget och en PIN-kod inte matas in i något steg. För att verifiera en säkerhetsegenskap är det tillräckligt att endast beakta de ändliga spåren av en Kripke-struktur och kontrollera om något sådant spår är ett dåligt prefix.

En LT-egenskap P är en säkerhetsegenskap om och endast om $closure(P)=P$ .

Invarianta egenskaper

En invariant egenskap är en typ av säkerhetsegenskap där tillståndet endast avser det aktuella tillståndet. Till exempel är ATM-exemplet inte en invariant eftersom vi inte kan avgöra om egenskapen kränks genom att se att det aktuella tillståndet är "dispensera pengar", bara genom att se att det nuvarande tillståndet är "dispensera pengar" och inget tidigare tillstånd "läses" STIFT". Ett exempel på en invariant är trafikljusvillkoret "trafikljusen kan inte båda vara gröna samtidigt" ovan. En annan är "variabeln x är aldrig negativ", i en modell av ett datorprogram.

Formellt är en invariant av formen:

P=\{A_{0}A_{1}....\in (2^{AP})^{\omega }\mid \forall j\in \mathbb {N} :A_{j}\ {\text{tillfredsställer}}\ \Phi \}

för någon propositionell logisk formel $\Phi$ .

En Kripke-struktur tillfredsställer en invariant om och endast om varje nåbart tillstånd uppfyller invarianten, vilket kan kontrolleras genom en bredd-först-sökning eller djup-först-sökning . Säkerhetsegenskaper kan verifieras induktivt med invarianter.

Livlighetsegenskaper

En livlighetsegenskap är informellt av formen "något gott händer så småningom". Formellt P en livlighetsegenskap om $pref(P)=(2^{AP})^{*}$ dvs vilken ändlig sträng som helst kan fortsätta till ett giltigt spår. Ett exempel på en livlighetsegenskap är den tidigare LT-egenskapen "uppsättningen av ord som innehåller en oändligt ofta". Inget ändligt prefix för ett ord kan bevisa att ordet inte uppfyller denna egenskap, eftersom ordet kan fortsätta att ha oändligt många s .

När det gäller datorprogram inkluderar användbara livskraftsegenskaper "programmet avslutas så småningom" och, vid samtidig beräkning , "måste varje process så småningom betjänas".

Persistensegenskaper

En persistensegenskap är en livlighetsegenskap av formen "till slut för alltid ${\displaystyle \Phi }"$ . Det vill säga en egenskap av formen:

P=\{A_{0}A_{1}...\in (2^{AP}) ^{\omega }\mid \exists N\in \mathbb {N} :\forall n\geq N:A_{n}\ {\text{tillfredsställer}}\ \Phi \}

Förhållandet mellan säkerhet och livskraftsegenskaper

Ingen annan LT-egenskap än $(2^{AP})^{\omega }$ (mängden av alla ord över ${\displaystyle 2^{AP}})$ är både en säkerhet och en livlighetsegenskap. Även om inte varje egenskap är en säkerhetsegenskap eller en livlighetsegenskap (tänk på att " a inträffar exakt en gång"), är varje egenskap skärningspunkten mellan en säkerhet och en livlighetsegenskap.

I topologi kan uppsättningen av alla ord $(2^{AP})^{\omega }$ med måtten :

d(w,x):=\inf\{2^{-|s|}\mid s\in pref(w )\cap pref(x)\}

Då är en säkerhetsegenskap en sluten uppsättning och en livlighetsegenskap är en tät uppsättning .

Rättvisa egenskaper

Rättvisa egenskaper är förutsättningar som ställs på ett system för att utesluta orealistiska spår. Ovillkorlig rättvisa är av formen "varje process får sin tur oändligt ofta". Stark rättvisa är av formen "varje process får sin tur oändligt ofta om den aktiveras oändligt ofta". Svag rättvisa är av formen "varje process får sin tur oändligt ofta om den kontinuerligt aktiveras från en viss punkt".

I vissa system definieras en rättvisa begränsning av en uppsättning tillstånd, och en "rättvis väg" är en som passerar genom något tillstånd i rättvisa begränsningen oändligt ofta. Om det finns flera rättvisa begränsningar måste en rättvis väg passera oändligt ofta genom ett tillstånd per begränsning. Ett program "tillfredsställer någorlunda" en LT-egenskap P med avseende på en uppsättning rättvisa villkor om för varje väg antingen vägen misslyckas med ett rättvisande villkor eller så uppfyller den P . Det vill säga att egenskapen P är uppfylld för alla mässvägar.

En rättvisa egenskap är realiserbar för en Kripke-struktur om varje nåbart tillstånd har en rättvis väg som börjar från det tillståndet. Så länge som en uppsättning rättvisa villkor är realiserbara är de irrelevanta för säkerhetsegenskaper.

Temporal logik

Temporal logik som beräkningsträdlogik (CTL) kan användas för att specificera vissa LT-egenskaper. Alla linjär temporal logik (LTL) är LT-egenskaper. Genom ett räkneargument ser vi att all logik där varje formel är en ändlig sträng inte kan representera alla LT-egenskaper, eftersom det måste finnas oräkneligt många formler men det finns oräkneligt många LT-egenskaper.

Anteckningar

Alpern, B.; Schneider, FB (1987). "Erkänner säkerhet och livlighet". Distribuerad datoranvändning . 2 (3): 117. CiteSeerX 10.1.1.20.5470 . doi : 10.1007/BF01782772 .
Baier, Christel ; Katoen, Joost-Pieter (2008). Principer för modellkontroll . MIT Press. ISBN 9780262026499 .
Clarke, Edmund M. ; Grumberg, Orna ; Kroening, Daniel (2018). Modellkontroll . MIT Press. ISBN 9780262038836 .
D'Silva, Vijay; Kroening, Daniel ; Weissenbacher, Georg (2008). "En undersökning av automatiserade tekniker för formell mjukvaruverifiering". IEEE-transaktioner på datorstödd design av integrerade kretsar och system . 27 (7): 1165–1178.
Finkbeiner, Bernd; Torfah, Hazem (2017). "Tätheten av linjär-tidsegenskaper". Föreläsningsanteckningar i datavetenskap . Automatiserad teknik för verifiering och analys. Vol. 10482. Springer.
Kern, Christoph; Greenstreet, Mark R. (1999). "Formell verifiering i hårdvarudesign: En undersökning". ACM Transactions on Design Automation of Electronic Systems . Föreningen för Datormaskiner. 4 (2). doi : 10.1145/307988.307989 . ISSN 1084-4309 .

Vidare läsning

Emerson, E. Allen (1990). "Tidsmässig och modal logik". Handbok i teoretisk datavetenskap . B .
Pnueli, Amir (1986). "Tillämpningar av tidslogik för specifikation och verifiering av reaktiva system: En undersökning av aktuella trender". Aktuella trender i samtidighet : 510–584.