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 engleza
Limba de predare: Engleză

SYLLABUS

I. General data
Code	Subject	
MID0010	Software Systems Verification and Validation	

Semester	Hours: C+S+L	Category	Status	
6	2+1+1	speciality	compulsory	

II. Full status faculty members
Name and	Scientific	Didactic	Chair	Type of activity	
surname	title	title		C	S	L	
FRENTIU Militon	Ph.D.	Prof.	Programming  Languages and Methods	*			

Associated faculty members
Name and	Scientific	Institution	Type of	Type of activity	
surname	title		position	C	S	L	

III. Course objectives
To understand what a correct algorithm is. To gain knowledge of designing correct algorithms and proving their correctness hand- in-hand. To learn the methods of program verification and validation. To become used with building correct programs from specifications. 
To acquire a modern programming style.	

IV. Course contents
I. The theory of program correctness (4 lectures) 
- Program Specification 
- Floyd method for prooving correctness 
- Hoare axiomatisation method 
- Dijkstra: the weakest precondition. 
- Stepwise refinement from specifications 
- The Evolution of the concept of programcorrectness. The Contribution of Floyd, Hoare, Dijkstra, Gries, Droomey, Morgan 

II. Verification and validation: (3 lectures) 
- the concepts verification and validation; 
- the verification methods; 
- program inspection; 
- symbolic execution; 
- testing and debugging; 
- documentation. 
III. Program testing: (3 cursuri) 
- the concept of Program testing; 
- unit testing: testing criteria, blackbox and whitebox testing; 
- types of testing: integration T., system T., regression T., acceptance T. 
- testing automatizing 
IV. Model checking (2 lectures) 
V. Consequences of V&V on programming methodology (2 lectures) 
  - Cleanroom. 
  - Program Quality. SQA
  - The consequences of the theory of program correctness on programming. Programming style. 

V. Bibliography
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 şi Validarea Sistemelor, Ed.Presa Universitară Clujană, 2010
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. Thematic of didactic activities per weeks
Schedule of courses 
Lecture 1. Verification and validation (the concepts verification and validation); 
Lecture 2. Program testing (1): the concept of Program testing; unit testing: testing criteria, blackbox
           and whitebox testing;
Lecture 3. Program testing(2): types of testing( integration T., system T., regression T., acceptance T.),     
           testing automatizing;

Lecture 4. Program inspection
Lecture 5. Symbolic execution
Lecture 6. Model checking
Lecture 7. The theory of program correctness. The evolution of the concept of program correctness.       
           The Contribution of Floyd, Hoare, Dijkstra, Gries, Droomey, Morgan 
Lecture 8. Program Specification. Floyd’s method for prooving correctness. 
           Dijkstra: the weakest precondition. Stepwise refinement from specifications
           Hoare’s axiomatisation method 
Lecture 9. Comparing the verification methods (correctness-inspection-testing-symbolic execution)          
           Verification and validation: How? Who? When?
Lecture 10. Cleanroom. Program Quality.
Lecture 11. Quality, SPI, SQA,CMM.
Lecture 12. The consequences of the theory of program correctness on programming. Programming style. 

Schedule of seminars
S1: Specifications and Inspection
S2: Test cases using Black-box Testing (BBT) and White-box (WBT)testing techniques
S3: Control paper 1 + BBT and WBT
S4: Model checking+ Correctneses
S5: Control paper 2 +Correctness
S6:Inspection

Schedule of labs 
L1: Static analysis using ESCJava2, JML
L2:Black-box Testing
L3:White-Box Testing
L4:Model cheking
L5:Testing GUI, Web app.
L6:Inspection

VII. Didactic methods used
Presentation – for lectures and seminars;
Conversation – for seminars and lectures;
Didactic demonstration – for lectures;
Problematizations – for lectures and laboratory work;
Discovery – for laboratory work;
Other methods – individual study, exercices – for laboratory work.	

VIII. Assessment
The activity at seminaries, consisting from participation in solving the exercises and discussions, will be appreciatewd by a mark S. A second mark L will be given for the laboratories work.  At the end a written examination will give a  mark E. The final mark F is given by:
                                  F=(A+L+2E)/4.
Details at: www.cs.ubbcluj.ro/~mfrentiu/Lectures/	

IX. Additional references

	
           Dean,
           PhD Prof. Leon TAMBULEA	      Chair Chief, 
         PhD. Prof. Bazil PARV

	Date,							Course responsible,
	   1.10.2009	  					  Prof. FRENTIU Militon, Ph.D.