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ó    

    Szoftver verifikáció és validáció

    A tantárgy angol neve: Software Verification and Validation

    Adatlap utolsó módosítása: 2018. április 27.

    Budapesti Műszaki és Gazdaságtudományi Egyetem
    Villamosmérnöki és Informatikai Kar

    Műszaki Informatika Szak

    Doktorandusz képzés

     

    Tantárgykód Szemeszter Követelmények Kredit Tantárgyfélév
    VIMMD052   4/0/0/v 5 1/1
    3. A tantárgyfelelős személy és tanszék Dr. Majzik István, Méréstechnika és Információs Rendszerek Tanszék
    A tantárgy tanszéki weboldala http://www.mit.bme.hu/oktatas/targyak/vimmd052/
    4. A tantárgy előadója

    Név:

    Beosztás:

    Tanszék, Int.:

    dr. Majzik István

    egyetemi docens

    MIT

    6. Előtanulmányi rend
    Ajánlott:

    Nincs.

    7. A tantárgy célkitűzése

    A tantárgy célja a szoftverfejlesztésben tipikusan használt verifikációs és validációs technikák szisztematikus áttekintése. Az előadások tárgyalják a verifikáció és validáció klasszikus megoldásait (átvizsgálás, analízis, tesztelés), a formális verifikáció (modellellenőrzés, ekvivalencia ellenőrzés, helyességbizonyítás) matematikai alapjait, valamint a modell alapú tesztgenerálást. A hallgatók megismerik azokat a technikákat, amik a szoftverfejlesztés során a specifikáció, tervek, implementáció ellenőrzésére alkalmazhatók, különösen a modellalapú tervezés során.

    8. A tantárgy részletes tematikája

    1. A verifikáció és validáció szerepe a fejlesztési folyamatban:

    A verifikáció és validáció (V&V) szerepének és tipikus technikáinak áttekintése különféle fejlesztési módszertanok és szabványok esetén. A formális verifikáció szerepe.

    2. A specifikáció verifikációja:

    Az informális, fél-formális és formális specifikációs nyelvek áttekintése és kategorizálása. A specifikáció ellenőrzésének aspektusai (teljesség, konzisztencia, tesztelhetőség, megvalósíthatóság).

    3. Az architektúra tervek verifikációja:

    Az architektúra terv átvizsgálása: szisztematikus interfész és hibahatás analízis, architektúra trade-off analízis. A funkcionális és extra-funkcionális tulajdonságok (megbízhatóság, rendelkezésre állás, teljesítmény, biztonságosság) modell alapú analízise.

    4. A részletes tervek verifikációja:

    A tervek átvizsgálása. A viselkedési modellek formális verifikációja: modellellenőrzés, ekvivalencia ellenőrzés, helyességbizonyítás. A biztonsági és élőségi tulajdonságok specifikálása temporális logikákkal. Algoritmusok a temporális tulajdonságok ellenőrzéséhez. A viselkedési modellek nagy állapotterének hatékony kezelése szimbolikus technikákkal, inkrementális modellellenőrzéssel, részleges redukcióval. Absztrakciós technikák (predikátum absztrakció, ellenpélda vezérelt absztrakció finomítás). Részletes tervek ekvivalenciájának illetve finomítási relációinak ellenőrzése.

    Az extra-funkcionális (szolgáltatásminőségi) tulajdonságok modell alapú ellenőrzése.

    Időfüggő viselkedés formális verifikációja.

    5. Az implementáció verifikációja:

    Forráskód ellenőrzés: statikus analízis, forráskód metrikák használata, absztrakt interpretációval végzett verifikáció.

    Helyességbizonyítás a forráskód vagy részletes program reprezentáció alapján: Matematikai technikák (számítási és strukturális indukció). A programhelyesség és terminálás formalizálása. A helyesség bizonyítása egyszerű determinisztikus programok és strukturált nyelven írt programok esetén. A tételbizonyító eszközök tulajdonságai és használhatósági korlátai.

    6. Szoftvertesztelés:

    Egységtesztelés specifikáció alapú és struktúra alapú technikákkal. Adatfolyam alapú tesztelés. Integrációs tesztelés inkrementális és szcenárió alapú technikákkal. Teszt minőségi mértékek.

    Specifikus tesztelési technikák: GUI tesztelés, robusztusság tesztelés, OO szoftverek tesztelése. Forráskód alapú tesztelés, szimbolikus végrehajtás.

    Modell alapú tesztgenerálás programgráf alapú algoritmusokkal, modellellenőrzéssel, mutációs és evolúciós algoritmusokkal. A teszteléshez használt konformancia relációk. Kontextus-függő autonóm viselkedés modell alapú tesztelése (esettanulmány).

    7. Validáció:

    Validáció elemzéssel, teszteléssel, mérésekkel.

    Verifikáció és validáció változások és karbantartás esetén. Az újraverifikálás támogató technikái (programszeletelés, inkrementális tesztelés).

    9. A tantárgy oktatásának módja (előadás, gyakorlat, laboratórium)

    Előadás.

    10. Követelmények

    A szorgalmi időszakban: Egy otthoni feladat kidolgozása és bemutatása. A feladat elégséges teljesítése a feltétele az aláírás megszerzésének és a vizsgázásnak.

    A vizsgaidőszakban: Szóbeli vizsga.

    11. Pótlási lehetőségek

    Az otthoni feladat a pótlási időszakban pótolható.

    12. Konzultációs lehetőségek

    Vizsgák előtt, előre egyeztetett időpontban.

    13. Jegyzet, tankönyv, felhasználható irodalom

    Diasorok és prezentációk elektronikusan hozzáférhető formában (tantárgy web lapon).

    Gerard O'Regan: Concise Guide to Formal Methods: Theory, Fundamentals and Industry Applications. Springer, 2017.

    N. S. Godbole: Software Quality Assurance: Principles and Practices. 2nd edition, Alpha Science, 2016.

    B. Berard et. al.: Systems and Software Verification. Springer, 2007.

    G. G. Schulmeyer, G. R. MacKenzie: Verification and Validation of Modern Software-Intensive Systems. Prentice Hall, 2010.

    D. Peled: Software Reliability Methods. Springer, 2001.

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

     

    Kontaktóra

    56

    Félévközi készülés órákra

    14

    Otthoni feladat elkészítése

    25

    Kijelölt írásos tananyag elsajátítása

    15

    Vizsgafelkészülés

    40

    Összesen

    150

    15. A tantárgy tematikáját kidolgozta

    Név:

    Beosztás:

    Tanszék, Int.:

    dr. Majzik István

    egyetemi docens

    MIT