Overovanie modelov

z Wikipédie, slobodnej encyklopédie
Prejsť na: navigácia, hľadanie

Overovanie modelov alebo model checking je automatizovaná metóda formálnej verifikácie paralelného systému s konečným počtom stavov. Kontroluje sa, či zadaný model vyhovuje špecifikácii. Model sa zadáva ako systém prechodov stavov kde vrcholy sú stavy a postupnosť prechodov predstavuje vykonávanie správania sa modelu. Špecifikácia systému sa zadáva formulami temporálnej logiky. Výsledkom verifikácie je odpoveď na otázku, či model spĺňa špecifikáciu. Ak nie, je k dispozícii protipríklad (counter-example), ktorý predstavuje postupnosť prechodov, ktoré vedú k nedodržaniu konkrétnej temporálnej formule. Táto metóda kontroluje celý stavový priestor modelu a dokáže odhaliť množstvo zákerných chýb, ktoré su neodhaliteľné pri simulácii a testovaní.