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

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.

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

Előadás.

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.

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

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

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.