Validace modelu

Aktuální verze stránky ještě nebyla zkontrolována zkušenými přispěvateli a může se výrazně lišit od verze recenzované 26. srpna 2019; kontroly vyžadují 2 úpravy .

Model checking ( model checking , anglicky  model checking ) je metoda automatického formálního ověřování paralelních systémů s konečným počtem stavů, umožňuje kontrolovat, zda daný model systému splňuje formální specifikace.

Jako model se obvykle používá tzv. Kripkeho model , který je formálně definován následovně: , kde  je množina stavů,  je množina počátečních stavů,  je přechodový poměr,  je označovací funkce.

Specifikace jsou obvykle uvedeny v jazyce formální logiky. Pro specifikaci hardwaru a softwaru se zpravidla používá temporální logika  - speciální jazyk, který umožňuje popsat chování systému v čase.

Důležitou otázkou specifikace je úplnost. Metoda kontroly modelu umožňuje ověřit, že model navrhovaného systému odpovídá dané specifikaci, nelze však určit, zda daná specifikace pokrývá všechny vlastnosti, které musí systém splňovat.

Hlavní úskalí, kterou je třeba v průběhu testování na modelech překonat, souvisí s kombinatorickým efektem exploze ve stavovém prostoru. K tomuto problému dochází v systémech s mnoha komponentami, které se vzájemně ovlivňují, a také v systémech s datovými strukturami, které mohou nabývat velkého počtu hodnot.

Nástroje

Poznámky

  1. ↑ Zing . Získáno 18. července 2018. Archivováno z originálu 18. července 2018.

Literatura

Odkazy