IV113 Validace a verifikace Detekce akceptujícího cyklu Jiří Barnat Připomenutí Problém Kripkeho struktura M LTL formule ϕ M |= ϕ ? Řešení pomocí Büchiho automatů Asys – automat akceptující běhy modelu A¬ϕ – automat akceptující běhy porušující vlastnost ϕ L(Asys) ∩ L(A¬ϕ) = L(Asys × A¬ϕ) L(Asys × A¬ϕ) = ∅ ⇐⇒ model má běh porušující ϕ L(Asys × A¬ϕ) = ∅ ⇐⇒ M |= ϕ IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 2/37 Algoritmus pro detekci akceptujících cyklů Vstup algoritmu Produktový automat ve formě tří následujících funkcí |F|_init() — Vrací iniciální stav automatu. |F|_succs(s) — Pro daný stav vrací jeho přímé následníky. |Accepting|(s) — O stavu řekne, zda je či není akceptující. Výstup algoritmu Přítomen / Nepřítomen Protipříklad. Algoritmus Využívá vnořené prohledávání do hloubky – Nested DFS. Vnější procedura detekuje akceptující stavy, vnitřní procedura testuje, zda akceptující stav je dosažitelný ze sebe sama (leží na cyklu). IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 3/37 Sekce Detekce akceptujících cyklů IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 4/37 Detekce akceptujících cyklů Problém Je dán Büchiho automat A = (S, Σ, δ, s0, F). Je jazyk akceptovaný automatem A neprázdný? Redukce na detekci akceptujícího cyklu v grafu Nechť G = (S, E), kde E = {(u, v) ∈ S × S | ∃a ∈ Σ takové, že v ∈ δ(u, a)} je graf Büchiho automatu. L(A) je neprázdný právě když graf automatu A obsahuje dosažitelný akceptující cyklus, tj. cyklus jehož alespoň jeden vrchol v je akceptující (v ∈ F) a zároveň dosažitelný z iniciálního stavu ((s0, v) ∈ E∗ ). IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 5/37 Detekce akceptujících cyklů Algoritmické řešení 1) V grafu Büchiho automatu identifikuj všechny dosažitelné akceptující vrcholy. (Vnější procedura.) 2) Pro každý takto identifikovaný vrchol ověř, že není dosažitelný ze sebe sama. (Vnitřní procedura.) Dosažitelnost v grafu Standardní grafový algoritmus. Výpočet množiny dosažitelných, případně akceptujících dosažitelných vrcholů lze provést v čase O(|V | + |E|). S obecným algoritmem detekce dosažitelnosti je detekce přítomnosti akceptujícího cyklu proveditelná v čase O(|V | + |E| + |F|(|V | + |E|)). Pokud ale použijeme strategii prohledávání do hloubky, lze dosáhnout času O(|V | + |E|). IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 6/37 Prohledávání grafu do hloubky proc Reachable(V ,E,v0) Visited = ∅ DFS(v0) return (Visited) end proc DFS(vertex) if vertex ∈ Visited then /∗ Visits vertex ∗/ Visited := Visited ∪ {vertex} foreach { v | (vertex,v)∈ E } do DFS(v) od /∗ Backtracks from vertex ∗/ fi IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 7/37 Barevné značení vrcholů při DFS Pozorování Při prohledávání grafu procedurou DFS se každý vrchol grafu nachází v jednom ze tří možných stavů. Barevné značení vrcholů Bílý vrchol - dosud nebyl navštíven. Šedý vrchol - navštívený, ale dosud nebyl backtrackován. Černý vrchol - navštívený i backtrackovaný. Zásobník rekurze Šedé vrcholy tvoří cestu od počátečního vrcholu k vrcholu, který je v daný okamžik algoritmem zpracováván. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 8/37 Vlastnosti DFS, G = (V , E) a v0 ∈ V Pozorování Pokud pro dva různé vrcholy v1, v2 platí, že (v0, v1) ∈ E∗ , (v1, v1) ∈ E+ , (v1, v2) ∈ E+ . Pak procedura DFS(v0) backtrackuje z vrcholu v2 dříve než backtrackuje z vrcholu v1. DFS post-order Pokud (v, v) ∈ E+ a (v0, v) ∈ E∗ , pak po skončení procedury DFS(v), volané v rámci výpočtu DFS(v0), jsou všechny vrcholy u takové, že (v, u) ∈ E+ navštívené a backtrackované. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 9/37 Detekce akceptujících cyklů v čase O(|V | + |E|) Předpoklady Volání vnitřní procedury pro akceptující vrchol v ohlásí cyklus a ukončí algoritmus, pokud akceptující vrchol v leží na akceptujícím cyklu. Klíčová myšlenka Vnořené procedury jsou volány v pořadí, ve kterém vnější procedura z akceptujících vrcholů backtrackuje, tj. dle DFS post-orderu. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 10/37 Detekce akceptujících cyklů v čase O(|V | + |E|) proc Detekce akceptujících cyklů Visited := ∅ DFS(v0) end proc DFS(vertex) if (vertex) ∈ Visited then Visited := Visited ∪ {vertex} foreach {s | (vertex,s) ∈ E} do DFS(s) od if IsAccepting(vertex) then DetectCycle(vertex) fi fi end IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 11/37 Detekce akceptujících cyklů v čase O(|V | + |E|) Pozorování Pokud podgraf dosažitelný z vrcholu s neobsahuje akceptující cyklus, pak žádný akceptující cyklus přes vrchol r ležící mimo podgraf dosažitelný z s neprochází stavem dosažitelným z s. Tvrzení Pokud vnitřní procedura pro vrchol v skončí aniž by ohlásila cyklus, tak podgraf dosažitelný z vrcholu v neobsahuje akceptující cyklus. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 12/37 Detekce akceptujících cyklů v čase O(|V | + |E|) Důsledek vedoucí k lineárnímu algoritmu Každou vnitřní proceduru lze omezit na vrcholy dosud nenavštívené v žádné předchozí vnitřní proceduře. O(|V | + |E|) algoritmus 1) Vnitřní procedury budou spouštěny pro akceptující vrcholy v pořadí, ve kterém vnější procedura z těchto vrcholů backtrackuje. 2) Vnitřní procedury nenavštěvují vrcholy navštívené v předchozích vnitřních procedurách. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 13/37 Detekce cyklu ve vnitřních procedurách Tvrzení Pokud je následníkem právě zpracovávaného vrcholu šedý vrchol (tj. vrchol na zásobníku rekurzivních volání procedury DFS), pak graf obsahuje cyklus. Využití Ve vnořené proceduře není nutné dosáhnout přesně vrcholu, pro který je detekce cyklu volána, ale stačí dosáhnout vrcholu na zásobníku vnější procedury. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 14/37 O(|V | + |E|) Algoritmus proc Detekce akceptujících cyklů Visited := Nested := in_stack := ∅ DFS(v0) Exit("Nepřítomen") end proc DFS(vertex) if (vertex) ∈ Visited then Visited := Visited ∪ {vertex} in_stack := in_stack ∪ {vertex} foreach {s | (vertex,s) ∈ E} do DFS(s) od if IsAccepting(vertex) then DetectCycle(vertex) fi in_stack := in_stack \ {vertex} fi end proc DetectCycle (vertex) if vertex ∈ Nested then Nested := Nested ∪ {vertex} foreach {s | (vertex,s) ∈ E} do if s ∈ in_stack then WriteOut(in_stack) Exit("Přítomen") else DetectCycle(s) fi of fi end IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 15/37 Složitost Vnější procedura Časová složitost: O(|V | + |E|) Prostorová složitost: O(|V |) Vnitřní procedury Celková časová složitost: O(|V | + |E|) Prostorová složitost: O(|V |) Složitost Časová složitost: O(|V | + |E| + |V | + |E|) = O(|V | + |E|) Prostorová složitost: O(|V | + |V |) = O(|V |) IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 16/37 DFS – příklad IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 17/37 Sekce Typy Büchi automatů a jejich využití při verifikaci IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 18/37 Podtřídy Büchi automatů Terminální Büchi automaty Všechny akceptující cykly v automatu jsou právě ve formě smyčky nad akceptujícím stavem strážené výrazem true. Slabé Büchi automaty (weak) Každá silně souvislá komponenta automatu je striktně tvořena buď pouze akceptujícími stavy, nebo pouze neakceptujícími. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 19/37 Dopad na verifikační proceduru Automat A¬ϕ Pro řadu LTL formulí ϕ je A¬ϕ terminální nebo slabý. A¬ϕ je typicky velmi malý (max desítky stavů). Typ A¬ϕ lze zjistit před procesem verifikace. Typy komponent A¬ϕ Neakceptující – bez akceptujícího cyklu. Striktně akceptující – každý cyklus je akceptující. Smíšené – obsahuje akceptující i neakceptující cykly. Produktový automat Prohledávaný graf je synchronní produkt AS a A¬ϕ. Typ komponent AS × A¬ϕ určen odpovídajícími komponentami A¬ϕ. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 20/37 Dopad na verifikační proceduru – Terminální BA A¬ϕ je terminální Büchi automat Pro důkaz existence akceptujícího cyklu stačí prokázat dosažitelnost stavu akceptujícího ve složce A¬ϕ. Proces verifikace se redukuje na analýzu dosažitelnosti. „Safety” vlastnosti Vlastnost ϕ, pro které je A¬ϕ terminální BA. Typická slovní formulace: „Nenastane špatná událost.” Pro verifikaci stačí analýza dosažitelnosti. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 21/37 Dopad na verifikační proceduru – Slabé BA A¬ϕ je slabý Büchi automat Neobsahuje smíšené komponenty. Pro důkaz existence akceptujícího cyklu stačí prokázat dosažitelnost cyklu v akceptující komponentě. Lze detekovat pomocí jednoduchého DFS. Znám optimální algoritmus, který nevyžaduje DFS. „Slabé” LTL vlastnosti Vlastnost ϕ, pro které je A¬ϕ slabý BA. Typická vlastnost je „response”: G (a =⇒ F (b)) IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 22/37 Klasifikace LTL formulí Klasifikace Každá LTL formule patří do jedné z následujících tříd: Reactivity, Recurrence, Persistance, Obligation, Safety, Guarantee Zajímavá fakta Je-li vlastnost ze třídy Guarantee, je popsatelná terminálním Büchi automatem. Je-li vlastnost ze tříd Persistance, Obligation nebo Safety je popsatelná slabým Büchi automatem. Při verifikaci se formule neguje (ϕ → A¬ϕ) ϕ ∈ Safety ⇐⇒ ¬ϕ ∈ Guarantee. ϕ ∈ Recurrence ⇐⇒ ¬ϕ ∈ Persistance. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 23/37 Klasifikace LTL formulí Guarantee Obligation Safety PersistenceRecurrence Reactivity General BA Weak BA Terminal BA IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 24/37 Sekce Boj se stavovou explozí IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 25/37 Stavová exploze Co je to stavová exploze Systém bývá popsán jako paralelní kompozice procesů. Vzájemným proložením možných chování jednotlivých procesů vznikají různé možné stavy systému jako celku. Počet dosažitelných stavů systému může být až exponenciálně větší než součet počtu stavů procesů. Důsledek Do operační paměti počítače nezle uložit všechny stavy produktového automatu. Je obtížně detekovat přítomnost akceptujícího cyklu. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 26/37 Vybrané metody boje se stavovou explozí Komprese stavových vektorů Neztrátové komprese Ztrátové – heuristiky On-The-Fly verifikace Symbolická reprezentace stavového prostoru Redukce počtu stavů produktového automatu Redukce zaváděním atomických bloků Redukce částečným uspořádáním akcí Redukce symetrií Paralelní/Distribuovaná verifikace IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 27/37 On-The-Fly verifikace Pozorování Graf lze zadat pomocí funkcí (tzv. implicitní definice) |F|_init() — Vrací iniciální vrchol grafu. |F|_succs(s) — Pro daný vrchol vrací jeho přímé následníky. |Accepting|(s) — O stavu řekne, zda je či není akceptující. On-the-fly verifikace Pokud graf obsahuje akceptující cyklus, algoritmus je schopen v některých případech detekovat přítomnost akceptujícího cyklu, aniž by přitom navštívil (a tedy uložil) všechny vrcholy grafu. Problém M |= ϕ je někdy možné rozhodnout bez nutnosti úplné enumerace vrcholů a hran automatu Asys × A¬ϕ. Metoda verifikace s výše popsanou vlastností se označuje jako on-the-fly metoda verifikace. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 28/37 Redukce uspořádáním akcí Příklad Uvažme systém tvořený dvěma procesy A a B. A je tvořen jednou akcí α, B sekvencí akcí β1, . . . , βm. Neredukovaný stavový prostor: βm α α α β1 β2 βm α β1 β2 s r Vlastnost: Je dosažitelný stav r? IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 29/37 Redukce uspořádáním akcí Pozorování Běhy (αβ1β2 . . . βm), (β1αβ2 . . . βm), . . . , (β1β2 . . . βmα) jsou vzhledem k dané vlastnosti ekvivalentní. Je dostačující zvážit pouze jednoho reprezentanta z třídy ekvivalence, například (β1β2 . . . βmα). βm α α α β1 β2 βm α β1 β2 s r Reprezentanta lze získat odkládáním akce α. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 30/37 Redukce uspořádáním akcí Princip redukce Při generování grafů se místo funkce všech přímých následníků, uvažují pouze někteří přímí následníci vrcholu. V důsledku toho je počet vygenerovaných stavů produktového automatu menší. Technická realizace Optimální způsob výběru následníků je obtížný. Nástroje implementují různé heuristiky. Redukovaný stavový prostor musí zachovávat přítomnost akceptujícího cyklu. Formule nesmí obsahovat operátor X (podtřída LTL). Anglický název Partial Order Reduction IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 31/37 Distribuovaná/Paralelní verifikace Princip Nesnaží se zmenšit paměťové nároky výpočtu. Snaží se efektivně využít větší množství výpočetních zdrojů. Problémy algoritmu Nested DFS Algoritmus přistupuje operační paměť velmi náhodně. Prosté swapování na disk nefunguje (výprask OS). Simulace Nested DFS algoritmu v prostředí s distribuovanou pamětí je pomalá (předávání peška). Není znám způsob jak DFS post-order napočítat efektivně paralelním algoritmem. (Otevřený problém.) IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 32/37 Paralelní algoritmy pro detekci cyklu Pozorování Místo Nested DFS algoritmu se používají jiné (časově neoptimální) algoritmy, jejichž výpočet ale lze dobře paralelizovat. Složitost Optimalita On-The-Fly Nested DFS O(V+E) Ano Ano OWCTY obecné Büchi automaty O(V.(V+E)) Ne Ne slabé Büchi automaty O(V+E) Ano Ne MAP O(V.V.(V+E)) Ne Částečně OWCTY+MAP obecné Büchi automaty O(V.(V+E)) Ne Částečně slabé Büchi automaty O(V+E) Ano Částečně IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 33/37 Sekce Ověřování modelu – shrnutí IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 34/37 Princip rozhodovací procedury a stavová exploze Platnost formule Požadovaná vlastnost může být porušena při jednom jediném konkrétním proložení akcí. Rozhodnutí je podloženo analýzou grafu stavového prostoru verifikovaného programu. Stavová exploze Není-li řečeno jinak, je třeba uvážit všechna možná proložení akcí. Počet stavů, do kterých se může dostat paralelní program, je exponenciálně větší než velikost zápisu paralelního programu. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 35/37 Výhody metody ověřování modelu Obecná technika aplikovatelná na různé typy systémů Hardware, software, zabudované systémy, . . . Garance výsledku (matematicky podložen) Rozhodovací procedura tvrdí, že M |= ϕ, tehdy a jen tehdy, pokud to skutečně platí. Existence podpůrných nástrojů – “model checkerů” Verifikace tzv. na kliknutí myši / zmačknutí tlačítka. Minimální účast uživatele v rozhodovacím procesu. Automatická identifikace a generování protipříkladů. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 36/37 Nevýhody metody ověřování modelu Vhodná pouze k verifikaci konkrétních transformací Nelze použít na obecný důkaz toho, že program například pro zadané n spočítá hodnotu n!. Lze však ověřit, že pro hodnotu 5 program vrátí 120. Verifikuje pouze model systému Platnost formule, neznamená splnění specifikace systémem. Nutnost vytváření modelu. Velikost stavového prostoru Aplikovatelné (pouze) na konečně stavové systémy. Vzhledem k stavové explozi je praktická aplikovatelnost techniky omezena na relativně malé modely. Verifikuje jen to, co je specifikováno Co není vyjádřeno formulemi, to se neverifikuje. IV113 Úvod do validace a verifikace: Detekce akceptujícího cyklu str. 37/37