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 tá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 tá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.

1. A formális módszerek szerepe az informatikai rendszerek fejlesztésében (bevezető): formális követelmény-specifikáció, modellezés, verifikáció (modellellenőrzés, helyességbizonyítás) szerepe. Mérnöki és formális modellek kapcsolata, modell-leképzések. Formális módszereket alkalmazó tervezőrendszerek (példák).
2. Alapszintű formális modellek és szemantikájuk: Kripke struktúrák, tranzíciós rendszerek, Kripke tranzíciós rendszerek, időzített automaták és időzített automaták hálózata.
3. Követelmények formalizálása temporális logikákkal: Lineáris temporális logika (LTL), elágazó idejű temporális logikák (CTL, CTL*). A kifejezőképesség összehasonlítása.
4. Formális verifikáció modellellenőrzéssel: Modellellenőrzés tabló módszerrel, valamint szimbolikus technikákkal. Időfüggő viselkedés ellenőrzése.
   Kijelölt írásos tananyag: Tutorial on UPPAAL. https://uppaal.org/documentation/
5. Nagyméretű állapottérrel rendelkező modellek verifikációja: Az állapottér kezelése döntési diagramok használatával. Korlátos modellellenőrzés.
6. Gyakorlati alkalmazások: Beágyazott vezérlők és protokollok modellezése időzített automatákkal, temporális követelmények ellenőrzése az UPPAAL modellellenőrző használatával. Automatikus tesztgenerálás modellellenőrzővel. Monitor szintézis temporális logikai követelmények alapján.
7. Állapotfüggő viselkedés magas szintű modellezése: Állapottérképek formális szemantikája. Tervezés állapottérképek használatával, az állapottérképek verifikációja. Az állapottérkép alapú forráskód szintézis elterjedt megoldásai.
8. Konkurens rendszerek modellezése és viselkedési tulajdonságainak vizsgálata: A Petri háló formalizmus. Modellek dinamikus tulajdonságainak (holtpontmentesség, élőség, korlátosság, perzisztencia, visszatérő állapotok) ellenőrzése szimulációval és az elérhetőségi gráf alapján. Hierarchikus Petri hálók. Modellezési mintapéldák.
9. Konkurens rendszerek strukturális tulajdonságainak vizsgálata: Állapotokra és viselkedésre vonatkozó invariánsok, strukturális korlátosság és vezérelhetőség kifejezése és ellenőrzése. Tulajdonságmegőrző modell-redukciós technikák.
10. Adatfüggő viselkedés modellezése: Adattípusok és adatkezelés modellezése. A dinamikus és strukturális tulajdonságok kiterjesztése. Gyakorlati alkalmazások: Elosztott adatkezelés konzisztenciájának vizsgálata, protokollok analízise.
11. Extra-funkcionális tulajdonságok specifikálása és verifikációja: A Petri hálók kiterjesztése valószínűségi és idő jellemzőkkel: sztochasztikus Petri hálók. Követelmények formalizálása sztochasztikus analízishez, teljesítmény és megbízhatósági tulajdonságok vizsgálata.
12. Modellfinomítás: A szisztematikus modellfinomítás módszerei. A modellfinomítás konzisztenciájának ellenőrzése a viselkedésre vonatkozó relációk használatával.
13. Szoftver forráskód alapú formális verifikációs technikák: Modellellenőrzés C programokon. Absztrakció használata: statikus analízis absztrakt interpretációval, predikátum absztrakció, ellenpélda vezérelt absztrakció finomítás a modellellenőrzés során.
14. Program helyességbizonyítás: Kontraktusok, elő- és utófeltételek, invariánsok formalizálása, ellenőrzésük az algoritmusok magas szintű leírása illetve köztes reprezentációja alapján.