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.

Klasická verifikaceEditovat

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.

Formální verifikaceEditovat

 
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 Hoareho logiky.