Automatizált ellenőrzési technikák

VIMIMA29  |  Mérnökinformatikus MSc  |  Félév: 2  |  Kredit: 5

A tantárgy célkitűzése

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.

A tantárgy teljesítése után a hallgatók

  • Á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).
    • Vörös András
    Vörös András

    docens

    tárgyfelelős

    A tárgy oktatói

    Cziborová Dóra
    Cziborová Dóra

    doktorandusz

    Szekeres Dániel
    Szekeres Dániel

    doktorandusz

    Vörös András
    Vörös András

    docens

    A tantárgy részletes tematikája

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

    Áttekintés

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

    Szoftvertesztelés

    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).

    Logikai megoldó technológiák használata a verifikációban

    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.

    Statikus ellenőrzési technikák

    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ó.

    Szolgáltatásbiztonság vizsgálata

    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.

    Kitekintés

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

    14. Vendégelőadás és/vagy konzultáció

    A gyakorlatok részletes tematikája:

    1. Modellalapú tesztelés

    2. Forráskód alapú tesztgenerálás

    3. SAT/SMT megoldók alkalmazása

    4. Statikus kódellenőrzés

    5. Szoftverek modellellenőrzése

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