A tantárgy adatlapja
1. A képzési program adatai
1.1 Felsőoktatási intézmény	Babeș–Bolyai Tudományegyetem	
1.2 Kar 	Matematika és Informatika Kar	
1.3  Intézet	Magyar Matematika és Informatika Intézet	
1.4 Szakterület	Informatika	
1.5 Képzési szint	Alapképzés	
1.6 Szak / Képesítés	Informatika	

2. A tantárgy adatai
2.1 A tantárgy neve	Szoftverrendszerek verifikációja és validációja	
2.2 Az előadásért felelős tanár neve	dr. Simon Károly	
2.3 A szemináriumért felelős tanár neve	dr. Simon Károly	
2.4 Tanulmányi év	3	2.5 Félév	2	2.6. Értékelés módja	vizsga	2.7 Tantárgy típusa	kötelező – szak	

3. Teljes becsült idő (az oktatási tevékenység féléves óraszáma)
3.1 Heti óraszám	4	melyből: 3.2 előadás	2	3.3 szeminárium/labor	1/1	
3.4 Tantervben szereplő össz-óraszám	48	melyből: 3.5 előadás	24	3.6 szeminárium/labor	12/12	
A tanulmányi idő elosztása:	óra	
A tankönyv, a jegyzet, a szakirodalom vagy saját jegyzetek tanulmányozása	30	
Könyvtárban, elektronikus adatbázisokban vagy terepen való további tájékozódás	30	
Szemináriumok / laborok, házi feladatok, portofóliók, referátumok, esszék kidolgozása	40	
Egyéni készségfejlesztés (tutorálás)	0	
Vizsgák	2	
Más tevékenységek: ..................	0	
3.7 Egyéni munka össz-óraszáma	102	
3.8 A félév össz-óraszáma	150	
3.9 Kreditszám	6	

4. Előfeltételek (ha vannak)
4.1 Tantervi	•	Nincs	
4.2 Kompetenciabeli	•	Algoritmika, programozás, fejlett programozási módszerek és környezetek, software engineering	

5. Feltételek (ha vannak)
5.1 Az előadás lebonyolításának feltételei	•	Videoprojektorral és táblával felszerelt előadóterem	
5.2 A szeminárium / labor lebonyolításának feltételei	•	Videoprojektorral és táblával ellátott szeminárium terem. Számítógépekkel felszerelt laborterem, a gépeken a megfelelő szoftverekkel (Java, Eclipse + megfelelő beépülő modulok) 	

6. Elsajátítandó jellemző kompetenciák
Szakmai kompetenciák	•	A verifikáció és validáció (V&V) fogalmainak megértése, az alkalmazott módszerek megismerése
•	Algoritmusok helyességével kapcsolatos fogalmak, valamint a helyesség bizonyítására használt módszerek megértése
•	Szoftverátvizsgálási módszerek megismerése
•	Tesztelés típusok, alkalmazott módszerek, eszközök és technológiák elsajátítása, alkalmazása a gyakorlatban
•	Kritikus rendszerek esetében alkalmazott fejlesztési stratégiák, valamint a megfelelo V&V módszerek megismerése
•	A V&V folyamat során alkalmazott formális módszerek bemutatása	
Transzverzális kompetenciák 	•	Önálló tanulás, kritikus gondolkodás, problémabeazonosítás és feladatmegoldás
•	A V&V folyamat fontosságának megértése, a minőségi standardok figyelembe vétele és betartása
•	Kritikus rendszerekkel, folyamatokkal kapcsolatos kihívások megismerése	

7. A tantárgy célkitűzései (az elsajátítandó jellemző kompetenciák alapján)
7.1 A tantárgy általános célkitűzése	•	A V&V folyamat megismerése
•	Algoritmusok helyességének bizonyítására alkalmazható módszerek elsajátítása
•	Szoftverátvizsgálási módszerek és stratégiák megismerése
•	Szoftvertesztelési módszerek megismerése és alkalmazása
•	Kritikus rendszerek validálásával kapcsolatos témakörök megismerése
•	A modellellenőrzés alapjainak elsajátítása
•	Szoftverfejlesztési stratégiák és alkalmazott V&V módszerek összekapcsolása
•	Rendszermodellek megértése
•	V&V a gyakorlatban (modellek, technológiák, eszközök)	
7.2 A tantárgy sajátos célkitűzései

	•	Algoritmusok helyességének bizonyítására alkalmazható alapvető módszerek megismerése (Floyd, Hoare stb.)
•	Tesztelési módszerek és keretrendszerek megismerése (JUnit, GUI tesztelési eszközök, teszteléssel kapcsolatos Eclipse beépülő modulok stb.)
•	Nagyvállalatoknál is alkalmazott átvizsgálási módszerek elsajátítása
•	Minőségi mutatókkal és monitorizálással kapcsolatos eszközök megismerése (Sonar stb.)
•	Alapvető rendszermodellek és modellezési eljárások elsajátítása	

8. A tantárgy tartalma
8.1 Előadás	Didaktikai módszerek	Megjegyzések	
1.	Verifikáció és validáció: általános bevezető
•	a verifikáció és validáció fogalmak
•	szoftverfejlesztési stratégiák, a V&V helye a fejlesztési folyamatban
•	statikus és dinamikus V&V módszerek
•	elfogadási szint
•	debugging
•	V&V tervezés	magyarázat, vetítés, konverzáció, példák		
2.	Algoritmusok helyességének bizonyítása
•	algoritmusok végrehajtása
•	algoritmusok helyessége
•	a Floyd módszer a helyesség bizonyítására
•	a Hoare módszer a helyesség bizonyítására	magyarázat, vetítés, konverzáció, példák		
3.	Szoftverek átvizsgálása
•	általános tudnivalók
•	programátvizsgálási stratégiák
•	hiba típusok (hibák listája - checklist)
•	automatizált statikus elemzés	magyarázat, vetítés, konverzáció, példák		
4.	Cleanroom szoftverfejlesztés
•	általános tudnivalók, történeti áttekintő
•	a Cleanroom megközelítés jellemzői
•	a Cleanroom folyamat modellje
•	Cleanroom szoftverfejlesztés
•	alkalmazott modellek és eszközök	magyarázat, vetítés, konverzáció, példák		
5.	Szoftvertesztelés
•	a tesztelési folyamat
•	komponensek tesztelése és integrációs tesztelés
•	funkció-orientált és objektum-orientált rendszerek tesztelése
•	hiányosságtesztelés
•	tesztesetek
•	fekete doboz tesztelés
•	ekvivalenciaosztályozás
•	struktúrateszt (fehér-/üvegdoboz tesztelés)
•	útvonaltesztelés
•	integrációs tesztelés
•	interfésztesztelés
•	stressztesztelés	magyarázat, vetítés, konverzáció, példák		
6.	Objektumorientált tesztelés
•	az objektumorientált és a funkcionális modell összehasonlítása
•	az objektumorientált tesztelés szintjei
•	objektumosztály tesztelése
•	objektumintegráció
•	forgatókönyv alapú tesztelés
•	tesztelési eszközrendszerek	magyarázat, vetítés, konverzáció, példák		
7.	Unit tesztelés (Unit Testing)
•	általános tudnivalók
•	unit testing Java-ban, a JUnit
•	a Fixture fogalom
•	Test Suite létrehozása, alkalmazása
•	az Eclipse által biztosított JUnit támogatás
•	JUnit alapú tesztelés Eclipse környezetben (példa)	magyarázat, vetítés, konverzáció, példák		
8.	Hibakövető és monitorizáló rendszerek
•	fejlesztési stratégiák bonyolultabb projektek esetében
•	csapatmunka (SVN rendszerek alkalmazása)
•	hibák jelentése, követése (bug reporting/bug tracking rendszerek, a Bugzilla bemutatása)
•	minőségi mutatókkal és monitorizálással kapcsolatos eszközök (Eclipse beépülő modulok, Sonar stb.)	magyarázat, vetítés, konverzáció, példák		
9.	Kritikus rendszerek validálása
•	kritikus rendszerek verifikálása és validálása
•	formális módszerek és kritikus folyamatok
•	megbízhatóság validálása
•	működési profilok
•	a megbízhatóság előrejelzése
•	biztonságosság szavatolása
•	biztonsági indoklások
•	a folyamat szavatolása
•	a védettség értékelése	magyarázat, vetítés, konverzáció, példák		
10.	Temporális logikák és modellellenőrzés
•	temporális logikák
•	temporális logikák osztályozása
•	temporális logikák modelljei
•	Kripke struktúrák
•	címkézett állapot-átmeneti rendszerek
•	Kripke állapot-átmeneti rendszerek
•	automaták
•	modell ellenorzés	magyarázat, vetítés, konverzáció, példák		
11.	Állapottérképek
•	UML állapottérképek
•	modellezés állapottérképpel
•	objektumok viselkedésének leírása állapottérképpel	magyarázat, vetítés, konverzáció, példák		
12.	Modellezés adatfolyam hálókkal
•	az adatfolyam módszer
•	adatfolyam hálók
•	adatfolyam hálókon alapuló workflow menedzsment (modellezés és analízis)	magyarázat, vetítés, konverzáció, példák		
Könyvészet
1. BALANESCU T., Corectitudinea programelor, Editura tehnica, Bucuresti 1995.
2. DIJKSTRA, E., A constructive approach to the problem of program correctness, BIT, 8(1968), pg.174-186.
3. DIJKSTRA, E., Guarded commands, nondeterminacy and formal derivation of programs, CACM, 18(1975), 8, pg.453-457.
4. DROMEY G., Program Derivation. The Development of Programs From Specifications, Addison Wesley Publishing Company, 1989.
5. FRENTIU, M., Verificarea corectitudinii programelor, Ed.Univ."Petru-Maior", 2001.
6. GRIES, D., The Science of Programming, Springer-Verlag, Berlin, 1981.
7. HOARE, C.A.R., An axiomatic basis for computer programming, CACM, 12(1969), pg.576-580, 583.
8. Morgan, C., Programing from Specifications, Prentice Hall, NewYork, 1990.	
8.2 Szeminárium / Labor	Didaktikai módszerek	Megjegyzések	
Szeminárium:			
-	a V és V folyamattal kapcsolatos feladatok megoldása, csoportos tevékenység
-	hallgatók bemutatói: a témakörrel kapcsolatos eszközök, módszerek, standardok bemutatása, esettanulmányok (prezentációk)
-	hallgatók bemutatóinak értékelése, megbeszélése
-	az aktuális lehetőségek függvényében: esettanulmányok bemutatása, cégek képviselőinek bevonásával 	egyéni bemutatók, konverzáció, (egyéni és csoportos) feladatmegoldás 		
Labor + projekt:			
1.	Az Eclipse környezetek V és V folyamattal kapcsolatos eszközeinek megismerése, használatuk bemutatása egy tetszőleges példaalkalmazás alapján
2.	Szoftverátvizsgálás: csoportos gyakorlat
3.	Statisztikai tesztelés: csoportos gyakorlat
4.	A JUnit keretrendszer alkalmazása
	Egyéni és csoportos feladatmegoldás		
Könyvészet	
1.	***, The Java Tutorial, Sun Microsystems, Inc, 2004. http://java.sun.com/docs/books/tutorial/index.html
2.	***, Eclipse Documentation, Eclipse Foundation, 2009.
http://www.eclipse.org/documentation/
3.	***, JUnit Documentation
http://www.junit.org/	

9. Az episztemikus közösségek képviselői, a szakmai egyesületek és a szakterület reprezentatív munkáltatói elvárásainak összhangba hozása a tantárgy tartalmával.
•	A tantárgy tematikája nagy átfedést mutat az egyetemi oktatásban a fontosabb egyetemeken oktatott hasonló tematikájú tantárgyak tartalmával.
•	A tananyagok kidolgozása nemzetközileg elismert szerzők munkái alapján történt, az ajánlott könyvészet szintén a terület releváns munkái alapján van összeállítva.
•	A tantárgy keretein belül oktatott témák szükségesek a szoftverfejlesztői iparban történő elhelyezkedéshez, a cégek elvárják az ilyen jellegű ismereteket.	

10. Értékelés
Tevékenység típusa	10.1 Értékelési kritériumok	10.2 Értékelési módszerek	10.3 Aránya a végső jegyben	
10.4 Előadás 	Vizsgafeladatok, bemutatott fogalmak és módszerek ismerete	Írásbeli vizsga	50%	
				
10.5 Szeminárium / Labor	Laborfeladatok és szemináriumi bemutató	A megoldások és a bemutató pontozása	50%	
				
10.6 A teljesítmény minimumkövetelményei	
Az átmenő jegy feltételei:
•	A végső jegyet meghatározó minden komponens esetén kötelező az átmenő jegy (min. 5-ös).
•	A végső jegy minimálisan 5-ös.	
Kitöltés dátuma			Előadás felelőse			Szeminárium felelőse
2012.09.25				dr. Simon Károly			dr. Simon Károly
Az intézeti jóváhagyás dátuma				Intézetigazgató	
..........................						dr. Szenkovits Ferenc