Formální verifikace
Z Wikipedie, otevřené encyklopedie
V oblasti počítačových systémů formální verifikace dokazuje nebo vyvrací správnost systému vzhledem k dané formální specifikaci nebo vlastnosti, použitím matematických formálních metod.
[editovat] Klasická verifikace
Pro hledání chyb v počítačových systémech se běžně používá testování nebo simulace. Tyto metody umožňují najít některé chyby, ale nelze pomocí nich zaručit, zda se v systému daná chyba nevyskytuje.
[editovat] Formální verifikace
Metody formální verifikace umožňují často automaticky ověřit, zda systém splňuje danou vlastnost nebo ne. Formální verifikace, na rozdíl od testování nebo simulace, bere v potaz všechna možná chování systému. Jsou tři základní metody formální verifikace:
- Equivalence checking (ověřování ekvivalencí): rozhoduje, zda je systém ekvivalentní se svou specifikací vzhledem k danému druhu ekvivalence v chování.
- Model checking (ověřování modelů): rozhoduje, zda systém splňuje danou vlastnost nebo ne. Pokud systém danou vlastnost nesplňuje, dokáže model checking ukázat protipříklad, tedy chování systému, které porušuje danou vlastnost.
- Theorem proving (dokazování vět): systém i jeho vlastnosti jsou vyjádřeny jako formule v některém ze systémů matematické logiky a theorem proving hledá důkaz vlastnosti. Tento proces zatím není plně automatický.
Ověřované vlastnosti jsou často popsány v temporálních logikách, jako jsou lineární temporální logika (anglicky linear temporal logic, LTL) nebo computational tree logic (CTL).
Některé programy funkcionálních jazyků mohou být formálně verifikovány použitím ekvivalencí a indukcí. Občas lze dokázat, že je kód imperativního jazyku správný neboli korektní, použitím Hoarovy logiky.
