Szoftver verifikáció és validáció

Senior Lecturer: 
István Majzik
Instructors: 
István Majzik

Aktuális információk

2017. szeptembertől a tárgy angol nyelven fut, az aktuális információk itt találhatók:
Software Verification and Validation

Információk 2016 őszén

A tantárgy célkitűzése

A tárgy célja a szoftverfejlesztésben használatos verifikációs és validációs módszerek rendszerező ismertetése. Ennek keretében a klasszikus verifikációs módszerek (felülvizsgálat, tesztelés) mellett hangsúlyosan tárgyalja a tipikus formális verifikációs technikák (modellellenőrzés, ekvivalencia ellenőrzés, helyességbizonyítás) matematikai alapjait, valamint a modell alapú tesztgenerálási módszereket is. Ezek segítségével lehetővé válik a tervek és az implementáció szisztematikus ellenőrzése, illeszkedve a modellvezérelt tervezéshez.

A tantárgy tematikájának áttekintése

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

  • Tervezési módszertanok és fejlesztési szabványok. A verifikáció és validáció helye, a tipikus technikák áttekintése. A formális módszerek szerepe.

2. Formális specifikáció

  • Formális specifikációs nyelvek szerepe, ezek csoportosítása: Modell-orientált nyelvek, processz-leíró nyelvek, logikai nyelvek, hibrid megközelítések.
  • Megbízhatósági és teljesítményjellemzők formális specifikációja.

3. A tervek verifikációja

  • A formális verifikáció szerepe. A formális verifikáció alapmódszerei: modell ellenőrzés, ekvivalencia ellenőrzés, tételbizonyítás. Az állapottér kezelésének módszerei (szimmetriák kihasználása, szimbolikus technikák).
  • Megbízhatósági és teljesítményjellemzők ellenőrzése: kapcsolódás a modellellenőrzés technikáihoz.
  • Program helyességbizonyítás. Matematikai alapmódszerek (strukturális és számítási indukció). Helyességi kritériumok megfogalmazása. Egyszerű determinisztikus programok bizonyítása (részleges helyesség és terminálás). A helyességbizonyítás gyakorlati eszközei (automatikus tételbizonyító rendszerek, kódverifikációs eszközök).

4. Az implementáció verifikációja és validációja

  • Szoftver tesztelési módszerek. Funkcionális és strukturális tesztelés. A vezérlési szerkezet tesztelése. Adatfolyam orientált tesztelés. Tesztminőségi mérőszámok.
  • Tesztelési stratégiák és folyamatok. Modulok tesztelése, izolációs tesztelés. Integrációs tesztelés és rendszertesztelés. Időfüggő viselkedés tesztelése.
  • Objektum-orientált rendszerek tesztelése. Speciális teszt fedettségi mértékek.
  • Automatikus teszttervezés és tesztgenerálás modell illetve formális specifikáció alapján.

Félévközi követelmények

Az aláírás megszerzésének feltétele egy referátum készítése "Szoftver verifikáció vagy validáció esettanulmány" témakörben.

A referátum 3 forma valamelyikében készíthető el:

  1. Kiselőadás tartása vetített fóliákkal az előadás órarendi időpontjában egy önálló feladatmegoldásról, választott verifikációs módszerrel és eszközzel.
    Az esettanulmány (mintapélda) a doktoranduszi tanulmányok során vagy más keretek között elvégzett verifikációs vagy validációs feladatot mutathat be.
    A kiselőadás mutassa be a problémát, a választott módszert és eszközt, valamint a megoldás tanulságait. A kiselőadás időtartama max. 20 perc.
  2. Kiselőadás tartása vetített fóliákkal az előadás órarendi időpontjában, egy irodalomból megismert esettanulmányról (mintapéldáról).
    A kiselőadás mutassa be a mintapéldában szereplő problémát, a felhasznált módszert és eszközt, valamint a megoldás tanulságait. A kiselőadás időtartama max. 20 perc.
    A mintapélda kiválasztása a hallgató feladata. Javasolt források például: a Springer kiadó "Software Tools for Technology Transfer" folyóirata, vagy a "Formal Methods for Industrial Critical Systems" konferencia sorozat.
  3. Írásos összefoglaló készítése egy irodalomból megismert esettanulmányról (mintapéldáról).
    Az összefoglaló 3-4 oldalban, magyar nyelven mutassa be a mintapéldában szereplő problémát, a felhasznált módszert és eszközt, valamint a megoldás tanulságait. 
    A mintapélda kiválasztása a hallgató feladata. Javasolt források például: a Springer kiadó "Software Tools for Technology Transfer" folyóirata, vagy a "Formal Methods for Industrial Critical Systems" konferencia sorozat.

Mindhárom lehetőség esetén fontos, hogy egy probléma modellezésének vagy egy szoftver elkészítésének bemutatása önmagában nem elegendő, kapcsolódnia kell V&V tevékenységnek is, amely érdekes és tanulságos megoldás.

Az 1. vagy 2. formájú referátum választását 2016. október 31-ig kérem jelezni a majzik@mit.bme.hu címre küldött levélben, megadva a bemutatni kívánt téma címét és rövid leírását. A kiselőadások időpontjainak beosztása ezután történik.

Az 1. vagy 2. formában teljesített referátum esetén a hallgató jogosultságot szerez arra, hogy a szóbeli vizsgán a vizsgakérdés-párok közül csak az egyikből vizsgázzon (a másik kérdésből a vizsga teljesítettnek minősül).

A korábbi évek referátumai megtekinthetők.