Správnost počítačových programů - očekávání a realita. Luboš Brim a Ivana Černá Fakulta informatiky, Masarykova univerzita, Brno Správnost a spolehlivost jsou fundamentální požadavky, které na moderní počítačové programy klademe. Notoricky známý příklad zavčas neodhalené chyby v procesoru Intel Pentium stál společnost Intel více než půl milionu dolarů. Vedle těchto slavných a mediálně zajímavých případů existuje nespočitatelné množství více či méně závažných chyb v programech, které jsou dnes již nepostradatelnou součástí mnoha produktů – počínaje pračkou, přes mobilní telefon a konče třeba automobilem. Mnohé z těchto chyb jsou časem odhaleny a opraveny, mnohé jsou v produktu přítomny nadále a my se s nimi naučíme žít. I když náklady na opravu těchto chyb nebyly nikdy spočítány, jsou vždy významné, nemluvě o nepřímých „nákladech“ v podobě ztráty důvěry v produkt apod. Není proto překvapující, že problematika správnosti a spolehlivosti počítačových programů, tj. výzkum a vývoj metod a technik, které by eliminovaly či alespoň významně snížili počet závažných chyb v programech, je jedním z centrálních témat současné informatiky. Jedním z nejčastěji používaných a také nejjednodušších způsobů, jak odhalit chyby v programech, je jejich testování. Testování spočívá v prostém vyzkoušení programu pro několik typických situací (vstupních dat). Problém je však v tom, že programy jsou natolik komplexní objekty, že množství situací, které by bylo žádoucí vyzkoušet, je tak obrovské, že jejich zpracování by trvalo roky, a to i v tom jednodušším případě. Není tedy možné provést dostatečně kompletní otestování programu, vždy je nutné některé situace vynechat a tím vynechat i případná problematická místa v chování programu. Testování tedy může odhalit chyby, ale nemůže garantovat jejich neexistenci. Je zajímavé, že i přes evidentní problémy s testováním, je tato technika stále tou hlavní, a bohužel často i jedinou, metodou, která má zaručit bezchybné chování programu. Naznačené potíže s testováním programů vedly k hledání takových metod, které by umožnily s velmi vysokou mírou jistoty zaručit bezchybné chování programů. Tou první byl pokus dokázat správnost programu, stejně tak, jako v matematice dokazujeme pravdivost matematických tvrzení. V ideálním případě bylo dokonce požadováno, aby takovýto důkaz bylo možné svěřit počítači, tj. aby byl vyvinut algoritmus, který by automaticky analyzoval zadaný program a buď konstatoval, že program je bez chyb či, v opačném případě, chyby odhalil. To vše navíc v rozumném čase. Je známo, že jenom pro triviální, a tedy prakticky zcela nezajímavé, programy, je možné takovýto automatizovaný postup skutečně realizovat. I přesto bylo mnoho lidí, kteří se dokazováním programů zabývalo, přesvědčeno, že je to právě tato technika, která jako jediná (i když možná ne plně automatizovaná) může odstranit problémy spojené s testováním. Již kolem roku 1960 začaly být vytvářeny první tzv. systémy pro dokazování vět, které však původní myšlenku dokazování programů naplňovaly pouze z poloviny. Tyto systémy byly totiž schopny potvrdit, že správný program je skutečně správný, ale pokud v programu byla chyba, pak systém neskončil výpočet, čili nebyl schopen
rozhodnout, ale pouze semi-rozhodnout. Zásadním nedostatkem systémů na dokazování vět tedy byla jejich neschopnost odhalovat chyby, byly to nástroje pro potvrzování správnosti. Z tohoto pohledu tedy nenahrazovaly testování, které právě naopak dokáže odhalovat chyby, ale neumí garantovat absenci chyb. Navíc se i ukázalo, že efektivní práce s těmito systémy vyžaduje vysoce kvalifikované a matematicky erudované specialisty. Je známou skutečností, že počet chyb na počátku vývoje programu je podstatně větší než ve fázi jeho finálního testování. Proto metody, které mohou potvrdit bezchybnost programu, ale mají velké problémy při odhalování chyb, jsou vhodnější pro závěrečné fáze výroby programu a méně vhodné pro počáteční fáze. Tyto metody jsou ale zpravidla i časově velmi náročné a oddalují den, kdy je možné program uvést na trh. V dnešním rychlém a konkurenčním světě, může byť jen malé zpoždění znamenat ztrátu trhu a to manažeři neradi vidí. Bylo proto nutné hledat takové metody, které by byly někde mezi testováním a dokazováním. Tyto metody by měly být automatizovatelné (není třeba zaměstnávat drahé experty a vše je mnohokrát rychlejší), měly by, podobně jako testování, odhalovat snadno chyby a (podobně jako dokazování) by měly být schopny podat evidenci, že v programu chyby nejsou. Takovéto metody je však marné hledat, pokud se neomezíme na nějaké speciální situace. Pozornost se proto zaměřila na programy, které jsou tzv. konečně-stavové. Na každý program lze nahlížet jako na zařízení, které má své vnitřní stavy (určené např. obsahem proměnných, které program používá) a tyto stavy mění během výpočtu. Z matematického hlediska se jistě jedná o zásadní omezení, na druhé straně však všechny programy, které jsou realizovány na digitálním zařízení, mají tuto vlastnost. Počet stavů ovšem může být enormní a to má nemalý vliv na efektivitu verifikačního procesu. K této otázce se vrátíme za chvíli. Nicméně, pro programy s konečným počtem stavů se podařilo očekávání skutečně naplnit (alespoň z velké části). V dnešní době, již existují průmyslově používané verifikační nástroje, které staví na právě uvedeném principu. Podstatným posunem je ovšem důraz na plnou automatizovatelnost procesu verifikace, čímž je jednak výrazně zvýšena produktivita tohoto procesu a také do značné míry odstraněna potřeba vysoce kvalifikovaných expertů pro tuto činnost. Již kolem roku 1975 se objevily první návrhy deduktivních systémů pro verifikaci konečně-stavových programů, přesněji řečeno konečných modelů programů. Tyto systémy byly založeny na použití tzv. temporálních logik. Temporální logiky jsou přirozeným rozšířením klasické výrokové logiky, kterou většina z nás dobře zná nejen ze školních lavic, ale v jistém slova smyslu ji máme „zakódovanou“ přímo v genech. Použití temporálních logik pro formulaci tvrzení o programech byl zásadním zvratem na cestě k automatizované verifikaci. Umožňuje totiž jednoduše vyjadřovat tvrzení o chování výpočetních systémů, jako např. „jestliže uživatel zadá příkaz pro tisk, pak je tisk někdy určitě proveden“. I když původně byly temporální logiky navrženy jako vhodný nástroj pro analýzu chování diskrétních událostí v programech, brzy se ukázalo, že je daleko důležitější konečně-stavový charakter těchto logik. Důvodem bylo, že všechna tvrzení v těchto logikách bylo možné rozhodnout pomocí jediného algoritmu
(rozhodovací procedury), který je založen na prostém prohledání odpovídajícího konečného modelu programu. Verifikaci lze plně automatizovat! Ještě však nebylo zcela vyhráno. V principu sice je možné vždy prohledat stavový prostor, ale to se nám nemusí v praxi vždy podařit proto, že nemáme dost výpočetních prostředků. Ukazuje se, že výpočetní složitost algoritmu, měřená v počtu kroků, které algoritmus pro svoji činnost vyžaduje, roste exponenciálně v závislosti na velikosti analyzovaného programu. Navíc ani nebylo realistické předpokládat, že tvůrci programů budou schopni a ochotni zapisovat svoje programy jako formule temporální logiky, což je při dokazování správnosti nutné učinit. I když tedy bylo možné, alespoň teoreticky, dokazovat formálně správnost programů, byl i nadále tento přístup spíše akademickou zajímavostí než praktickým nástrojem. Zásadní zvrat přišel v roce 1980. Nově objevený přístup nevyžadoval popsat jak program tak i jeho vlastnosti jako formule temporální logiky. Stačilo vytvořit konečně-stavový program modelující uvažovaný systém a v temporální logice popsat pouze vlastnost, jejíž pravdivost v tomto modelu bylo třeba ověřit. Zrodil se model-checking (přeloženo do češtiny jako technika ověřování modelu). Výpočetně se jednalo o jednodušší problém, protože za určitých omezení vyžadoval algoritmus pouze lineární zdroje (na rozdíl od exponenciálních, jako v případě dokazování) vzhledem k velikosti modelu. Stejně důležitá byla i skutečnost, že při ověřování modelu jsme schopni v případě negativní odpovědi produkovat i odpovídající protipříklad – zcela nepostradatelnou informaci pro opravu chyby v programu. Zavládlo velké nadšení, které se však ukázalo předčasné. Klíčovým místem byla velikost modelu. Počet stavů modelu závisí exponenciálně na počtu proměnných, které se v programu objevují. Tento jev se označuje jako „stavová exploze“. Výzkum se v dalších letech plně zaměřil na boj se stavovou explozí, tj. na hledání nejrůznějších metod a technik, které by umožnily tento problém zvládnout. V plné obecnosti se sice jedná o problém, který je neřešitelný, ale naštěstí je celá řada speciálních situací, ve kterých je možné za použití nejrůznějších heuristik uspět. Abychom lépe pochopili dále naznačená řešení, je vhodné podrobněji popsat, jak procedura pro ověřování modelu vlastně pracuje. Předpokládejme, že máme program a máme formuli temporální logiky, která vyjadřuje požadovanou vlastnost programu. Formule může například vyjadřovat vlastnost, že „kdykoli program uloží do proměnné V hodnotu 1, pak ji určitě v průběhu dalšího výpočtu zase změní zpět na hodnotu 0“. Smyslem verifikace nebo „ověření modelu“ je v tomto případě určit, zda tato formule je pravdivá pro daný program, neboli – řečeno jazykem matematické logiky – zda-li výpočty programu jsou „modelem“ formule. Pokud program používá jenom konečné množství paměti, lze na něj nahlížet jako na zařízení s konečným počtem stavů. Při tomto pohledu je model množina všech posloupností tvaru vstup/stav/výstup.
Model je vytvářen pomocí prohledávání, které začíná v počátečním stavu programu. K tomuto stavu jsou vygenerovány všechny stavy, do kterých se může program dostat po provedení jedné instrukce – po provedení jednoho přechodu. Pro každý stav může existovat velké množství přechodů, protože následný stav závisí na externím vstupu programu. Je-li program navíc „paralelní“, tj. počítá souběžně s jiným programem a přitom s ním komunikuje, je nutné za následnický stav brát i každý stav vyvolaný změnou stavu paralelně běžícího programu. Všechny tyto stavy mohou mít vliv na správnost programu a je tedy nutné je prozkoumat a zahrnout do modelu. Pro každý stav jsou takto vyhledány všechny jeho bezprostředně následnické stavy a ty, které nebyly již dříve vygenerovány, jsou uloženy do množiny stavů, které je nutné v dalším expandovat stejným způsobem. Tento postup je opakován tak dlouho, dokud jsou objevovány nové stavy. Prohledávání musí určitě skončit, neboť předpokládáme, že počet různých stavů je konečný a generování modelu skončí, jakmile je množina stavů, které mají být expandovány prázdná. Každý množný výpočet programu je tak reprezentován v modelu pomocí posloupnosti následných stavů. Ověření modelu pak spočívá v tom, že určíme, zda každá takováto posloupnost splňuje zadanou vlastnost a jestliže tomu tak není, pak vypíšeme na výstup (alespoň jednu) posloupnost, která vlastnost nesplňuje, tzv. protipříklad. I vygenerování protipříkladu je provedeno pomocí prohledávání. Vraťme se k příkladu znovu-nastavení proměnné V na hodnotu 0. Abychom vlastnost ověřili, označíme nejprve všechny stavy, ve kterých je hodnota proměnné V rovna nule. Pak se díváme zpět („proti směru výpočtu – proti času“) a označíme všechny stavy, které bezprostředně předcházely označený stav. Po jejich označení, opakujeme postup tak dlouho, dokud nedosáhneme „pevného bodu“, tj. situace, kdy není označen žádný nový stav. Tím jsme označili úplně všechny stavy, pro které každý následující výpočet určitě nastaví V na 0. Jestliže po označkování bude existovat stav, ve kterém je hodnota proměnné V rovna 1 a tento stav nebyl označen, pak formule neplatí. Takovýmto způsobem tedy algoritmus pro ověřování modelu ověřuje, zda program má požadovanou vlastnost a buď tuto skutečnost potvrdí, nebo ji vyvrátí podáním protipříkladu (viz Obr.1). Mohlo by se zdát, že za touto jednoduchou procedurou nemohou již být skryta žádná další úskalí. Bohužel ale jsou! Program, který je schopen uložit „zanedbatelných“ 250 bitů dat, má ve skutečnosti (alespoň) stavů, tedy více stavů než je částic ve vesmíru. Jakmile začne být vytvářený model natolik velký, že jej není možné umísti do operační paměti počítače, není možné popsaný postup přímo použít. Je nutné uplatnit výše zmíněné heuristiky ke zmenšení modelu. Nejjednodušší heuristiky, které se objevily, přímočaře formalizovaly techniky, které byly již dříve využívány v simulaci a testování: abstrakci nepodstatných částí modelu a využití hierarchické struktury a symetrií v programu. Jestliže např. víme, že jistá část programu nemá vliv na vlastnost, kterou ověřujeme (např. nemá vliv na hodnotu proměnné V z předchozího příkladu, a to ani nepřímý přes jiné proměnné), pak ji lze jistě eliminovat (provedená abstrakce tuto část programu zanedbá). Speciálním případem abstrakce je abstrakce dat. V tomto případě je namísto všech možných hodnot, kterých může nějaká proměnna nabývat, uvažováno jenom omezené (a malé) množství hodnot. Např. místo všech celých čísel, uvažujeme jenom dvě hodnoty: kladná a záporná. To lze samozřejmě udělat pouze
tehdy, jestliže takovéto zjednodušení nemá vliv na verifikovanou vlastnost. Metody, které jsou založeny na náhradě daného verifikačního problému jiným, výpočetně jednodušším, problémem při zachování správnosti řešení někdy označujeme jako redukční. Alternativním způsobem, jak přistoupit k zvládnutí velikosti stavového prostoru, je použít metodu pro symbolickou reprezentaci stavového prostoru. Trik spočívá v tom, že algoritmus nepracuje přímo s jednotlivými stavy, ale s množinami stavů. Výhoda spočívá v tom, že často je možné množinu stavů reprezentovat mnohem úsporněji než jednotlivé stavy. Symbolický ověřování modelu je založeno na tom, že množiny (stavů) lze ekvivalentně zadat pomocí výrokových formulí. Je-li například V proměnná v programu, pak formule „V=0“ vlastně definuje množinu všech stavů, ve kterých je hodnota proměnné V rovna 0. Tedy obrovská množina stavů, může být reprezentována velmi malou formulí. Verifikační algoritmus pak namísto se stavy pracuje s formulemi a reprezentuje tak příslušný stavový prostor nepřímo. Počáteční stav je také množina stavů a je proto reprezentován formulí. Rovněž množiny označených stavů jsou formule a zkoumání stavového prostoru je prováděno tak, že jsou manipulovány formule, nikoli stavy. Úspěšnost verifikačního algoritmu tak nezáleží na skutečné velikosti stavového prostoru, ale výlučně na kompaktnosti symbolické reprezentace. Symbolické ani redukční techniky nedávají garanci úspěchu. Není např. pravda, že symbolická reprezentace je vždy menší než explicitní. Často tomu tak však může být, zejména v situacích, kdy program vykazuje velkou míru „pravidelnosti“. To je zvláště typické pro HW systémy, kde je „program“ realizován jako technická součástka na čipu. Právě u HW systémů nacházíme na čipu tisíce tranzistorů, které jsou umístěny s určitou pravidelnou strukturou. Není proto překvapující, že symbolické techniky se zejména uplatňují při verifikaci hardwaru. Naproti tomu u softwaru jsou častěji úspěšné redukční techniky, zejména nejrůznější formy abstrakce. Přesto, že naznačené možnosti posunuly výrazným a doposud nebývalým způsobem možnosti automatizované verifikace blíže k reálným programům, existuje stále ještě mnoho situací, kdy problém stavové exploze brání verifikaci. Jsou to právě zcela praktické motivace, které nabízejí jiné taktiky, jak rozšířit použití verifikačních přístupů. Z praktického hlediska se zdá, že na verifikaci je často cennější odhalení chyb než důkaz o jejich neexistenci. Důvodů pro selhání programu může být mnoho a některé z nich jsou zcela mimo dosah verifikace. Jedním z nich je například fakt, že předpokladem pro verifikaci programu je správnost souvisejících programů. Jestliže tomu tak není, pak se nám celkem snadno může podařit dokázat správnost chybného programu. Navíc, pokud není zaručeně bezchybný způsob, jakým jsou návrhy programů implementovány, tj. jak je z předběžného logického návrhu systému pomocí implementační skriptu automatizovaně vytvořen výsledný program, lze ze správného návrhu vytvořit chybnou implementaci. Tento automatizovaný přechod od návrhu programu k implementaci je používán u hardwarových obvodů. V případě chyby procesoru u Intelu, použili návrháři špatný skript pro implementaci dělicí tabulky v Pentiu. Zatímco (logický) návrh tabulky byl určitě správný, její implementace do hardwaru pomocí uvedeného skriptu vedla k vynechání některých zásadních údajů v tabulce.
Jiným zajímavým efektem, který může automatizovaná formální verifikace přinést, je zvýšení produktivity práce a zkrácení doby nutné k uvedení produktu na trh (mimochodem i uspěchaný vývoj je jedním z důvodů tak časté chybovosti některých programů). Automatizovaná verifikace umožňuje rychlé a levné odhalování nejrůznějších chyb v programech, tyto chyby mohou být dokonce odhaleny velmi brzy již při prvotním návrhu programu a jejich odstranění je výrazně levnější, než nákladná náhrada produktu, který již bylo dodán zákazníkovi. Chyby v programech byly, jsou a budou. Programy jsou produkty lidského ducha a nelze je vyrábět automatizovaně, bez lidského zásahu. Po celou dobu moderní počítačové éry jsme svědky neustálého hledání takových postupů, které by chybovost programů eliminovaly či alespoň výrazně snížily. Kdykoli je objevena nějaká nová technika, jsou naše očekávání velká, zpravidla přehnaně velká. S narůstající složitostí programů se vždy ukázalo, že nový přístup má své hranice, že se nejedná o všelék. Realita je taková, že s dnešními možnostmi bychom mohli zaručit bezchybnost programů vytvořených před třiceti léty. K bezchybnosti dnešních programů potřebujeme metody, které teprve čekají na svoje objevení. Na druhé straně je však třeba říci, že bez dnešních metod by dnešní programy nebyly použitelné. Dnešní metody, a ověřování modelu je jednou z nich, výrazně snižují počet chyb v programech a zásadním způsobem eliminují podstatné chyby v programech – to vše za předpokladu, že výrobci tyto metody a postupy formální verifikace skutečně používají. Velké a rozumné firmy tak již činí.
