A tantárgy olyan intelligens ellenőrzési technikákkal ismerteti meg a hallgatókat, amik manapság már automatizált eszközökben is elérhetők és amelyekkel garantálható a szoftverintenzív rendszerek minősége. Ilyen technikákra manapság már nem csupán a kritikus rendszerek esetén van szükség (ahol ezek alkalmazását legtöbbször szabvány írja elő), hanem már olyan mindennapi informatikai rendszerekben is elterjedtek, mint a fejlesztő eszközökben lévő elemzések vagy a felhő platformok és az üzleti információs rendszerek.

Átlátják az ellenőrzési folyamatokat, és ismerik, hogy az egyes fejlesztési fázisokban mely technikák alkalmazása javasolt.

Képesek alkalmazni különböző tesztgenerálási technikákat.

Ismerik az automatizált ellenőrzéshez szükséges népszerű matematikai és logikai következtetési módszereket és képesek ezek verifikációban történő alkalmazására.

Ismerik a különböző statikus szoftverellenőrzési technikákat, és képesek statikus ellenőrző eszközöket feladatspecifikusan használni forráskódok átvizsgálására.

Ismerik az extrafunkcionális jellemzők elemzésére használható módszereket (pl. megbízhatóság modellezése és vizsgálata).

Az előadások részletes tematikája:

1. Különböző ellenőrzési módszerek áttekintése és helyük az informatikai fejlesztési folyamatokban.

2. Tesztelési módszerek és orákulumok (teszt orákulumok fajtái és szerepük a V&V során, metamorfikus tesztelés, regressziós tesztelés). Struktúra alapú teszttervezés (összetett lefedettségi kritériumok).

3. Modellalapú tesztgenerálás (tesztgenerálási algoritmusok, MBT folyamat, lefedettségi kritériumok).

4. Kód alapú tesztgenerálás (véletlen tesztgenerálás, fuzzing, dinamikus szimbolikus végrehajtás).

5. Verifikációs problémák leképezése formális logikai és matematikai problémákra. Logikai megoldók fajtái és tipikus felhasználásuk: IP, LP és SAT megoldók.

6. Elsőrendű logikai feladatok a programverikációban, SMT megoldók felépítése és felhasználása.

7. Hatékony verifikáció komplex és objektumorientált programkódokhoz (bitvektor, tömbök, mutatók, aritmetikai műveletek). SMT megoldók szükséges mögöttes elméletei.

8. A forráskódon használható statikus analízis eszközök típusai. Ellenőrzés által detektált tipikus hibák. Ellenőrzési módszerek és tulajdonságaik.

9. Szoftverek modellellenőrzése (vezérlési struktúra és adatfolyam ellenőrzése, formalizmusok szoftverkódok reprezentálására).

10. Statikus ellenőrzési módszerek és algoritmusok: absztrakt interpretáció, moduláris verifikáció.

11. Szolgáltatásbiztonsági követelmények modellezése (dinamikus hibafa, Markov-láncok).

12. Szolgáltatásbiztonsági követelmények ellenőrzése, kvalitatív és kvantitatív analízis.

13. Esettanulmányok: Blokklánc és mesterséges intelligencia alapú rendszerek ellenőrzése

A gyakorlatok részletes tematikája:

6. Szolgáltatásbiztonság modellezése és ellenőrzése