A biztonságkritikus rendszerek (pl. vasúti biztosítóberendezések, repülőgépek, kormányművek) helyes működésének szavatolása kulcsfontosságú, mert az azokban jelenlévő legkisebb hiba is súlyos anyagi kárral járhat, extrém esetekben emberi életekbe is kerülhet. A modellellenőrzés lehetőséget ad a tervezett rendszer helyességének bizonyítására és a hibák automatikus megtalálására, széleskörű felhasználását azonban hátráltatja nagy számításigénye, fontos megoldandó probléma tehát a modellellenőrző algoritmusok hatékonyságának javítása. Az önálló labor során ilyen algoritmusok fejlesztésére és optimalizálására nyílik lehetőség.