Szoftver verifikáció és validáció

Aktuális információk / Actual informations

2017. szeptembertől a tárgy angol nyelven fut, az aktuális információk itt találhatók /
From September 2017, the subject is in English, the course material is avalable here:
Software Verification and Validation

Információk 2016 őszén

• Tematika
• Félévközi követelmények
• Segédanyagok
• Vizsgakérdések
• Referátumok
• Korábbi évek referátumai (a régi web szerveren)

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.