syllabus
1. Information regarding the programme
1.1 Higher education institution 	Babes-Bolyai University	
1.2 Faculty	Mathematics and Computer Science	
1.3 Department	Computer Science	
1.4 Field of study	Computer Science	
1.5 Study cycle	Master	
1.6 Study programme / Qualification 	Component Based Programming	

2. Information regarding the discipline 
2.1 Name of the discipline		
2.2 Course coordinator 	Militon FRENTIU 	
2.3 Seminar coordinator	Militon FRENTIU	
2.4. Year of study	1	2.5 Semester	1	2.6. Type of evaluation	ex	2.7 Type of discipline	Compulsory	

3. Total estimated time (hours/semester of didactic activities) 
3.1 Hours per week 	3	Of which: 3.2 course	2	3.3 seminar/laboratory	1	
3.4 Total hours in the curriculum 	42	Of which: 3.5 course	28	3.6 seminar/laboratory	14	
Time allotment:	hours	
Learning using manual, course support, bibliography, course notes	28	
Additional documentation (in libraries, on electronic platforms, field documentation) 	14	
Preparation for seminars/labs, homework, papers, portfolios and essays	14	
Tutorship	10	
Evaluations	 4	
Other activities: ..................	 2	
3.7 Total individual study hours 	66	
3.8 Total hours per semester	108	
3.9 Number of ECTS credits		

4. Prerequisites (if necessary)
4.1. curriculum	•	Formal Methods in Programming	
4.2. competencies	•	Advanced knowledge of Formal Development of Programs	

5. Conditions (if necessary)
5.1. for the course	•	course attendance	
5.2.  for the seminar /lab activities	•	Individual work	

6. Specific competencies acquired 
Professional competencies	To introduce the students to the formal techniques needed in the development of systems. To have an understanding of both the theory and practice of formal mathematical thinking in software specification, verification and development. To be able to perform formal analysis and to reason about designs and developments. To obtain the ability to analyse  the correctness of algorithms, and to measure the qualities of programs.	
Transversal competencies	
● Formal program development
● Formal Verification	

7. Objectives of the discipline (outcome of the acquired competencies)
7.1 General objective of the discipline
	•	To introduce the students to the formal techniques needed in the development of systems. To have an understanding of both the theory and practice of formal mathematical thinking in software specification, verification and development. 	
7.2 Specific objective of the discipline
	•	To be able to perform formal analysis and to reason about designs and developments. To obtain the ability to analyse  the correctness of algorithms, and to measure the qualities of programs.	

8. Content
8.1 Course	Teaching methods	Remarks	
1.	What are Formal Methods? Myths. Applications.	Exposure, conversation		
2.	Formal Specification	Exposure, conversation		
3.	Derivation of correct  program from specifications  	Exposure, conversation		
4.	Introduction to Z language	Exposure, conversation		
5.	Schema operators	Exposure, conversation		
6.	Promotion	Exposure, conversation, examples		
7.	Data Refinement	Exposure, conversation		
8.	Functional refinement	Exposure, conversation, examples		
9.	Refinement calculus	Exposure, conversation, examples		
10.	Formal Verification  	Exposure, conversation		
11.	Formal Methods and program testing	Exposure, conversation		
12.	Industrial use of Formal Methods	Exposure, conversation		
13.	Model Checking: Kripke Trenasition Systems;
Temporal Logic: LTL and CTl	Exposure, conversation		
14.	Model Checking in practice	Exposure, conversation		
Bibliography
MORGAN C., Programming from Specifications, Prentice Hall, 1990.
WOODCOCK,J., J. DAVIES, Uzing Z. Specification, Refinement and Proof, Prentice-Hall, 1996
Spivey, J., The Z Notation: A Reference Manual, Prentice Hall International Series in Computer Science, 1992.
Internet articles
	
8.2 Seminar / laboratory	Teaching methods	Remarks	
1.	Levels of Formal Methods	Conversation, debate		
2.	Formal derivation of programs	Conversation,examples		
3.	Formal specification	Conversation,debate		
4.	Z schemas	Conversation,examples		
5.	Project one presentation	Conversation, debate		
6.	Project two presentation	Conversation, debate		
7.	Consequences in practice	Conversation, debate		
Bibliography
    Internet papers

	

9. Corroborating the content of the discipline with the expectations of the epistemic community, professional associations and representative employers within the field of the program

•	 The course respects the ACM Curriculla for CS studies;
•	The course exists in the studying master program of the major universities

10. Evaluation
Type of activity	10.1 Evaluation criteria	10.2 Evaluation methods	10.3 Share in the grade (%)	
10.4 Course	a final written examination covering both theory and practice	Marks for answers at a
Written exam	50%	
				
10.5 Seminar/lab activities	the activity during the term reflected in two projects	Two marks for projects	50%	
				
10.6 Minimum performance standards	
•	At least grade 5, in a scale of 1 to 10	

Date				Signature of course coordinator 	Signature of seminar coordinator
17 september .2012		Prof. PhD Militon Frentiu		. Prof. PhD Militon Frentiu	

Date of approval  					  Signature of the head of department	
...........................................					...........…............................