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.

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.

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

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.

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.

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.

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

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