model checking

Angol

model checking (tsz. model checkings)

(informatika) A model checking (magyarul: modellellenőrzés) egy automatikus formális verifikációs technika, amely segítségével egy rendszer formális modelljének minden lehetséges állapotát végigvizsgálják annak érdekében, hogy ellenőrizzék, teljesíti-e a kívánt tulajdonságokat (például helyességi vagy biztonsági követelményeket).

Egy formális modell (pl. véges állapotgép) segítségével reprezentáljuk a vizsgált rendszert.
Egy logikai formulát (pl. lineáris idő logika LTL vagy elágazó idő logika CTL) fogalmazunk meg a rendszer tulajdonságairól.
A model checker automatikusan megvizsgálja, hogy a modell kielégíti-e a formulát.
Ha nem, akkor hibapéldát (counterexample) ad, amely megmutatja, hol és hogyan sérül a tulajdonság.

Hardverek verifikációja (pl. processzormagok, vezérlők)
Szoftverek helyességének ellenőrzése (biztonsági protokollok, beágyazott rendszerek)
Kommunikációs protokollok vizsgálata

Modellalkotás: A rendszer viselkedését egy véges állapotgépben definiáljuk.
Specifikáció megadása: A kívánt tulajdonságokat formális logikában fejezzük ki.
Automatikus ellenőrzés: A model checker végigpróbál minden lehetséges állapotot és átmenetet.
Eredmény: Igaz vagy hamis, esetleg hibapéldával.

Fogalom	Leírás
Model checking	Automatikus formális rendszerellenőrzés
Alapja	Véges állapotgép modell + formális logikai specifikáció
Kimenet	Igazságérték vagy hibapélda