Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Masterat
Domeniul: Informatica
Programul de studii: Programare bazată pe componente - în limba engleză
Limba de predare: Engleză

SYLLABUS

I. General data
Code	Subject	
MID1002	Formal Methods in Programming	

Semester	Hours: C+S+L	Category	Status	
1	2+2+0	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.		*	*		

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

III. Course objectives
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 familiarize students with the language Z and its use  for formal specification, verification of software systems. To obtain the ability to evaluate the coverage of testing, and to prove the correctness of programs.

IV. Course contents
1.	The object of Formal Methods
2. Derivation of correct  programs from specifications  
3. Formal Specification
4  Z language: specification and refinement
5. Industrial use of Formal Methods
6. Formal Verification 
7. Formal Methods and program testing
8. Formal Methods in Object-Oriented Development 
9. Model checking	

V. Bibliography
1. Dan Craigen, Susan Gerhart, Ted Ralston, An International Survey of Industrial Applications of Formal Methods, U.S. Department of Commerce, NISTGCR 93/626.
2. Ehrig H., B.Mahr, Fundamentals of Algebraic Specification, Springer-Verlag, 1985
3. M.Frenţiu, Formal Methods in Software Engineering Education, Proceedings ICELM1, Tg.Mureş, 3-5 iunie 2004, şi www.cs.ubbcluj.ro/~mfrentiu.
4. M. Frenţiu, Verificarea corectitudinii programelor, Petru Maior University Press, 2000.
5. A.Gawanmeh, S.Tahar, K.Winter, Formal Verification of ASM Designs using the MDG Tool, Procc. Of the First International Conference on Software Engineering and Formal Methods (SEFM’03), 2003.
6. Jonathan Jacky, The Way of Z: Practical Programming and Formal Methods, Cambridge University Press, 1997.
7. Morgan C., Programming from Specifications, Prentice Hall, 1990.
8. J.W.Nimmer, Automatic Generation and Checking of Program Specification, Technical Report #MIT-LCS-TR-852, 2002.
9. J.Rushby, Formal Methods and the Certification of Critical Systems, USA, SRI Intern., Technical Report CSL-93-7, 315 pages.
10. Sherrell L.B. and D.L.Carver, FunZ: An intermediate specification language, Computer Journal, 38(1995), 3, 193-207.
11. J.M.Spivey, The Z Notation, Prentice Hall, London, 1998. 
12. Jim Woodcock and Jim Davies, Using Z: Specification, Refinement, and Proof, Prentice Hall, 1996.

VI. Thematic of didactic activities per weeks
C1 (+S1). The object of Formal Methods ([3])
• Software crisis
• What are the Formal Methods?
• Are FM needed?
• Levels of using Formal Methods
C2 (+S2). Formal Specification ([7], chapter 1)
• The Concept of Formal Specification
• Methods of Specification
• Formal Specification Languages
C3 (+S3). Derivation of correct  program from specifications  ([7], chapters 2-4)
• The software life-cycle 
• Pre- and post-conditions 
• The Specifications as contracts 
• Refinement
• Refinement rules
• Examples of refinements
C4 (+S4). Introduction to Z language ([12], chapter  1-10)
• Mathematical notations: sets, predicates, relations, functions, sequences 
• Z schemas: conventions, expressions
• Examples• Schema operators
C5 (+S5). Schema operators ([12], chapter 11,12 )
• operators: conjunction, decoration, disjunction, negation, quantification
• composition
• Examples
C6 (+S6). Promotion ([12], chapter 13)
• Local and global operations
• The concept of  promotion
• Examples of specification by promotion
C7 (+ S7). Data Refinement ([12], chapters 16 and 17)
• Data types and data refinement
• Schema Refinement
• Examples
C8 (+S8). Functional refinement ([12], chapter 18 )
• Retrieve functions
• Functional refinement
• Calculating data refinement
• Refining promotion
C9 (+S9). Refinement calculus ([12], chapter 19)
  • Specification statement
     • Refinement rules for sequential compositon, conditional and iteration statements
     • Examples
C10 (+S10). Industrial use of Formal Methods ([1])
   • Examples of real projects where  FM were used
   • Findings and recommendations
   • Used Formal Methods
C11 (+S11). Formal Verification  ([4, section 5.4], [8, chapter 3], [O7, pp.280-420])
    • proving correctness 
    • is automated proof possible?
    • formal inspections
C12 (+S12). Formal Methods and program testing ([O7, pp.235-264])
    • formal description of software architecture;
    • conformance testing;
    • generating test cases;
    • automated synthesis of test cases.
C12 (+S13). Formal Methods in Object-Oriented Development  ([O1])
   • Formalality Methods in Object Technology ([chapter 2])
   • Integrating Formal Methods in O.O.Systems ([chapter 7])
C14 (+S14). Model checking ([O6, O8])
   • Abstract State Machines
   • Kripke Transition  Systems
   • temporal logic
   • Model checking method
   • The state explosion problem
   • Symbolic Model Verifier (SMV)
   • Model checking in practice

VII. Didactic methods used
   Expositions: class lectures, introductive lectures, dialog-based lectures, lectures with demonstrations, descriptions and explanations.
   Conversations: dialog, debate, introductive conversations,   conversations to systematize and synthesize knowledge.
   Discovery: inductive and deductive discovery, directed and independent rediscovery, creative discovery, experimental discovery.
   Use of problems: use of problem questions, problems and problem situations.
   Other methods: exercises,  individual and homework study, case study, brainstorming.

VIII. Assessment
A first grade will be given for a final written examination covering both theory and practice, and a second grade will be given for the activity during the term. The final result will be the average of these two grades.	

IX. Additional references
O1. J.-R. Abrial, The B-Book: Assigning Programs to Meanings, Cambridge University Press, 1996.
O2. O8. M.Chechik, Wei Ding, On Interpreting Results of Model-Checking with Abstraction, CSRG Technical Report, Dept. Of CS, Univ.of Toronto, 2000.
O3. Goldsack S.J., and S.J.H.Kent, Formal Methods and Object Technology, Springer.
O4. KIM S.D., Formal Specification in OO Software Development, PhD Thesis, 1991, Iowa University
O5.  Lano K., Formal Object-Oriented Development, Springer
O6. A.-J.Kaijanaho, The formal method known as B and a sketch for its implementation, Master’s thesis in Information Technology, University of Jyvaskyla, 2002.
O7. K.-K.Lau, R.Banach, Formal Methods and Software Engineering: 4th International Conference on Formal Engineering, ICFEM 2005, LNCS 3785.
O8. Vadera S. and F.Meziane, From English to Formal Specifications, Computer Journal, 37(1994), 9, 753-763.
O9. **** Formal Methods Specification and Verification GuideBook for Software and Computer Systems, NASA/TP-98-208193.
O10.  Other Papers on Formal Methods from the Journals: 
a.	IEEE Software. 
b.	IEEE Transactions on Software Engineering. 
c.	Transactions on Software Engineering and Methodology (TOSEM), ACM.
d.	Software -- Practice and Experience, Wiley. 
e.	Internet

	Dean 							Head of chair,

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