Szoftver verifikáció és validáció

A tantárgy angol neve: Software Verification and Validation

Adatlap utolsó módosítása: 2007. január 31.

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

5. A tantárgy az alábbi témakörök ismeretére épít

Programozás technológiája.

6. Előtanulmányi rend
Ajánlott:

Nincs.

7. A tantárgy célkitűzése

A tárgy célja a professzionális szoftvertervezésben használatos formális specifikációs nyelvek, verifikációs módszerek és validációs technikák rendszerező ismertetése. Ennek keretében hangsúlyosan tárgyalja a tipikus formalizmusok és módszerek matematikai alapjait (formális nyelvek és szemantikák) valamint a korszerű tesztelési módszereket. Segítségükkel lehetővé válik algoritmusok és adatstruktúrák precíz leírása, tulajdonságaik bizonyítása és elemzése.

8. A tantárgy részletes tematikája

1. A verifikáció és validáció szerepe a tervezési folyamatban. A szoftver minőség és ennek mértékei, a program és a dokumentáció minősége. Tervezési módszertanok és fejlesztési szabványok. 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.

Objektum-orientált specifikációs nyelvek.

Megbízhatósági és teljesítményjellemzők formális specifikációja (sztochasztikus logika).

3. Verifikáció: A formális szemantika szerepe. A formális verifikáció alapmódszerei: modell ellenőrzés, ekvivalencia ellenőrzés és tételbizonyítás. Az állapottér kezelésének módszerei (szimmetriák kihasználása, BDD). A tételbizonyítás és a temporális logikai modell ellenőrzés összekapcsolása.

Megbízhatósági és teljesítményjellemzők ellenőrzése: szoftver megbízhatósági modellek, kapcsolódás a modell ellenő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). Kompozicionális bizonyítás. A helyességbizonyítás gyakorlati eszközei (automatikus tételbizonyító rendszerek, kódverifikációs eszközök).

4. Validáció: Szoftver tesztelési módszerek. Hibamodellek és érvényességi körük. Funkcionális és strukturális tesztelés. A vezérlési szerkezet tesztelése. 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őzítési szempontok és tesztelésük.

Objektum-orientált rendszerek tesztelése. Wrapper osztályok használata. Öröklésfüggő, állapotfüggő, szálfüggő lefedettség. Statisztikai tesztelés OO rendszerekben.

Automatikus teszttervezés modell illetve formális specifikáció alapján.

9. A tantárgy oktatásának módja (előadás, gyakorlat, laboratórium)

(előadás, gyakorlat, laboratórium):

Előadás.

10. Követelmények
  1. A szorgalmi időszakban:
    A félév végi aláírás feltétele referátum készítése és bemutatása adott témakörből, kiadott irodalom (cikkek) alapján.
  2. A vizsgaidőszakban: Szóbeli vizsga.
  3. Elővizsga: Nincs.
11. Pótlási lehetőségek

A félévközi követelmények a vizsgaidőszak első három hetében pótolhatók. A referátum pótlása a vizsgaidőszakban csak írásban történhet.

A korábban megszerzett aláírások érvényesek.

12. Konzultációs lehetőségek

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

13. Jegyzet, tankönyv, felhasználható irodalom
  • Óravázlatok elektronikusan hozzáférhető formában (tantárgy web lapon).
  • Majzik I.: Formális verifikáció. Elektronikus jegyzet, BME MIT, 2001.
  • Sziray J., Majzik I., Benyó B., Pataricza A., Góth J., Kalotai L., Heckenast T., Nagy N.: Szoftver rendszerek minőségbiztosítása és verifikálása. Elektronikus jegyzet, 2000.
  • N. Francez: Program Verification. Addison-Wesley, 1992.
  • G. G. Schulmeyer, G. R. MacKenzie: Verification and Validation of Modern Software-Intensive Systems. Prentice Hall, 2000.
  • D. Peled: Software Reliability Methods. Springer-Verlag, 2001.
  • E. M. Clarke, O. Grumberg, D. Peled: Model Checking. MIT Press, 2000.
  • G. Holzmann: Design and Validation of Computer Protocols. Prentice Hall, 1991.
14. A tantárgy elvégzéséhez átlagosan szükséges tanulmányi munka

(a tantárgyhoz tartozó tanulmányi idő körülbelüli felosztása a tanórák, továbbá a házi feladatok és a zárthelyik között (a felkészülésre, ill. a kidolgozásra átlagosan fordítandó/elvárható idők félévi munkaórában, kredit x 30 óra, pl. 5 kredit esetén 150 óra)):

 

Kontakt óra

60

Félévközi készülés órákra

10

Felkészülés zárthelyire

0

Referátum 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

dr. Pataricza András

egyetemi docens

MIT