Overovanie modelov: Rozdiel medzi revíziami

Smazaný obsah Přidaný obsah
Pokus9999 (diskusia | príspevky)
preklepy
Pokus9999 (diskusia | príspevky)
wikilinky
Riadok 1:
'''Overovanie modelov''' alebo '''model checking''' je automatizovaná [[metóda]] [[formálna verifikácia|formálnej verifikácie]] [[paralelný výpočet|paralelného]] systému s konečným počtom stavov. Kontroluje sa, či zadaný model vyhovuje [[formálna špecifikácia|š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álna logika|temporálnej logiky]]. Výsledkom verifikácie je odpoveď na otázku, či model spĺňa špecifikáciu. Ak nie, je k dispozícii proti-prikladprotipriklad (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í.
 
[[Kategória:Informatika]]