Overovanie modelov: Rozdiel medzi revíziami
Smazaný obsah Přidaný obsah
preklepy |
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
[[Kategória:Informatika]]
|