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