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 romana
Limba de predare: Română

SYLLABUS

I. Date generale
Codul	Disciplina	
MID0010	Verificarea şi validarea sistemelor soft	

Semestrul	Ore: C+S+L+P	Categoria	Statutul	
6	2+1+1+0	specialitate	obligatorie	

II. Cadre didactice cu norma de bază în Universitate
Numele şi	Titlul	Gradul	Catedra	Tipul activităţii	
prenumele	ştiinţific	didactic		C	S	L	
VESCAN Andreea		Asist.	Limbaje şi Metode de Programare	*			

Cadre didactice asociate
Numele şi	Titlul	Instituţia	Tipul	Tipul activităţii	
prenumele	ştiinţific		postului	C	S	L	

III. Obiectivele disciplinei
1. Intelegerea notiunilor de algoritm partial si total corect;
2. Formarea deprinderilor de proiectare a algoritmilor in paralel cu demonstrarea corectitudinii lor;
3. Cunoasterea metodelor de testare si verificare a sistemelor soft;
4. Formarea deprinderilor de proiectare a programelor corecte din specificatii;
5. Formarea unui stil modern de programare.

IV. Conţinutul disciplinei
I. Teoria corectitudinii programelor (4 cursuri)
 -  Specificarea programelor.
 - Metoda lui Floyd de demonstrare a corectitudinii.
 - Metoda lui Hoare de demonstrare. 
 - Axiome şi reguli pentru logica Floyd-Hoare: completitudine şi necontradicţie. 
 - Dezvoltarea corecta a programelor din specificaţii
 - Evoluţia istorică a corectitudinii programelor. Contribuţii: Floyd, Hoare, Dijkstra, Gries, Droomey, Morgan
II. Verificarea şi validarea sistemelor  (3 cursuri)
 - conceptele verificare şi validare; asemănări şi deosebiri
 - metode de verificare
 - inspectarea programelor
 - necesitatea documentării programelor
 - execuţie simbolică
III. Testarea programelor. (3 cursuri)
 - conceptul de testare
 - tipuri de testare: a unei proceduri, a unui modul, T.de integrare,  T. de regresie, T. sistemului, T.de acceptare
 - criterii de testare
 - determinarea datelor de test
 - automatizarea testării
IV. Verificarea modelelor (model checking) (2 cursuri)
V. Consecinte asupra metodologiei programarii (2 cursuri)
  - Cleanroom. SPI.
  - Impactul teoriei corectitudinii programelor asupra programarii. Reguli de programare.

V. Bibliografie
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.
B. Internet 	

VI. Tematica activităţilor didactice pe săptămâni

Tematica activitatilor pentru curs 

C1. Verificarea şi validarea sistemelor: concepte, metode, asemănări şi deosebiri
C2. Testarea programelor:  conceptul de testare,  tipuri de testare: a unei proceduri, a unui modul, a întregului sistem. Testarea unui modul (subalgoritm): testarea funcţională şi testarea structurală; Criterii de testare,  determinarea datelor de test;
C3. T.de integrare,  T. de regresie, T. sistemului, T.de acceptare. Automatizarea testării
C4. Inspectarea programelor
C5. Execuţie simbolică
C6. Verificarea modelelor (model checking)
C7.  Evoluţia istorică a corectitudinii programelor. Contribuţiile lui Floyd, Hoare, Dijkstra, Gries, Droomey, Morgan
C8. Metoda lui Floyd de demonstrare a corectitudinii. Metoda axiomatică a lui Hoare de demonstrare a corectitudinii. 
C9. Cleanroom. SPI. 
C10. Cleanroom. Program Quality.
C11. Quality, SPI, SQA,CMM.
C12. Consecinţe asupra metodologiei programării.

Tematica activitatilor pentru seminar
S1: Specificatii si Inspectare
S2: Cazuri de testare: Black-box Testing (BBT) si White-box (WBT) testing
S3: Lucrare de control 1 + BBT and WBT
S4: Model checking+ Corectitudine
S5: Lucrare de control 2 +Corectitudine
S6:Inspection

Tematica activitatilor pentru laborator
L1: Analiza statica . Instrumentrul ESCJava2, JML
L2:Black-box Testing
L3:White-Box Testing
L4:Model cheking
L5:Testare GUI, Web app.
L6:Inspectare

VII. Metode didactice folosite
Conversaţia, expunerea, demonstratia, studii de caz	

VIII. Evaluare
In timpul semestrului activitatea la seminar va fi apreciată prin nota S, iar la laborator prin nota L. La sfarsitul semestrului activitatea se incheie printr-un examen scris, în urma căruia se obţine nota E. Nota finala va fi media aritmetica a notelor mentionate mai sus: F=(S+L+2E)/4.

Details at: www.cs.ubbcluj.ro/~avescan
Section Teaching, at the discipline Verificarea si Validarea Sistemelor Soft 	

IX. Bibliografie suplimentară

	Decan,							Sef de catedra,
Prof. Dr. Leon TAMBULEA 			Prof. Dr. Bazil PARV

	Data,							Titular curs,
		1.10.2009						Lect. dr.  AndreeaVESCAN