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á 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.

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. +more 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. +more 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 jazyka správný neboli korektní, použitím +more_A. _R. _Hoare'>Hoareho logiky.

Kategorie:Programování Kategorie:Aplikovaná matematika