Několik poznámek k laboratořím z TI2 -- 2003/2004

B. Křena, T. Vojnar


Formální analýza a verifikace


Proč se zabýváme formálními technikami?

Cena odstranění nalezené chyby roste s dobou, po kterou chyba nebyla nalezena (např. cena opravy při zadání = 1, při analýze = 2, při návrhu = 5, při implementaci = 10, při testování = 15, u zákazníka = 50).

Chyby, které se projeví až při provozu jsou zvláště nepříjemné, protože snižují věrohodnost produktu. Navíc u kritických aplikací může dojít k nenahraditelným ztrátám (třeba i na životech).

Formální techniky nám pomáhají nalézt chyby co nejdříve a tím snižují náklady na jejich odstranění.


Jaké jsou možnosti hledání chyb?


Jaký je rozdíl mezi testováním a simulací a formální analýzou a verifikací?

Testování a simulace může prokázat pouze existenci chyby, zatímco formální analýza a verifikace může dokázat správnost modelu/systému. V praxi se techniky kombinují. I v případě, kdy formální nalýza či verifikace není úspěšná při dokazování správnosti systému (příliš složitý systém), mohou být nalezeny v systému chyby, a to jiné než při simulaci či testování (jiný způsob zkoumání chování systému)


Nevýhody formální analýzy a verifikace?


Jaký je rozdíl mezi formální analýzou a verifikací?

Analýza odpovídá na obecnější otázky (např. živost, bezpečnost/omezenost, konzervativnost systému, pokrytí invarianty), z nichž lze vyvodit konkrétní závěry pro zkoumaný systém (model).

Verifikace odpovídá na konkrétně položené otázky. Typické odpovědi jsou "ano", "ne"/"ne, protože" (či "chyba -- nedostatek paměti").


Proces formální analýzy:


Proces formální verifikace:


Příklady vlastností, které lze zjišťovat při formální analýze:


Základní přístupy k formální verifikaci zahrnují:


Theorem proving


Model checking


Static analysis


V čem spočívá problém stavové exploze?

Velikost stavového prostoru roste exponenciálně s velikostí modelu, a proto nelze přímou cestou verifikovat rozsáhlejší modely. Příčinou exponenciálního nárustu je procházení všech možných kombinací hodnot jednotlivých proměnných a všech možných kombinací řídících stavů jednotlivých paralelních procesů.


Jak lze problém stavové exploze řešit či omezit?

Různými technikami, které využívají speciální vlastnosti konkrétních modelovacích a dotazovacích jazyků či třídy verifikovaných problémů. Například:

Zdroje nekonečnosti

Možných zdrojů nekonečnosti u zkoumaných systémů, resp. jejich modelů je celá řada: práce s reálným časem, neomezenými čítači, zásobníkem, neomezenými komunikačními kanály, neomezenou alokací paměti, parametry (chceme ověřit, že systém se chová správně pro libovolný počet procesů apod.). Reálný čas (a další spojité proměnné) a parametry představují zdroje nekonečnosti přítomné i v reálných systémech. Práce s neomezenými čítači, zásobníkem, komunikačními kanály apod. představuje abstrakci reálných systémů, ale její použití může být stále snazší než práce s obrovskými či parametrickými mezemi systému.




zpět na hlavní stránku
Případně nalezené nedostatky prosím oznamte na: Tomáš Vojnar.