Model a specifikace
Program a jeho specifikace( popis vlastností programu nebo požadovaného či nežádoucího cho vání v nějakém formálním jazyku) je pak zpracován speciálním programem, kterému se říká model checker, a ten vyhodnotí, zda program specifikaci splňuje či nesplňuje. V případě nesplnění specifikace obdrží uživatel i popis místa, kde k porušení došlo.
Problémy
Výše popsaný přístup má však svá úskalí a zdaleka ho nelze aplikovat ve všech případech. Jednou z největších výzev je problém příliš velkého modelu – model checker není v takovém případě schopen v rozumném čase model zkontrolovat a ověřit jeho správnost. Zde je možné aplikovat různé optimalizační metody zahrnující jak rychlejší a efektivnější zpracování modelu, tak jeho vlastní reprezentaci.
Dalším palčivým problémem je takzvaná nerozhodnutelnost programů pro model che cking. To znamená, že existují programy, u nichž nemůže model checker vyhodnotit, jestli odpovídají nebo neodpovídají zadané specifikaci, byť by byl sebelepší. Východiskem z této situace je v mnoha případech nějaké omezení vstupního programu například tím, že nesmí používat výpočty s čísly s pohyblivou desetinnou čárkou, tedy smí používat v zásadě jen celá čísla. Programy, které tato omezení nesplňují, nelze automaticky verifikovat.
Výsledky
Nástupem rychlých počítačů s velkou operační pamětí se otevřely dveře pro verifikaci skutečných programů – velikost programů, které lze verifikovat, velmi vzrostla, a i když jsme zatím nedosáhli potřebné velikosti, jednodušší programy už ověřit umíme. Stále je tedy potřeba hledat lepší způsoby reprezentace programů( a odpovídajících modelů) a efektivnější metody kontroly. I druhý problém, nerozhodnutelnost model checkingu, poskytuje mnoho příležitostí k výzkumu. Zde se snažíme rozšířit množinu programů, které lze verifikovat tak, aby množství omezení kladených na verifikovaný program bylo co nejmenší.
Na základě výsledků našeho výzkumu jsme vytvořili vlastní model checker GMC( Gimple Model Checker), viz http:// d3s. mff. cuni. cz /~ sery / gmc /, pro verifikaci programů napsaných v jazyce C / C ++ a pracujeme již také na nástroji pro verifikaci zdrojových kódů aktivních webových stránek, používaných například v internetovém bankovnictví.
Informatika: Verifikace programů 85