Szoftver verifikáció és validáció - Segédanyagok

Félév: 2012. ősz
Cím	Egyedi szöveg
EA08: Sztochasztikus logikák	Sztochasztikus logikák
EA09: Időzített rendszerek modellezése és verifikációja	Időzített rendszerek modellezése. Időt kezelő temporális logikák.
EA10: Ekvivalencia ellenőrzés	Ekvivalencia ellenőrzés
EA11: Helyességbizonyítás egyszerű programok esetén	Helyességbizonyítás egyszerű programok esetén
EA12-13: Kitekintés: A modellellenőrzés korszerű módszerei	CEGAR Szaturáció Mintapélda
EA14: Helyességbizonyítás strukturált programok esetén	Helyességbizonyítás strukturált programok esetén
EA15: Forráskód verifikáció	Forráskód verifikáció
EA16: Absztrakció a verifikáció során	Absztrakció a verifikáció során
EA17: Tesztelés és teszttervezés modul/unit szinten	Modul/unit tesztelés
EA18: Integrációs- és rendszertesztelés	Integrációs- és rendszertesztelés
EA19: Speciális tesztelési feladatok	Speciális tesztelési feladatok
EA20: Relációk a teszteléshez	Tesztelési relációk
EA21: Modell alapú tesztelés	Modell alapú tesztelés
EA22: Szoftver karbantartás és értékelés	Szoftver karbantartás és értékelés
EA23: Eseményalapú rendszertervezés helyességbizonyítással (Event-B)	Modellfinomítás és ellenőrzése
EA24: A B módszer elemei	Programok szintézise A B módszer áttekintése A B módszer és az UML kapcsolata
JE01: Korábbi évek jegyzetei	Korábbi évek jegyzetei (háttéranyag)

Félév: 2011. ősz
Cím	Egyedi szöveg
EA01: Bevezető áttekintés	Az előadás témája: Motiváció Milyen minőségi igények vannak a szoftverrel szemben, és mit tud ma a szoftveripar? Miért olyan nagy a szoftver ellenőrzési technikák jelentősége? A verifikáció és validáció technikái (áttekintés) Milyen tipikus technikák vannak? Fejlesztési életciklus modellek Milyen szerepet kapnak a tipikus technikák az egyes fejlesztési folyamatokban? Fejlesztési szabványok szerepe Hogyan valósul meg a szisztematikus ellenőrzés? SZVV_EA01_intro.pdf
EA02: Követelmény-specifikáció készítés és ellenőrzés	Az előadás anyaga: A fázis ki- és bemenetei A szoftverkövetelmény-specifikáció elkészítése Formális nyelvek (áttekintés) Félformális és strukturált technikák Példa: SysML Ellenőrzési feladatok Általános szempontok és módszerek Teljesség és ellentmondás-mentesség Követelménykezelés Feladatok Automatikus eszközök SZVV_EA02_kovetelmenyek.pdf
EA03: Szoftver architektúra tervek ellenőrzése	Az előadás anyaga: A fázis ki- és bemenetei Az architektúra tervek elkészítése A komponensek azonosítása Mit határoz meg az architektúra? Ellenőrzési feladatok Követelményeknek való megfelelőség, követhetőség Hibahatások vizsgálata Extra-funkcionális követelmények vizsgálata Teszt tervezés SZVV_EA03_architektura.pdf
EA04: Részletes szoftver tervek ellenőrzése	Az előadás anyaga: A részletes tervek elkészítése Szoftver konstrukció Modul tervezés Ellenőrzések Verifikációs lépések Formális verifikáció Alapszintű formalizmusok KS, LTS, KTS Automaták SZVV_EA04_reszletes_tervezes.pdf
EA05: Hennessy-Milner logika, PLTL lineáris temporális logika és modellellenőrzése	Az előadás anyaga: Temporális követelmények A Hennessy-Milner logika Modellellenőrzés a tabló módszerrel A PLTL lineáris temporális logika Operátorok Modellellenőrzés automata-elméleti alapon A modellellenőrzés komplexitása SZVV_EA05_hml_ltl.pdf
EA06: Elágazó idejű temporális logikák és modellellenőrzésük	Az előadás anyag: CTL* szintaxis és szemantika CTL szintaxis és szemantika CTL modellellenőrzés a szemantika alapján Modális mu-kalkulus SZVV_EA06_ctl.pdf
EA07: Hatékony modellellenőrzés (az állapottér kezelése)	Az előadás anyaga: Szimbolikus modellellenőrzés CTL esetén Az ROBDD-k használata Részleges rendezés a PLTL modellellenőrzsé során SZVV_EA07_allapotter_kezeles.pdf
EA08: Korlátos modellellenőrzés	Az előadás anyaga: Korlátos modellellenőrzés SZVV_EA08_bounded_mc.pdf