Az informatikai rendszerek bonyolultságának és a potenciális hibák kockázatának növekedésével
mindinkább elvárás az, hogy a kritikus funkciók tervezése és megvalósítása bizonyítottan helyes
(hibamentes) legyen. Ennek egyik jellegzetes megoldása a formális módszereket alkalmazó fejlesztés:
formális modellek biztosítják a követelmények és tervek egyértelmű és precíz rögzítését, formális
verifikációval vizsgálhatók a tervezői döntések és bizonyíthatók a tervek egyes tulajdonságai, az
ellenőrzött tervek pedig alapját képezhetik a forráskód szintézisnek. A tantárgy áttekintést ad az
informatikai rendszerek formális modelljeinek megalkotásához és analíziséhez szükséges
számításelméleti háttérről, ideértve a legfontosabb modellezési nyelveket, valamint a kapcsolódó
analitikus és szimulációs vizsgálati módszereket. A tantárgy demonstrálja a formális módszerek
alkalmazását a követelmény-specifikáció, a rendszer- és szoftvertervezés, a modell alapú verifikáció,
valamint a forráskód szintézis területén.
A tantárgy követelményeit eredményesen teljesítő hallgatók
(1) megismernek és alkalmazni tudnak különböző formális módszereket,
(2) képesek lesznek nem-formális rendszerleírások alapján formális modellt alkotni,
(3) tisztában lesznek a formális verifikációs technikák előnyeivel és korlátaival,
(4) megismernek formális módszereket támogató alapvető eszközöket.