Automatizált ellenőrzési technikák

Automated Verification Techniques

A tantárgyleírás hatályossága

Hatályosság kezdete:

2026. March 21.

Hatályosság vége:

—

Tantárgy neve (magyarul, angolul)

Automatizált ellenőrzési technikák

Automated Verification Techniques

Tantárgykód

BMEVIMIMA29

Tantárgyjelleg

—

Képzési szint

—

Kurzustípusok és óraszámok (heti/féléves)

Kurzustípus	elmélet	gyakorlat	laboratóriumi gyakorlat
óraszám (heti)	2	1	0
jelleg (kapcsolt/önálló)	—	kapcsolt	—

Tanulmányi teljesítmény/értékelés típusa

vizsga

Tantárgy kreditértéke

Tantárgyfelelős

Vörös András

beosztás: egyetemi docens

elérhetőség: voros.andras@vik.bme.hu

Tantárgyat gondozó oktatási szervezeti egység

Mesterséges Intelligencia és Rendszertervezés Tanszék

Kar

Villamosmérnöki és Informatikai Kar

Tantárgy weboldala

http://www.mit.bme.hu/oktatas/targyak/VIMIMA29

Tantárgy elsődleges mintatantervi jellege

—

Közvetlen előkövetelmények – Erős előkövetelmény

nincs

Közvetlen előkövetelmények – Gyenge előkövetelmény

nincs

Közvetlen előkövetelmények – Párhuzamos előkövetelmény

nincs

Közvetlen előkövetelmények – Mérföldkő előkövetelmény

nincs

Közvetlen előkövetelmények – Kizáró feltétel

nincs

Célkitűzés

Tantárgyprogram

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

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

Tanulmányi eredmények

Ez a tantárgy a KKK rendeletben meghatározott, következő kompetenciák fejlesztését szolgálja:

Tudás

Nincsenek rögzített tanulási eredmények.

Képességek

Nincsenek rögzített tanulási eredmények.

Attitűd

Nincsenek rögzített tanulási eredmények.

Autonómia és felelősség

Nincsenek rögzített tanulási eredmények.

Oktatási módszertan

Előadás és gyakorlat.

Tanulástámogató anyagok

Online források

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.

A tantárgy teljesítéséhez ajánlott előzetes ismeretek

Tudás típusú kompetenciák

(azon előzetes ismeretek összessége, amelyek megléte nem kötelező, de a tantárgy eredményes teljesítését nagyban elősegíti)

Szoftvertesztelés, V&V, szoftverfejlesztési folyamatok.

Képesség típusú kompetenciák

(azon előzetes képességek és készségek összessége, amelyek megléte nem kötelező, de a tantárgy eredményes teljesítését nagyban elősegíti)

nincs

Ajánlott (nem kötelező) előzetesen megszerzendő kompetenciák

(azon ajánlott (nem kötelező) előzetesen megszerzendő kompetenciák összessége, amelyek jelentősen hozzájárulnak a tantárgy eredményes teljesítéséhez)

Szoftvertesztelés, V&V, szoftverfejlesztési folyamatok.

Általános szabályok

Követelmények: 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%. Pótlási lehetőségek: A házi feladatok pótlására, javítására és ismétlésére nincs lehetőség.

Teljesítményértékelési módszerek

Szorgalmi időszakban végzett teljesítményértékelések részletes leírása

Nincs megadva részletes értékelés.

Szorgalmi időszakban végzett teljesítményértékelések részaránya

Nincs megadva részarány.

Vizsgaidőszakban végzett teljesítményértékelések részletes leírása

Nincs megadva részletes értékelés.

Vizsgarészek részaránya

Nincs megadva részarány.

Érdemjegy megállapítása

Nincs megadva érdemjegy határ.

Jelenléti és részvételi követelmények

Nincs megadva jelenléti követelmény.

Javítás, ismétlés és pótlás különös szabályai

Nincs megadva.

Rövid leírás

Nincs megadva.

Részletes leírás

Nincs megadva.

Ajánlott tantárgyak

Nincs megadva.

A tantárgy elvégzéséhez szükséges tanulmányi munka

Nincs megadva munkaidő bontás.

Tantárgykövetelmények hatályossága

Tantárgykövetelmények hatályosságának kezdete:

—

Tantárgykövetelmények hatályosságának vége:

—

Tantervi elhelyezés

Nincsenek rögzített tantervi elhelyezések ehhez a tárgyverzióhoz.