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?
- simulace a testování
- formální analýza a verifikace
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?
- nároky na kvalifikaci uživatele
- vysoké nároky na výpočetní zdroje (paměť, procesorový čas, ...)
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:
- vytvoření modelu (lze přeskočit při práci přímo se systémem, např.
programem, specifikací obvodu ve VHDL apod.)
- (automatický) výpočet obecných vlastností
- interpretace výsledků
Proces formální verifikace:
- vytvoření modelu (lze přeskočit při práci přímo se systémem)
- specifikace vlastnosti, kterou chceme ověřit
- (automatická) kontrola, zda model splňuje specifikaci
Příklady vlastností, které lze zjišťovat při formální analýze:
- Síť je obyčená (ordinary), pokud násobnost všech hran je rovna jedné.
- Síť je stejnorodá (homogeneous), pokud všechny hrany vycházející
z libovolného místa p sítě mají stejnou násobnost.
- Síť je čistá (pure), pokud neobsahuje vlastní cyklus.
Preset a postset jsou tedy disjunktní množiny pro každý
přechod sítě.
- Síť je konzervativní (conservative), pokud zachovává počet
značek. Tzn. počet odebraných značek z presetu
je roven počtu značek umístěných do postsetu pro každý přechod
sítě.
- Síť je podkonzervativní (subconservative), pokud nezvyšuje
počet značek. Tzn. počet odebraných značek z presetu
je roven nebo větší než počet značek umístěných do postsetu
pro každý přechod sítě.
- Síť (graf) je souvislá(ý) (connected), pokud pro každý prvek
sítě (uzel grafu) existuje neorientovaná cesta ke každému
dalšímu prvku sítě (uzlu grafu).
- Síť (graf) je silně souvislá(ý) (strongly connected) pokud
pro každý prvek sítě (uzel grafu) existuje orientovaná cesta
ke každému dalšímu prvku sítě (uzlu grafu).
- Síť nazveme značený graf (marked graph), jestliže každé místo
má právě jeden přechod v presetu a právě jeden přechod v postsetu
(násobnost hran v úvahu nebereme).
- Síť nazveme stavovým strojem (state machine), jestliže každý přechod
má právě jedno místo v presetu a právě jedno místo v postsetu
(násobnost hran v úvahu nebereme).
- Síť nazýváme sítí s volným výběrem (free choice), pokud každé
sdílené místo je jediné místo v presetu všech přechodů, které
náleží do postsetu tohoto sdíleného místa.
Základní přístupy k formální verifikaci zahrnují:
- model checking
- theorem proving
- static analysis
Theorem proving
- Využívá poloautomatický dokazovací prostředek.
- Je založený na odvozovacích pravidlech zvolené logiky
obvykle vyššího řádu, která je obecně nerozhodnutelná.
- Vyžaduje experta, který určuje, jak se má důkaz vést.
Model checking
- Využívá obvykle automatický prostředek.
- Využívá (explicitní či implicitní) generování a prohledávání stavového
prostoru.
- Hlavní nevýhodou je problém stavové exploze,
kdy velikost stavového prostoru roste exponenciálně
s velikostí modelu, případně nutnost práce s nekonečným počtem stavů.
Static analysis
- Využívá obvykle automatický prostředek.
- Snaha o ověření příslušných vlastností na základě popisu modelu či
systému, aniž by se tento prováděl a procházel se stavový prostor (využití
invariantů apod.).
- Minimalizuje se stavová exploze, rozsah ověřitelných vlastností se
snižuje. (Vidíme-li, že v programu je proměnná x inicializována na 0 a nikde
není operace - nad x, můžeme říci, že x>0 je invariant, ale bez provádění
programu nemusíme být schopni určit, zda také x<10 je invariant.)
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:
- Symbolický model checking
- reprezentace velkých i nekonečných množin stavů relativně malou
formulí, automatem apod.
- velice úspěšné u verifikace HW
- Redukce založené na částečném uspořádání (partial order)
- výběr jedné reprezentativní ze všech možných posloupností akcí
- klíčové při verifikaci SW
- Kompozitní přístup (compositional reasoning)
- Ověříme standardní cestou jednotlivé části a pak se pokusíme na
základě zjištěných skutečností ověřit, že vlastnost splňuje i celek.
- Automatizovaná abstrakce
- Pokusíme se automaticky vygenerovat systém s méně detaily chování
než u původního systému a tím s jednodušším a menším (či alespoň
konečným) stavovým prostorem.
- Abstrakce by měla nadaproximovat původní systém. Pak pokud neodhalíme
chybu, není chyba ani v původním systému. Pokud chybu odhalíme, může se
jednat o chybu uměle vnesenou do systému asbtrakcí. V tom případě je nutno
abstrakci zjemnit (counterexample guided abstraction refinement).
- Symetrie
- Využívá symetrie v systému a zkoumá jen reprezentatnty symetrických
situací (např. jeden proces čte, ostatní čekají, přičemž není důležité,
zda čte proces jedna, dvě, či jiný).
- On-the-fly techniky
- Ověřujeme specifikovanou vlastnost současně s generováním stavového
prostoru a pokud ji vyloučíme nebo potvrdíme, ukončíme generování
zbývající části stavového prostoru.
- Generování může být navíc řízeno ověřovanou vlastností: Jsme-li
schopni detekovat, že žádný z následníků daného stavu nemůže ovlivnit
zkoumanou vlastnost, nebudeme dále rozvíjet příslušnou větev stavového
prostoru.
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.