• Verifi kace
programů
Moti vace
Katedra distribuovaných
a spolehlivých systémů
http://d3s.mff.cuni.cz/
Přiblížit se co nejvíce k tomu, aby
počítačový program dělal to, co má,
lze pomocí testování a formální veri-
fi kace. K vlastním výsledkům v této
oblasti patří Gimple model checker,
který verifi kuje vlastnosti programů
napsaných v programovacím jazyce
C/C++, dále pak Web badger, který
verifi kuje zdrojové kódy aktivních
webových stránek
Výzkumná témata řešená v mezi-
národních projektech:
predikování výkonnosti programů,
sklá dání programů z komponent a slu -
žeb.
Dne 21. 9. 1997, nedaleko pobřeží u mě-
sta Cape Charles ve Virginii: během vojen-
ské ho cvi čení se americká vojenská loď
York towns, kódovým označením CG-48,
z nezná mých důvodů zastavila a skoro tři
hodiny zůstala nečinně stát na širém moři.
Jak se poté ukázalo, důvodem byla chyba
v obslužném programu – operátor omy lem
zadal do počítače jako jeden z úda jů nulu.
Dělení nulou způsobilo tzv. výji mku, která
nebyla odpovídajícím způ sobem ošetřena.
Ta byla propagová na na všechny počítače
v síti a jeden z nich pak vypnul motory.
Programy jsou dnes používány téměř
všu de a chy by v nich mohou mít daleko
závaž nější důsledky než vypnutí motorů
u vojenské lodi během manévrů. Jako pří-
klad lze uvést programové vybavení le ta -
del, medicínských přístrojů používaných
k operacím nebo programy ob slu hující in-
ternetové bankovnictví. Ve všech těch to pří-
padech je žádoucí, aby programy neobsa-
hovaly žádné chyby.
Testování a verifi kace
Jedním ze základních prostředků hledání
chyb v programu je testování – programá-
tor (tvůrce programu) opakovaně spouští
program a simuluje chování skutečných
uži vatelů. Tímto způsobem však nelze od-
ha lit všechny chyby; množství různých
cho vání uživatele může být enormní. Proto
je třeba programy tzv. verifi kovat. Verifi -
kace programu je jeho formální ověření,
tj. ověření na základě matematického dů-
kazu, že program neobsahuje žádné chy by,
případně že odpovídá zadané specifi kaci.
Aby mohl být program verifi kován, je nutné
vytvořit jeho model v nějakém mate ma tic-
kém systému.
84
Informati ka: Verifi kace programů