Formální verifikace

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

Princip model checkingu

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.