IV113 Validace a verifikace Ověřování modelu s využitím řešičů SAT a SMT (Bounded Model Checking) Jiří Barnat Připomenutí – SAT a SMT Problém splnitelnosti – SAT Nalezení valuace boolovských proměnných formule výrokové logiky takové, že formule je v této valuaci pravdivá. Satisfiability Modulo Theory – SMT Problém rozhodnout splnitelnost formule prvořádové logiky s rovností, predikáty a funkčními symboly kódující jednu či více zvolených teorií. Typické teorie SMT Aritmetika neomezených celých a desetinných čísel. Aritmetika celých čísel omezené velikosti (bitové vektory). Teorie datových struktur (seznamy, pole, . . . ). IV113 Úvod do validace a verifikace: Bounded Model Checking str. 2/30 Připomenutí – Řešiče SAT a SMT ZZZ aka Z3 Nástroj vyvíjený v Microsoft Research. WWW interface — http://www.rise4fun.com/Z3 Binární API pro použití v jiných aplikacích. SMT-LIB Standardizace jazyka pro zadávání SMT dotazů. Volně dostupná knihovna s implementací SMT. IV113 Úvod do validace a verifikace: Bounded Model Checking str. 3/30 Připomenutí – Splnitelnost a platnost Pozorování Formule je platná právě když její negace není splnitelná. Důsledek Řešiče SAT a SMT lze využít jako nástroje pro dokazování platnosti formulovaných tvrzení. Syntéza modelu Řešiče SAT nejen rozhodují splnitelnost formulí, ale v případě splnitelnosti vrací požadovanou valuaci proměnných, pro níž je formule pravdivá. Na rozdíl od dokazovacích nástrojů tak poskytují "protipříklad" v případě neplatnosti dokazovaného tvrzení. IV113 Úvod do validace a verifikace: Bounded Model Checking str. 4/30 Sekce Ověřování safety vlastností redukcí na problém SAT IV113 Úvod do validace a verifikace: Bounded Model Checking str. 5/30 Bounded Model Checking (BMC) Hypotéza Je-li v systému chyba, pro její reprodukci stačí malý počet kontrolovaných kroků systému. Myšlenka metody Používáme-li metodu ověřování modelu pro detekci chyb, je smysluplné zkoumat, zda k porušení specifikace dojde během prvních k kroků systému. Literatura Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu: Symbolic Model Checking without BDDs. TACAS 1999: 193-207, LNCS 1579. Henry A. Kautz, Bart Selman: Planning as Satisfiability.Proceedings of the 10th European conference on Artificial intelligence (ECAI’92): 359-363, 1992, Kluwer. IV113 Úvod do validace a verifikace: Bounded Model Checking str. 6/30 Redukce problému BMC na problém SAT Předpoklady Množinu prefixů délky k všech běhů Kripkeho struktury M lze kódovat boolovskou formulí [M]k . Porušení vlastnosti typu safety, které se projeví po provedení k kroků systému, lze kódovat formulí [¬ϕ]k . Redukce na problém SAT Ověřuje se splnitelnost formule [M]k ∧ [¬ϕ]k . Splnitelnost indikuje existenci protipříkladu délky k. Nesplnitelnost formule prokazuje neexistenci protipříkladu délky k. IV113 Úvod do validace a verifikace: Bounded Model Checking str. 7/30 Kripkeho struktura jako boolovské formule Předpoklady Mějme Kripkeho strukturu M = (S, T, I) s iniciálním stavem s0 ∈ S. Libovolný stav s ∈ S lze reprezentovat jako bitový vektor délky n, tj. stav s = a0, a1, . . . , an−1 . Kódování M skrze boolovské formule Init(s) – formule, která je splnitelná právě pro takovou valuaci proměnných a1, a2, ..., an, které popisují stav s0. Trans(s, s ) – formule, která je splnitelná pro stavové vektory s, s , právě tehdy když valuace proměnných a1, a2, ..., an, a1, a2, ..., an popisuje stavy, mezi kterými existuje přechod, tj. (s, s ) ∈ T. IV113 Úvod do validace a verifikace: Bounded Model Checking str. 8/30 Kódování konečných běhů M Popis běhů systému délky k Běh délky k je tvořen k + 1 stavy s0, s1, . . . , sk. Množina všech běhů délky k struktury M je označena jako [M]k a je popsána následující formulí: [M]k ≡ Init(s0) ∧ k i=1 Trans(si−1, si ) Příklad [M]3 ∧ [¬ϕ]3 Init(s0)∧Trans(s0, s1)∧Trans(s1, s2)∧Trans(s2, s3)∧¬ϕ(s3) IV113 Úvod do validace a verifikace: Bounded Model Checking str. 9/30 Sekce Úplnost metody BMC IV113 Úvod do validace a verifikace: Bounded Model Checking str. 10/30 Úplnost BMC pro detekci porušení safety vlastností Problém – nedetekované porušení vlastnosti typu safety Porušení invariantu je cestou délky k nedosažitelné. Cesty kratší než k nejsou v [M]k kódovány. Ohraničení k shora Pokud k ≥ d, kde d je průměr grafu, všechny místa možného porušení invariantu jsou pokryta. Průměr grafu lze omezit konstantou 2n , kde n je počet bitů stavového vektoru. Řešení problému Realizace procedury BMC postupně pro k ∈ [0, d]. IV113 Úvod do validace a verifikace: Bounded Model Checking str. 11/30 Automatická detekce průměru grafu Fakta Určení konstanty d uživatelem je nereálné. Bezpečné horní odhady jsou velmi vzdálené realitě. Chtěli bychom, aby samotná procedura verifikace detekovala, zda má smysl nadále zvyšovat k. Kostra algoritmu pro úplný BMC k = 0 while (true) do if (existuje protipříklad délky k) then return "Invalid" if (neexistuje protipříklad délky větší než k) then return "Valid" k = k + 1 od IV113 Úvod do validace a verifikace: Bounded Model Checking str. 12/30 Značení I Předpoklady Kripkeho struktura M = (S, T, I). Stavy popsány bitovými vektory fixní délky. Trans je SAT reprezentace binární relace T. Cesta délky n path(s[0..n]) ≡ 0≤i