Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Licenţă
Domeniul: Calculatoare şi tehnologia informaţiei
Programul de studii: Ingineria informatiei - in limba maghiara
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)

Szemináriumi tevékenység:
•	különböző szervezeteknél alkalmazott V&V módszerek, standardok, stratégiák bemutatása
•	esettanulmányok bemutatása
•	hallgatók dolgozatainak bemutatása: a félév folyamán minden hallgatónak el kell készítenie egy a tárgy tematikájával kapcsolatos dolgozatot, amelyet egy adott szemináriumon bemutat társainak

Gyakorlati tevékenység (laborórák feladatai):
•	az előzőekben tanult módszerek ismétlése (L1, L2)
•	debugging Eclipse környezetben (L3, L4)
•	szoftverátvizsgálás a gyakorlatban (átvizsgáló csoportok kialakítása, egy konkrét alkalmazás átvizsgálása, a folyamat dokumentálása, következtetések) (L5, L6)
•	szoftvertesztelés (L7, L8): egy konkrét projekt esetében a teszttervek elkészítése, tesztelés, a folyamat és az eredmények dokumentálása (alapul szolgálhat egy korábban, pl. a közös projekt tantárgy keretein belül elkészített projekt), különböző tesztelési típusok alkalmazása
•	hibakövető rendszer alkalmazása (pl. az előző feladat projektjeinek valamelyikéből kiindulva, csoportokba szerveződve) (L8, L9)
•	unit tesztelés a gyakorlatban (JUnit alkalmazása Eclipse környezetben) (L11, L12)

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