Overovanie modelov: Rozdiel medzi revíziami

'''Model checking''' je automatizová [[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 tzv. 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í.