IV113 Validace a verifikace Ověřování modelu pro Lineární Temporální Logiku Jiří Barnat Motivace Ověřování kvality Testování je neúplné, nedává garanci správnosti. Deduktivní verifikace je drahá. Typický kontext výskytu chyb Neočekávané či krajní vstupy. Interakce komponent. Paralelizmus (nelze testovat). Model Checking – Ověřování modelu Automatizovaný proces verifikace pro ... ... paralelní a distribuované systémy. IV113 Úvod do validace a verifikace: LTL MC str. 2/43 Sekce Verifikace paralelních a reaktivních programů IV113 Úvod do validace a verifikace: LTL MC str. 3/43 Paralelní programy Paralelní kompozice Komponenty souběžně přispívají k transformaci výchozího stavu na cílový. Významová funkce pro paralelně běžící programy vznikne libovolným proložením atomických akcí jednotlivých komponent. (Interleaving.) Nekompozicionalita významových funkcí Významovou funkci paralelního programu nelze získat jako složení významových funkcí jednotlivých komponent. Výsledek může být závislý na proložení akcí. IV113 Úvod do validace a verifikace: LTL MC str. 4/43 Příklad nekompozicionality Příklad Systém: (y=x; y++; x=y) (y=x; y++; x=y) Vstup-výstupní proměnná x Významová funkce obou procesů je λx->x+1. Složení významových funkcí: (λx->x+1)·(λx->x+1). (λx->x+1)·(λx->x+1) 0 = 2 2 konkrétní běhy Stav = (x, y1, y2) (0,-,-) y1=x −→ (0,0,-) y2=x −→ (0,0,0) y1++ −→ x=y1 −→ (1,1,0) y2++ −→ x=y2 −→ (1,1,1) (0,-,-) y1=x −→ (0,0,-) y1++ −→ x=y1 −→ (1,1,-) y2=x −→ (1,1,1) y2++ −→ x=y2 −→ (2,1,2) IV113 Úvod do validace a verifikace: LTL MC str. 5/43 Vlastnosti paralelních programů Pozorování Konkrétní časování událostí souvisejících s interakcí programů je forma vstupu. Paralelní programy jsou svým způsobem reaktivní systémy, neboť nejsou dopředu známa všechna vstupní data. Důsledek U paralelních a reaktivních programů často požadujeme (specifikujeme) chování, která se nedají vyjádřit s použitím vstupních a výstupních podmínek. IV113 Úvod do validace a verifikace: LTL MC str. 6/43 Vlastností paralelních/reaktivních programů Příklady specifikace Události A a B nastanou dříve, než událost C. Uživateli program není dovoleno vložit novou hodnotu vstupu, dokud program přechozí hodnotu nezpracuje. Není pravda, že procedura X bude souběžně vykonávána procesem P i Q (vzájemné vyloučení). Každá akce A vyvolá sekvenci reakcí B,C a D. Formalizace slovního popisu Lze formalizovat pomocí temporálních logik. Amir Pnueli, 1977 IV113 Úvod do validace a verifikace: LTL MC str. 7/43 Dokazování pomocí formulí temporálních logik Pozorování Pro modální logiky je možné vystavět podobné důkazové systémy, jako pro Hoarovu logiku. Tyto důkazové techniky vykazují stejné/podobné nevýhody jako verifikace paralelních programů s využitím vstupních a výstupních podmínek. Model checking Jiná metoda ověření platnosti formule temporální logiky. IV113 Úvod do validace a verifikace: LTL MC str. 8/43 Sekce Ověřování modelu (Model Checking) IV113 Úvod do validace a verifikace: LTL MC str. 9/43 Ověřování modelu Ověřování modelu – přehled Vytvoříme formální model M verifikovaného systému. Specifikaci vyjádříme formulí ϕ zvolené temporální logiky. Rozhodneme, zda M |= ϕ. Tj., zda M je modelem formule ϕ. (Odtud název ověřování modelu.) Volitelné Postranním produktem rozhodnutí může být (případně větvící se) posloupnost stavů, dokládající rozhodnutí. Tato posloupnost se běžně označuje slovem protipříklad (často produkována pouze za účelem ukázání neplatnosti ϕ). Proces rozhodnutí lze pro konečné (a některé nekonečné) modely systému automatizovat. IV113 Úvod do validace a verifikace: LTL MC str. 10/43 Ověřování modelu – schéma Requirements Specification Property Formalization System System Model Model Checking Simulation Counterexample Invalid Valid ErrorModelling IV113 Úvod do validace a verifikace: LTL MC str. 11/43 Automatické nástroje pro ověřování modelu Model-checkery Softwarové nástroje, které pro model systému a temporální vlastnost provedou rozhodnutí o splnění dané vlastnosti modelem. SPIN, UppAll, SMV, Prism, DIVINE . . . Modelovací jazyky Procesy popsány jako rozšířené konečné automaty. Rozšíření umožňuje podmínit provedení přechodu/akce platností boolovského výrazu, případně synchronizací s akcí jiného souběžně běžícího procesu. IV113 Úvod do validace a verifikace: LTL MC str. 12/43 Sekce Modelování a formalizace verifikovaného systému IV113 Úvod do validace a verifikace: LTL MC str. 13/43 Formalizace stavového prostoru – Atomické propozice Připomenutí Na systém lze nahlížet jako na množinu stavů, které se mění vlivem vykonávání akcí programu. Stav = valuace modelovaných proměnných. Atomické propozice Základní tvrzení vyjadřujících se o kvalitách jednotlivých stavů. (Např. max(x, y) ≥ 3, . . .) Platnost atomických propozic musí být algoritmicky rozhodnutelná na základě daného stavu, tj. s využitím valuace modelovaných proměnných. Množina základních o stavu pozorovatelných jevů je ovlivněna mírou abstrakce použitou při modelování systému. IV113 Úvod do validace a verifikace: LTL MC str. 14/43 Formalizace stavového prostoru – Kripkeho struktury Kripkeho struktury Nechť je dána množina atomických propozic AP. Kripkeho struktura je čtveřice (S, T, I, s0), kde S je (konečná) množina stavů, T ⊆ S × S je přechodová relace, I : S → 2AP je interpretace AP. s0 ∈ S je počáteční stav. Kripkeho přechodové systémy Je-li dána množina Act akcí proveditelných programem, je možné Kripkeho struktury rozšířit o označení přechodů. Kripkeho přechodový systém je pětice (S, T, I, s0, L), kde (S, T, I, s0) je Kripkeho struktura, L : T → Act je značkovací funkce. IV113 Úvod do validace a verifikace: LTL MC str. 15/43 Kripkeho struktura – příklad Kripkeho struktura Z Z,K,P Z,K,L Pivo Limo Platba Volba AP={Z – zaplaceno, K – kelímek, L – limo, P – pivo} IV113 Úvod do validace a verifikace: LTL MC str. 16/43 Kripkeho struktura – příklad Kripkeho přechodový systém Z Z,K,P Z,K,L Mince Bere limo Bere pivo Chce pivo Chce limo Pivo Limo Platba Volba AP={Z – zaplaceno, K – kelímek, L – limo, P – pivo} IV113 Úvod do validace a verifikace: LTL MC str. 16/43 Formalizace stavového prostoru – běh systému Běh Maximální (tj. nerozšiřitelný) sled v grafu indukovaného Kripkeho strukturou, počínající v iniciálním stavu Kripkeho struktury. Nechť M = (S, T, I, s0) je Kripkeho struktura. Běh je posloupnost stavů π = s0, s1, s2, . . . taková, že ∀i ∈ N0.(si , si+1) ∈ T. Konečné běhy – úmluva Maximální sled může být konečný: π = s0, s1, s2, . . . , sk, pokud sk+1 ∈ S.(sk, sk+1) ∈ T. Z technických důvodu lze na konečné maximální sledy nahlížet jako na nekonečné běhy, které vzniknou opakováním posledního stavu daného maximálního sledu. Maximální sled s0, . . . , sk se chápe jako běh s0, . . . , sk, sk, sk, . . .. IV113 Úvod do validace a verifikace: LTL MC str. 17/43 Implicitní a explicitní popis systému Pozorování Kripkeho struktura, jež udává konkrétní chování systému, se často nepopisuje výčtem stavů a hran (explicitní forma), ale pouze programem (implicitní forma). Implicitní zápis může být exponenciálně úspornější. Generování stavového prostoru Výpočet explicitní reprezentace z implicitního popisu. Interpretace implicitního zápisu sleduje přesně formálně definovaná pravidla. Praxe Programovací jazyky nemají přesnou sémantiku. Využívají se umělé modelovací jazyky. IV113 Úvod do validace a verifikace: LTL MC str. 18/43 Příklad modelovacího jazyka – DVE Konečný automat Stavy (Lokace) Iniciální stav Přechody (Akceptující stavy) Přechody rozšířené o Stráž Synchronizaci s předáváním hodnot Efekt (přiřazení) Lokální proměnné integer, byte channel p1 p4 p2 p3 x==b b=0,x=0 sync c?x b=b+1 b=b+1 Process B byte b,x; IV113 Úvod do validace a verifikace: LTL MC str. 19/43 Příklad modelu v jazyce DVE channel {byte} c[0]; process A { byte a; state q1,q2,q3; init q1; trans q1→q2 { effect a=a+1; }, q2→q3 { effect a=a+1; }, q3→q1 { sync c!a; effect a=0; }; } process B { byte b,x; state p1,p2,p3,p4; init p1; trans p1→p2 { effect b=b+1; }, p2→p3 { effect b=b+1; }, p3→p4 { sync c?x; }, p4→p1 { guard x==b; effect b=0, x=0; }; } system async; IV113 Úvod do validace a verifikace: LTL MC str. 20/43 Sémantika ukázána simulací State: []; A:[q1, a:0]; B:[p1, b:0, x:0] 0 0.0 : q1 → q2 { effect a = a+1; } 1 1.0 : p1 → p2 { effect b = b+1; } Command:1 ————————————————————— State: []; A:[q1, a:0]; B:[p2, b:1, x:0] 0 0.0 : q1 → q2 { effect a = a+1; } 1 1.1 : p2 → p3 { effect b = b+1; } Command:1 ————————————————————— State: []; A:[q1, a:0]; B:[p3, b:2, x:0] 0 0.0 : q1 → q2 { effect a = a+1; } Command:0 ————————————————————— State: []; A:[q2, a:1]; B:[p3, b:2, x:0] 0 0.1 : q2 → q3 { effect a = a+1; } Command:0 ————————————————————— State: []; A:[q3, a:2]; B:[p3, b:2, x:0] 0 0.2&1.2 : q3 → q1 { sync c!a; effect a = 0; } p3 → p4 { sync c?x; } Command:0 ————————————————————— State: []; A:[q1, a:0]; B:[p4, b:2, x:2] IV113 Úvod do validace a verifikace: LTL MC str. 21/43 Sekce Formalizace vlastností IV113 Úvod do validace a verifikace: LTL MC str. 22/43 Specifikace jako jazyky nekonečných slov Problém Jak se formálně vyjadřovat o kvalitách běhu? Jak mechanicky rozhodovat, že běh má danou kvalitu? Řešení Konečný automat jako mechanický pozorovatel běhu. Běh je nekonečný! Konečné automaty pro jazyky nekonečných slov (ω-regulární jazyky) Büchi akceptační podmínka – automat akceptuje slovo pokud nekonečněkrát projde koncovým stavem. IV113 Úvod do validace a verifikace: LTL MC str. 23/43 Automaty nad nekonečnými slovy Büchi automaty Büchi automat je pětice A = (Σ, S, s, δ, F), kde Σ je konečná abeceda znaků, S je konečná množina stavů, s ∈ S je iniciální stav, δ : S × Σ → 2S je přechodová relace, a F ⊆ S je množina koncových stavů. Jazyk akceptovaný Büchi automatem A Běh ρ automatu A nad nekonečným slovem w = a1a2 . . . je sekvence stavů ρ = s0, s1, . . . taková, že s0 ≡ s a ∀i : si ∈ δ(si−1, ai ). inf (ρ) – množinu stavů, které se v ρ vyskytly nekonečně krát. Běh ρ je akceptující, pokud inf (ρ) ∩ F = ∅. Jazyk akceptovaný automatem A je množina všech slov, pro které existuje akceptující běh. Označujeme L(A). IV113 Úvod do validace a verifikace: LTL MC str. 24/43 Přehlednost zápisu/nákresu Pozorování AP={X,Y,Z}, Hrana označená {X} značí, že platí X a neplatí Y a Z. Pokud je třeba vyjádřit že platí X, neplatí Z a na platnosti Y nezáleží, je třeba vést hrany pod {X} a {X, Y }. Množiny AP jako boolovské formule Jednotlivé hrany mezi dvěma stejnými vrcholy pod různými kombinacemi atomických propozic lze sloučit do jedné hrany ohodnocené boolovskou formulí. Příklad Hrany {X}, {Y}, {X,Y}, {X,Z}, {Y,Z} a {X,Y,Z} lze nahradit jednou hranou ohodnocenou formulí X ∨ Y . Pokud vůbec nezáleží na platnosti při provedení hrany, je možné ji označit štítkem true ≡ X ∨ ¬X. IV113 Úvod do validace a verifikace: LTL MC str. 25/43 Vyjádřete Büchi automatem Systém Prodejní automat Σ = 2{Z,K,L,P}, jeZ = {A ∈ Σ | Z ∈ A}, jeK = {A ∈ Σ | K ∈ A}, . . . Vlastnosti Prodejní automat vydá alespoň jeden kelímek s nápojem. Prodejní automat vydá alespoň jeden kelímek s limonádou. Prodejní automat vydá nekonečně mnoho kelímků. Prodejní automat vydá nekonečně mnoho kelímků s pivem. Prodejní automat nevydá kelímek s nápojem, bez zaplacení. Pokaždé, když zaplatím, dostanu kelímek s nápojem. IV113 Úvod do validace a verifikace: LTL MC str. 26/43 Sekce Lineární temporální logika IV113 Úvod do validace a verifikace: LTL MC str. 27/43 LTL neformálně Formule ϕ Vyhodnocuje se nad jedním během systému. Vyjadřuje se o platnosti atomických propozic ve stavech daného běhu. Temporální operátory LTL F ϕ — (Future) Někde v běhu platí ϕ. G ϕ — (Globally) V daném běhu vždy platí ϕ. ϕ U ψ — (Until) Někde platí ψ a do té doby platí ϕ. X ϕ — (Next) V příštím stavu platí ϕ. ϕ W ψ — (Weak Until) Jako Until ale ψ nemusí nastat. ϕ R ψ — (Release) ψ platí dokud neplatí ϕ ∧ ψ. IV113 Úvod do validace a verifikace: LTL MC str. 28/43 Grafické znázornění sémantiky temporálních operátorů X ϕ : •−→ ϕ •−→•−→•−→•−→• · · · ϕ U ψ : ϕ •−→ ϕ •−→ ϕ •−→ ϕ •−→ ψ •−→• · · · F ϕ : •−→•−→•−→•−→ ϕ •−→• · · · G ϕ : ϕ •−→ ϕ •−→ ϕ •−→ ϕ •−→ ϕ •−→ ϕ • · · · ϕ R ψ : ψ •−→ ψ •−→ ψ •−→ ψ •−→ ϕ∧ψ • −→• · · · or ψ •−→ ψ •−→ ψ •−→ ψ •−→ ψ •−→ ψ • · · · ϕ W ψ : ϕ •−→ ϕ •−→ ϕ •−→ ϕ •−→ ψ •−→• · · · or ϕ •−→ ϕ •−→ ϕ •−→ ϕ •−→ ϕ •−→ ϕ • · · · IV113 Úvod do validace a verifikace: LTL MC str. 29/43 Syntax LTL Nechť AP je množina atomických propozic. Pak Je-li p ∈ AP, pak p je formule. Je-li ϕ formule, pak ¬ϕ je formule. Jsou-li ϕ a ψ formule, pak ϕ ∨ ψ je formule. Je-li ϕ formule, pak X ϕ je formule. Jsou-li ϕ a ψ formule, pak ϕ U ψ je formule. Alternativní zápis ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | X ϕ | ϕ U ϕ IV113 Úvod do validace a verifikace: LTL MC str. 30/43 Syntaktické zkratky Výroková logika ϕ ∧ ψ ≡ ¬(¬ϕ ∨ ¬ψ) ϕ ⇒ ψ ≡ ¬ϕ ∨ ψ ϕ ⇔ ψ ≡ (ϕ ⇒ ψ) ∧ (ψ ⇒ ϕ) Temporální operátory F ϕ ≡ true U ϕ G ϕ ≡ ¬F ¬ϕ ϕ R ψ ≡ ¬(¬ϕ U ¬ψ) ϕ W ψ ≡ ϕ U ψ ∨ G ϕ Alternativní syntax Fϕ ≡ ϕ Gϕ ≡ ϕ Xϕ ≡ ◦ϕ IV113 Úvod do validace a verifikace: LTL MC str. 31/43 Modely formulí LTL Model LTL formule Je dána množina atomických propozic AP. Modelem LTL formule je běh π Kripkeho struktury. Značení Nechť π = s0, s1, s2, . . .. Suffix běhu π počínaje stavem sk budeme značit jako πk = sk, sk+1, sk+2, . . .. K-tý stav běhu π, budeme značit jako π(k) = sk. IV113 Úvod do validace a verifikace: LTL MC str. 32/43 Sémantika LTL Předpoklady Je dána množina atomických propozic AP. Je dán běh π Kripkeho struktury M = (S, T, I, s0). ϕ, ψ jsou syntakticky správné LTL formule. p ∈ AP je atomická propozice. Sémantika π |= p iff p ∈ I(π(0)) π |= ¬ϕ iff π |= ϕ π |= ϕ ∨ ψ iff π |= ϕ or π |= ψ π |= X ϕ iff π1 |= ϕ π |= ϕ U ψ iff ∃k.0 ≤ k, πk |= ψ and ∀i.0 ≤ i < k, πi |= ϕ IV113 Úvod do validace a verifikace: LTL MC str. 33/43 Sémantika temporálních operátorů π |= F ϕ iff ∃k.k ≥ 0, πk |= ϕ π |= G ϕ iff ∀k.k ≥ 0, πk |= ϕ π |= ϕ R ψ iff (∃k.0 ≤ k, πk |= ϕ ∧ ψ and ∀i.0 ≤ i < k, πi |= ψ) or (∀k.k ≥ 0, πk |= ψ) π |= ϕ W ψ iff (∃k.0 ≤ k, πk |= ψ and ∀i.0 ≤ i < k, πi |= ϕ) or (∀k.k ≥ 0, πk |= ϕ) IV113 Úvod do validace a verifikace: LTL MC str. 34/43 LTL Model checking Verifikace s použitím LTL Na systém nahlížíme jako na množinu možných běhů. Systém splňuje vlastnost specifikovanou LTL formulí pokud (a jen tehdy) všechny běhy systému začínající v iniciálním stavu systému splňují danou formuli. Kterýkoliv běh systému, který začíná v iniciálním stavu a nesplňuje danou formuli může být dokladem toho, že systém nesplňuje specifikovanou vlastnost. Tvrzení Pokud konečně stavový systém nesplňuje vlastnost specifikovanou formulí LTL, tak to lze dokladovat během π, který lze vyjádřit jako π = π1 · (π2)ω, kde π1 = s0, s1, . . . , sk π2 = sk+1, sk+2, . . . , sk+n, kde sk ≡ sk+n. Běhy s uvedenou vlastností nazýváme lasa (lasso shape). IV113 Úvod do validace a verifikace: LTL MC str. 35/43 Sekce LTL Model Checking s využitím teorie formálních jazyků a automatů IV113 Úvod do validace a verifikace: LTL MC str. 36/43 Spojitost s jazyky nekonečných slov Pozorování 1 Systém je množina (nekonečných) běhů. Na systém lze nahlížet jako na jazyk nekonečných slov. Pozorování 2 Dva různé běhy (různé posloupnosti stavů) jsou z hlediska platnosti dané formule ekvivalentní, pokud se shodují v interpretaci atomických proměnných. Jestliže π = s0, s1, . . ., pak I(π) def ⇐⇒ I(s0), I(s1), I(s2), . . .. Pozorování 3 Každý běh danou formuli buď splňuje, anebo nesplňuje. Každá LTL formule vymezuje množinu splňujících běhů. IV113 Úvod do validace a verifikace: LTL MC str. 37/43 Redukce problému na jazykovou inkluzi Problém Je dána množina AP, Kripkeho struktura M = (S, T, I, s0) a specifikace LTL formulí ϕ. Splňuje systém M specifikaci ϕ? (M |= ϕ) Jazyky nekonečných slov Nechť Σ = 2AP. Jazyk Lsys všech běhů systému M: Lsys = {I(π) | π je běh v M}. Jazyk Lϕ všech běhů splňující formuli ϕ: Lϕ = {I(π) | π |= ϕ}. Pozorování Systém M splňuje specifikaci ϕ právě když Lsys ⊆ Lϕ. IV113 Úvod do validace a verifikace: LTL MC str. 38/43 Lsys a Lϕ vyjádřeny Büchi automatem Tvrzení 1 Pro každou LTL formuli ϕ existuje (a lze efektivně sestrojit) Büchi automat Aϕ takový, že Lϕ = L(Aϕ). [Vardi, Wolper 1986] Tvrzení 2 Pro každou Kripkeho strukturu M = (S, T, I, s0) lze sestrojit Büchi automat Asys takový, že Lsys = L(Asys). Konstrukce Asys Nechť AP je množina atomických propozic. Pak Asys = (S, 2AP , s0, δ, S), kde q ∈ δ(p, a) právě když (p, q) ∈ T ∧ I(p) = a. IV113 Úvod do validace a verifikace: LTL MC str. 39/43 Synchronní kompozice Büchi automatů – zjednodušená Tvrzení Nechť A = (SA, Σ, sA, δA, FA) a B = (SB, Σ, sB, δB, FB) jsou Büchi automaty nad shodnou abecedou Σ. Pak existuje (lze efektivně sestrojit) Büchi automat A × B takový, že L(A × B) = L(A) ∩ L(B). Pozorování Büchi automat Asys je zkonstruován tak, že FA = SA, tj. má všechny stavy akceptující. Konstrukce A × B pro případ, že FA = SA A × B = (SA × SB, Σ, (sA, sB), δA×B, SA × FB) (p , q ) ∈ δA×B((p, q), a) pro všechna p ∈ δA(p, a) q ∈ δB(q, a) V plné obecnosti je konstrukce A × B složitější. IV113 Úvod do validace a verifikace: LTL MC str. 40/43 Redukce na problém prázdnosti Büchi automatu Tvrzení Pro každou LTL formuli ϕ platí: co−L(Aϕ) = L(A¬ϕ). Redukce M |= ϕ na problém prázdnosti L(Asys × A¬ϕ) M |= ϕ ⇐⇒ Lsys ⊆ Lϕ M |= ϕ ⇐⇒ L(Asys) ⊆ L(Aϕ) M |= ϕ ⇐⇒ L(Asys) ∩ co−L(Aϕ) = ∅ M |= ϕ ⇐⇒ L(Asys) ∩ L(A¬ϕ) = ∅ M |= ϕ ⇐⇒ L(Asys × A¬ϕ) = ∅ IV113 Úvod do validace a verifikace: LTL MC str. 41/43 Redukce problému na detekci akceptujícího cyklu Tvrzení Büchi automat A = (S, Σ, s0, δ, F) akceptuje neprázdný jazyk právě když existují stav s ∈ F a slova w1, w2 ∈ Σ∗ taková, že s ∈ ˆδ(s0, w1) a s ∈ ˆδ(s, w2). Tj. graf Büchi automatu obsahuje dosažitelný akceptující cyklus (cyklus přes nějaký akceptující stav). Rozhodovací procedura pro problém M |= ϕ? Zkonstruuje se produktový automat (Asys × A¬ϕ). Graf produktového automatu se prověří na přítomnost akceptujících cyklů. Obsahuje-li graf akceptující cyklus, pak M |= ϕ. Neobsahuje-li graf akceptující cyklus, pak M |= ϕ. IV113 Úvod do validace a verifikace: LTL MC str. 42/43 Domácí úkol Připomenutí Pro hodnocení stupněm A, nutno realizovat všechny domácí úlohy. Domácí úkol Sestudujte způsob převodu LTL formule na ekvivalentní Buchi automat a implementujte ve Vámi zvoleném programovacím jazyce. Kontrola-demonstrace bude realizována během ústního zkoušení. IV113 Úvod do validace a verifikace: LTL MC str. 43/43