IV113 Validace a verifikace Lehk´y u´vod do anal´yzy program˚ u Jiˇr´ı Barnat
Anal´yza program˚ u
C´ıle programov´ e anal´ yzy Odvodit vlastnosti program˚ u z jejich zdrojov´eho k´odu a ... ... vyuˇz´ıt je pro optimalizaci program˚ u. ... vyuˇz´ıt je pro (alespoˇn ˇc´asteˇcnou) verifikaci program˚ u. Nerozhodnutelnost Vˇsechny zaj´ımav´e vlastnosti program˚ u zapsan´ych v obecn´em programovac´ım jazyce jsou v nerozhodnuteln´e. Henry Gordon Rice (1953) – Riceovy vˇety. Alan Turing (1936) – Probl´em zastaven´ı.
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 2/29
Nerozhodnuteln´e – Jak d´al? Abstrakce Zakryt´ı detail˚ u, za u´ˇcelem zjednoduˇsen´ı anal´yzy. Snaha o korektn´ı, byˇt ne´upln´a ˇreˇsen´ı. Vyuˇ zit´ı abstrakce Zjednoduˇsen´e modelovac´ı jazyky pro popis programu. (Typicky vedou na koneˇcnˇe velk´y stavov´y prostor.) Vykon´av´an´ı k´odu pˇri uvaˇzovan´e abstrakci – abstraktn´ı interpretace. Jin´ e cesty – pˇripomenut´ı jin´ ych pˇr´ıstup˚ u Fixovan´a, ˇci jinak omezen´a mnoˇzina vstup˚ u (testov´an´ı). Omezen´ı zkouman´eho prostoru (bounded MC). Praktick´a nerozhodnutelnost (ˇreˇsiˇce SMT). ´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 3/29
Sekce
Datov´e a predik´atov´e abstrakce
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 4/29
Datov´e abstrakce Motivace Stavov´a exploze zp˚ usoben´a velk´ymi datov´ymi dom´enami. Redukce myˇslenkou dom´enov´eho testov´an´ı, tj. nahrazen´ı konkr´etn´ı velk´e datov´e dom´eny abstrahovanou datovou dom´enou s menˇs´ım poˇctem prvk˚ u. Terminologie Abstrakce: mapov´an´ı konkr´etn´ıch stav˚ u na abstraktn´ı. Konkretizace: mapov´an´ı abstraktn´ıch stav˚ u na mnoˇziny konkr´etn´ıch stav˚ u. Pˇr´ıklad datov´ e abstrakce Int -> { Even, Odd } Konkr´etn´ı stav: h PC:12, A:15, B:0 i Abstraktn´ı stav: h PC:12, A:Odd, B:Even i ´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 5/29
Abstraktn´ı pˇrechodov´y syst´em Pˇrechody v konkr´ etn´ı a abstraktn´ı s´ emantice Pˇr´ıkaz programu na ˇr´adku 12: A := A+A V konkr´etn´ı s´emantice: hPC:12, A:15, B:0i −→ hPC:13, A:30, B:0i
V abstraktn´ı s´emantice: hPC:12, A:Odd, B:Eveni −→ hPC:13, A:Even, B:Eveni
Nedeterminismus v abstraktn´ım pˇrechodov´ em syst´ emu Abstraktn´ı stav: hPC:13, A:Even, B:Eveni Pˇr´ıkaz programu na ˇr´adku 13: A := A div 2 hPC:13, A:Even, B:Eveni −→ hPC:14, A:Even, B:Eveni hPC:14, A:Odd, B:Eveni
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 6/29
Vztah abstraktn´ıho a konkr´etn´ıho pˇrechodov´eho syst´emu Nad-aproximace (Over-Approximation) Kaˇzd´y bˇeh konkr´etn´ıho syst´emu je obsaˇzen v konkretizaci nˇejak´eho abstraktn´ıho bˇehu. Mohou existovat bˇehy, jeˇz jsou obsaˇzeny v konkretizaci nˇejak´eho abstraktn´ıho bˇehu, ale nejsou v p˚ uvodn´ım konkr´etn´ım pˇrechodov´emu syst´emu. Pod-aproximace (Under-Approximation) Kaˇzd´a bˇeh obsaˇzen´y v konkretizaci libovoln´eho abstraktn´ıho bˇehu je bˇehem p˚ uvodn´ıho konkr´etn´ıho pˇrechodov´eho syst´emu. Mohou existovat bˇehy konkr´etn´ıho pˇrechodov´eho syst´emu, kter´e nejsou obsaˇzeny v konkretizaci ˇz´adn´eho abstraktn´ıho bˇehu. ´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 7/29
Verifikace aproximovan´ych pˇrechodov´ych syst´em˚ u Znaˇ cen´ı APS – abstraktn´ı pˇrechodov´y syst´em KPS – konkr´etn´ı pˇrechodov´y syst´em Verifikace nad-aproximace Absence chyby v APS dokazuje absenci chyby v KPS. Chyba v APS m˚ uˇze a nemus´ı b´yt chyba v KPS. Chyba v APS, kter´a nen´ı chybou v KPS, se oznaˇcuje jako ”spurious error” (false positive, false alarm). Verifikace pod-aproximace Chyba v APS dokazuje pˇr´ıtomnost chyby v KPS. Absence chyby v APS nedokazuje absenci chyby v KPS. Chyba v KPS, kter´a nen´ı zachycena v APS, se oznaˇcuje jako (false negative). ´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 8/29
Pˇr´ıklad – konkr´etn´ı s´emantika Pˇr´ıklad Je dosaˇziteln´y chybov´y stav v n´asleduj´ıc´ım programu? % oznaˇcuje operaci modulo, A je celoˇc´ıseln´a promˇenn´a K´od programu
Hodnota A v konkr´etn´ı s´emantice po proveden´ı pˇr´ıkazu vlevo
1 2 3 4 5 6 7
[int] [0] [1]
[1] [2]
read(A); A = A % 2; A = A + 1; if (A==0) error; else return;
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 9/29
Pˇr´ıklad – datov´a abstrakce Pˇr´ıklad Je dosaˇziteln´y chybov´y stav v n´asleduj´ıc´ım programu? A je abstrahov´ano do dom´eny {even,odd} K´od programu
Hodnota A v abstrahovan´e s´emantice po proveden´ı pˇr´ıkazu vlevo
1 2 3 4 5 6 7
[even] [even] [odd]
[odd] [odd] [even] <true/false> <error>
read(A); A = A % 2; A = A + 1; if (A==0) error; else return;
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 10/29
Predik´atov´a abstrakce
Predik´ atov´ a abstrakce Predik´aty – podm´ınkov´e v´yrazy o valuaci promˇenn´ych. Jin´y zp˚ usob jak definovat abstraktn´ı pˇrechodov´y syst´em. Jedna moˇzn´a konkr´etn´ı definice abstrakce: hˇc´ıtaˇc instrukc´ı + valuace zvolen´ych predik´at˚ ui M´ıra abstrakce Mnoˇzstv´ı predik´at˚ u ovlivˇnuje pˇresnost abstrakce. M´alo predik´at˚ u velk´a nepˇresnost, mal´a stavov´a exploze V´ıce predik´at˚ u mal´a nepˇresnost, velk´a stavov´a exploze
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 11/29
Pˇr´ıklad Zad´ an´ı Pro n´ıˇze uveden´y program a uveden´e mnoˇziny predik´at˚ u nakreslete abstraktn´ı pˇrechodov´y syst´em, kter´y vznikne pouˇzit´ım metody predik´atov´e abstrakce. Ve v´ami navrˇzen´em pˇrechodov´em syst´emu rozhodnˇete, zda je nˇekter´a z cest vedouc´ı do chybov´eho programu realizovateln´a. 1 2 3 4 5 6 7
read(A); A = A % 2; A = A + 1; if (A==0) error; else return;
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
a) P1 ≡ A = 0 b) P1 ≡ A = 0, P2 ≡ A ≥ 0
str. 12/29
Pozn´amky k predik´atov´e abstrakci
Anal´ yza abstraktn´ıch cest vedouc´ıch k chybˇ e Rozhodnut´ı o realizovatelnosti (jedn´a se o faleˇsn´y alarm?) Odvozen´ı nov´ych predik´at˚ u, kter´e zpˇresn´ı abstrakci. Probl´ em velikosti abstraktn´ıho pˇrechodov´ eho syst´ emu S poˇctem predik´at˚ u roste exponenci´alnˇe velikost abstraktn´ıho pˇrechodov´eho syst´emu. Moˇ zn´ e ˇreˇsen´ı Predik´aty sv´azan´e s konkr´etn´ı lokac´ı v programu.
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 13/29
Sekce
Metoda CEGAR
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 14/29
Counter-Example Guided Abstraction Refinement Princip metody CEGAR Syst´em je abstrahov´an metodou predik´atov´e abstrakce pro inici´aln´ı mnoˇzinu predik´at˚ u. Abstraktn´ı pˇrechodov´y syst´em (nad-aproximace) verifikov´an metodou ovˇeˇrov´an´ı modelu. V pˇr´ıpadˇe nalezen´ı ”spurious” protipˇr´ıkladu je tento pouˇzit k odvozen´ı nov´ych predik´at˚ u a zpˇresnˇen´ı abstrakce. Po zpˇresnˇen´ı abstrakce se postup opakuje. Pozn´ amky Odvozov´an´ı nov´ych vhodn´ych predik´at˚ u je velmi sloˇzit´e. Odvozov´an´ı predik´at˚ u v dobˇe bˇehu verifikace (on-the-fly). Berkeley Lazy Abstraction Software Verification Tool (BLAST). ´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 15/29
Sch´ema metody CEGAR System
Abstract
Abstract Model
Property Is property satisfied?
Yes
System is valid
No Refined Model Refine Model
Counter Example Is c−example No spurious?
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
System is invalid
Yes
str. 16/29
Sekce
Z´aklady abstraktn´ı interpretace
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 17/29
Programov´a anal´yza abstraktn´ı interpretac´ı Reprezentace programu – Flow Graph ”Speci´aln´ı verze” grafu toku ˇr´ızen´ı (Control-Flow Graph). Kaˇzd´a hrana m´a budˇ pr´avˇe jednu str´aˇz (podm´ınku), nebo pr´avˇe jeden efekt (pˇriˇrazen´ı). C´ıl Vypoˇc´ıtat vlastnosti jednotliv´ych vrchol˚ u flow-grafu. Pˇr´ıklady c´ıl˚ u V jak´em rozsahu hodnot se v dan´em m´ıstˇe programu m˚ uˇze vyskytnout vybran´a promˇenn´a. Kter´e promˇenn´e jsou v dan´em m´ıstˇe programu ˇziv´e. ... ´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 18/29
Obecn´y postup v´ypoˇctu Poˇ zadavky Dom´ena moˇzn´ych ˇreˇsen´ı pro jednotliv´e vrcholy grafu. Inici´aln´ı ˇreˇsen´ı asociovan´e s kaˇzd´ym vrcholem grafu. Definice toho, jak´ym zp˚ usobem ovlivˇnuje (aktualizuje) hrana mezi dvˇema vrcholy ˇreˇsen´ı asociovan´e k dotˇcen´ym vrchol˚ um. Aktualizace ˇreˇsen´ı zp˚ usoben´e (opakovan´ym) zpracov´an´ım hrany flow grafu je monot´onn´ı funkce. V´ ypoˇ cet Vyberu nezpracovanou hranu a aktualizuji ˇreˇsen´ı u pˇridruˇzen´ych vrchol˚ u, pokud se ˇreˇsen´ı zmˇenilo, oznaˇc´ım hranu znovu jako nezpracovanou. Opakuji, dokud existuj´ı nezpracovan´e hrany. ´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 19/29
Pˇr´ıklad – v´ypoˇcet ˇziv´ych promˇenn´ych Konfigurace v´ ypoˇ ctu Dom´ena = potenˇcn´ı mnoˇzina mnoˇziny vˇsech promˇenn´ych. Inici´aln´ı hodnota asociovan´a s vrcholy je ∅. Pro hranu z vrcholu u do vrcholu v je definov´an update ˇreˇsen´ı pro vrchol u takto: V (u) = V (u) ∪ V (v ) \ assigned(u, v ) ∪ used(u, v ) , kde V (x) oznaˇcuje mnoˇzinu ˇreˇsen´ı asociovan´ych s vrcholem x, assigned(u, v ) a used(u, v ) oznaˇcuj´ı promˇenn´e pˇredefinovan´e a pouˇzit´e hranou z u do v . Pozorov´ an´ı V kaˇzd´em bodˇe v´ypoˇctu m´am nˇejak´e (aproximuj´ıc´ı) ˇreˇsen´ı. Dosaˇzen´ı pevn´eho bodu nen´ı garance nejlepˇs´ıho ˇreˇsen´ı. ´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 20/29
Abstraktn´ı interpretace Pozorov´ an´ı V´yˇse uveden´y postup je ve sv´e podstatˇe velmi obecn´y, vhodnou volbou abstrakce a dalˇs´ıch parametr˚ u lze ovˇeˇrovat mnoho r˚ uzn´ych vˇec´ı. Oznaˇcuje se jako abstraktn´ı interpretace. Co lze parametrizovat Abstraktn´ı dom´enu ˇreˇsen´ı. Smˇer aktualizace (po smˇeru, proti smˇeru, oboj´ı). Definice update funkc´ı. Jak kombinovat hodnoty v m´ıstˇe spojen´ı cest flow-grafu. Poˇrad´ı vyhodnocov´an´ı nezpracovan´ych hran. Detekce ˇcasn´eho ukonˇcen´ı. ´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 21/29
Relevantn´ı ot´azky abstraktn´ı interpretace
Existuje pevn´ y-bod? Struktura moˇzn´ych ˇreˇsen´ı asociovan´ych s jednotliv´ymi vrcholy tvoˇr´ı u´pln´y svaz. Knaster-Tarskiho teor´em ˇr´ık´a, ˇze na takov´e dom´enˇe m´a kaˇzd´a monot´onn´ı funkce pevn´y bod. Terminuje v´ ypoˇ cet? Pokud neexistuje nekoneˇcn´a rostouc´ı posloupnost moˇzn´ych ˇreˇsen´ı, pak ano. V opaˇcn´em pˇr´ıpadˇe nemus´ı.
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 22/29
Pomocn´e techniky – Rozˇs´ıˇren´ı Rozˇs´ıˇren´ı (Widening) Pomocn´a transformace vypoˇc´ıtan´ych mezi-ˇreˇsen´ı tak, aby zachovalo korektnost, ale zabr´anilo existenci nekoneˇcnˇe rostouc´ı posloupnosti, respektive zkr´atilo jej´ı d´elku. Pˇr´ıklad Urˇcen´ı ˇc´ıseln´eho intervalu, ve kter´em budou hodnoty zpracov´any pˇresnˇe, mimo tento interval budou reprezentov´any hodnotou +∞ nebo −∞. Posloupnost [0,1] ⊂ [0,2] ⊂ [0,3] ⊂ [0,4] ⊂ [0,5] ⊂ [0,6] ... se pro interval pˇresnosti [0,3] zmˇen´ı na: [0,1] ⊂ [0,2] ⊂ [0,3] ⊂ [0,+∞] ´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 23/29
Pomocn´e techniky – Z´uˇzen´ı Z´ uˇ zen´ı (Narrowing) Pouˇzit´ı rozˇs´ıˇren´ı vede na velmi nepˇresn´e v´ysledky. M˚ uˇze b´yt pouˇzit pouze doˇcasnˇe k terminaci anal´yzy cykl˚ u. Po anal´yze cyklu moˇzno prov´est anal´yzu cyklu znovu a pˇresnˇe, avˇsak s inici´aln´ı hodnotou z´ıskanou po dokonˇcen´ı anal´yzy cyklu s rozˇs´ıˇren´ım. Pˇr´ıklad Hodnota [0,+∞] se proveden´ı z´uˇzen´ı dostane na re´alnou hodnotu [0,n]. Koment´ aˇr Pˇresn´e a dalˇs´ı pouˇzit´ı technik rozˇs´ıˇren´ı a z´uˇzen´ı je nad r´amec tohoto kurzu. ´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 24/29
Fin´aln´ı pozn´amky k abstraktn´ı interpretaci Dalˇs´ı oblasti programov´ e anal´ yzy Mezi-procedur´aln´ı anal´yza. Anal´yza paraleln´ıch program˚ u. Generov´an´ı invariant˚ u. Anal´yza ukazatel˚ u a dynamick´ych datov´ych struktur. ... CPA checker The Configurable Software-Verification Platform http://cpachecker.sosy-lab.org/ V´ıtˇez mnoha kategori´ıch v Software Verification Competition. ´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 25/29
Dom´ac´ı u´kol
Pˇripomenut´ı Pro moˇznost udˇelen´ı hodnocen´ı stupnˇem A, je nutn´e vypracovat vˇsechny dom´ac´ı u´lohy. Zad´ an´ı dom´ ac´ı u ´lohy Identifikujte ve slajdech m´ısto, kter´e by st´alo za to doplnit nˇejak´ym vysvˇetluj´ıc´ım obr´azkem, tento obr´azek vytvoˇrte a nejpozdˇeji v den kon´an´ı zkouˇsky poˇslete emailem vyuˇcuj´ıc´ımu spolu s identifikac´ı m´ısta um´ıstˇen´ı.
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 26/29
Sekce
A to je konec ...
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 27/29
Shrnut´ı IV113 a reklama IV113 – Pˇrehled verifikaˇ cn´ıch pˇr´ıstup˚ u Black-box testing. White-box testing a symbolick´a exekuce. Principy deduktivn´ı verifikace. Model checking LTL a CTL. Bounded model checking. ´ Uvod do programov´e anal´yzy. IA159 – Formal Verification Methods Detaily vybran´ych verifikaˇcn´ıch metod. Programov´a anal´yza. Verifikace nekoneˇcnˇe stavov´ych syst´em˚ u. IV101 – Semin´ aˇr z verifikace Pouˇzit´ı verifikaˇcn´ıch n´astroj˚ u. ´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 28/29
Z´avˇerem
Zkouˇsky Bez pomocn´ych materi´al˚ u na veˇsker´y odpˇredn´aˇsen´y obsah. Nutno se pˇrihl´asit skrze IS. V´ yzva Pros´ım o zpˇetnou vazbu skrze studentskou anketu. Uv´ıt´am n´amˇety a obr´azky na doplnˇen´ı slajd˚ u.
Dˇ ekuji za pozornost!
´ IV113 Uvod do validace a verifikace: Anal´ yza program˚ u
str. 29/29
