
Description:  Formal mechanisms for specifying, building, and verifying software; Formal specification using various techniques, and initial specification and refinement towards implementation; Integration of formal methods with existing programming languages; The application of formal methods to requirements analysis, testing and safety analysis; Objectoriented approaches. (Prerequisite: SWEB300) 
Credit Hours.:  3 
Text Book:  David Lightfoot, Formal Specification Using Z 
Coordinator:  Boumediene Belkhouche 
Topics Outline:   Introduction to Formal Methods
 Review: Mathematical Background
 Formal Specifications
 Specification Language
 Specifying Systems
 The Object Constraint Language (OCL)
 Application of OCL
 Algebraic Specifications of Concurrent Processes
 Proofs of correctness

Outcomes:   Explain the role of formal methods in software development
 Differentiate the formal verification techniques
 Write basic OCL constraints
 Produce Software specifications using Z.
 Identify the challenges of deriving formal specifications from requirements.

Mapping of Topics Outline to Outcomes   1 
2 
3 
4 
5 
6 
7 
8 
9 
1 
        
2 
        
3 
        
4 
        
5 
        

Prerequisite  SWEB300: Software Engineering Fundamentals
