Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Licenţă
Domeniul: Informatică
Programul de studii: Informatică – linia de studiu maghiară
Limba de predare: Maghiară

SYLLABUS

I. Általános adatok
Kód	Tantárgy neve	
MID0010	Szoftverrendszerek verifikációja és validációja
(Verificarea şi validarea sistemelor soft)	

Félév	Órák: C+S+L	Kategória	Típus	
6	2+1+1	szaktárgy	kötelező	

II. Foállásban az  Egyetem  oktatói
Név	Tudományos	Oktatói	Tanszék	Tevékenység	
	fokozat	státus		E	Sz	L	
SIMON Károly	Dr. 	Lect.	Limbaje şi Metode de Programare	*			

Társult oktatók
Név	Tudományos	Intézmény	Állás	Tevékenység 	
	fokozat		típusa	E	Sz	L	

III. A tantárgy célkitűzései
•	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 megfelelő V&V módszerek megismerése
•	A V&V folyamat során alkalmazott formális módszerek bemutatása	

IV. A tantárgy tartalma
•	A V&V folyamat általános bemutatása
•	Algoritmusok helyességének bizonyítása
•	Szoftverek átvizsgálása
•	Szoftverek tesztelése
•	Kritikus rendszerek validálása
•	Modellellenőrzés
•	Szoftverfejlesztési stratégiák és alkalmazott V&V módszerek
•	Rendszermodellek
•	V&V a gyakorlatban (modellek, tecchnológiák, eszközök)	

V. Könyvészet
1. Sommerville I., Szoftverrendszerek fejlesztése, Panem kiadó, Budapest, 2002
2. Patricza A., Formális módszerek az informatikában, Typotex kiadó, Budapest, 2006 
3. Frentiu M., Verificarea corectitudinii programelor, Ed.Univ."Petru-Maior", 2001.
4. ***, JUnit Documentation, http://www.junit.org	

VI. Az oktatói tevékenység heti tematikája
Előadásokon tárgyalt témák:

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

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

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

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

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

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

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)

8.	Hibakövető 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)

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

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
o	Kripke struktúrák
o	címkézett állapotátmeneti rendszerek
o	Kripke állapotátmeneti rendszerek
o	automaták
•	modell ellenőrzés

11.	Állapottérképek
•	UML állapottérképek
•	modellezés állapottérképpel
•	objektumok viselkedésének leírása állapottérképpel

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)

További információk:
    http://www.cs.ubbcluj.ro/~ksimon	

VII. Alkalmazott didaktikai módszerek
előadás, párbeszéd, gyakorlati feladatok, egyéni munka
az előadásokhoz tartozó jegyzetek kivetítése, a jegyzetek hozzáférhetővé tétele az Interneten	

VIII. Értékelés
A végső jegyet az alábbiakban leírtak szerint határozzuk meg: 
A. Évközi tevékenység (laborfeladatok, szemináriumi bemutató): 50% 
B. Írásbeli vizsga: 50%
Az elméleti jellegű írásbeli vizsgára a vizsgaidőszakban kerül sor. 
A tantárgy sikeres letételéhez minden részeredmény (A és B) esetében átmenő osztályzatot (5) kell elérni.	

IX. Kiegészítő 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.	Dijktsra 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.	Gries D., The Science of Programming, Springer-Verlag, Berlin, 1981.
6.	Hoare C.A.R., An axiomatic basis for computer programming, CACM, 12(1969), pg.576-580, 583.
7.	Manna Z., Mathematical Theory of Computation, McGrawHill, NewYork, 1974.	

	Dékán,						Tanszékvezető,

	Dátum,						Előadás felelőse,
								Lect. Dr. SIMON Károly