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

    Belépés
    címtáras azonosítással

    vissza a tantárgylistához   nyomtatható verzió    

    Automatizált ellenőrzési technikák

    A tantárgy angol neve: Automated Verification Techniques 

    Adatlap utolsó módosítása: 2023. január 4.

    Budapesti Műszaki és Gazdaságtudományi Egyetem
    Villamosmérnöki és Informatikai Kar
    Mérnökinformatikus mesterképzés (MSc)
    Kritikus rendszerek mellékspecializáció
    Tantárgykód Szemeszter Követelmények Kredit Tantárgyfélév
    VIMIMA29   2/1/0/v 5  
    3. A tantárgyfelelős személy és tanszék Dr. Vörös András,
    A tantárgy tanszéki weboldala http://www.mit.bme.hu/oktatas/targyak/VIMIMA29
    4. A tantárgy előadója Dr. Vörös András egyetemi docens, MIT
    5. A tantárgy az alábbi témakörök ismeretére épít Szoftvertesztelés, V&V, szoftverfejlesztési folyamatok.
    6. Előtanulmányi rend
    Kötelező:
    NEM
    (TárgyEredmény( "BMEVIMIMA01", "jegy" , _ ) >= 2
    VAGY
    TárgyEredmény("BMEVIMIMA01", "FELVETEL", AktualisFelev()) > 0)

    A fenti forma a Neptun sajátja, ezen technikai okokból nem változtattunk.

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

    7. 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).
    8. 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
    9. A tantárgy oktatásának módja (előadás, gyakorlat, laboratórium) Előadás és gyakorlat.
    10. 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%.

     

    11. 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.
    12. Konzultációs lehetőségek Igény szerint a félév során.
    13. Jegyzet, tankönyv, felhasználható irodalom
    • 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.
    14. A tantárgy elvégzéséhez átlagosan szükséges tanulmányi munka
    Kontakt óra42
    Félévközi készülés órákra14
    Felkészülés zárthelyire 
    Házi feladat elkészítése36
    Kijelölt írásos tananyag elsajátítása18
    Vizsgafelkészülés40
    Összesen150
    15. A tantárgy tematikáját kidolgozta

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

    Dr. Semeráth Oszkár adjunktus, MIT

    Dr. Micskei Zoltán egyetemi docens, MIT