Budapest University of Technology and Economics, Faculty of Electrical Engineering and Informatics

A kötelező előtanulmányi rend az adott szak honlapján és képzési programjában található.

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

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

Szorgalmi időszakban:

A félév végi aláírás feltétele a tárgy gyakorlatainak témájához kapcsolódó otthoni feladatok megfelelő színvonalú elkészítése.
Az otthoni feladatok legalább kétharmadát (4 darab a lehetséges 6 feladat közül) kell teljesíteni az adott feladaton kapható pontok legalább 40%-ának elérésével.

Vizsgaidőszakban:

Szóbeli vizsga.
A félév végi osztályzatban a házi feladatokra kapott pontszám súlya 20%.

• G. G. Schulmeyer, G. R. MacKenzie. Verification and Validation of Modern Software-Intensive Systems. Prentice Hall, 2000.
• N. G. Leveson: Safeware: System Safety and Computers. Addison Wesley, 1995
• G. J. Myers, C. Sandler. The Art of Software Testing. John Wiley & Sons, 2004.
• M. Broy, B. Jonsson, J.-P. Katoen, M. Leucker, A. Pretschner. Model-Based Testing of Reactive Systems: Advanced Lectures (Lecture Notes in Computer Science). Springer-Verlag, 2005.

Dr. Vörös András egyetemi docens, MIT

Dr. Semeráth Oszkár adjunktus, MIT