Introduction: Modern software development inevitably requires the design and analysis of a number of different artifacts. Formal methods allow the mathematically precise formulation of some of these artifacts. This course is an introduction to the use of formal methods for the specification, design, and automatic analysis of software-based systems. Z notational language would be used for system design and verification.

Course Code: SE-4340

Credit Hours: 03

Course pre-requisites: None
 

Learning outcomes: The purpose of this course is to learn how to specify the behavior of systems and to experience the design of a system where you can prove that the behavior is correct. More specifically:

1. Define and state the Z notion of correct system execution.
2. Distinguish between correct and incorrect system behavior.
3. Apply formal logic in expressing (desired) system behavior.
4. Analyze and classify the output of tool for formal system verification..
5. Modify the system structure in order to satisfy the desired behavior.
6. Design and integrate or modify tools for formal system verification.
7. Construct formal models of real systems suitable for verification.

Textbook: The Way of Z: Practical Programming with Formal Methods by Jonathan Jacky, Cambridge University Press (November 28, 1996). ISBN-10: 0521559766

Book Link: https://epdf.pub/the-way-of-z-practical-programming-with-formal-methods.html

Course Contents:

1. Introduction to Formal methods
2. Introducing Z, Elements of Z,
3. Logic and Using Predicates in Z
4. Schemas and Schema Calculus
5. Formal Reasoning
6. Case Studies in Z
7. Safety-Critical Protection System
8. Modeling Large Systems
9. Computer Graphics and Computational Geometry.
10. Rule-Based Programming, Graphical User Interface,
11. Concurrency and Real-time, Refinement, Program Derivation, and Formal Verification
12. Converting Z into Code.

Evaluation:

• Mid Term Exam: 30 Marks
• Final Term Exam: 50 Marks
• Sessional: 20 Marks
  • Quiz: 05 Marks
  • Assignment: 05 Marks
  • Project & Presentation: 10 Marks

Class Timings:

1. BSSE 6th (Regular)
   • Wednesday (12:30pm to 2:00pm)
   • Thursday (12:30pm to 2:00pm)
2. BSSE 6th (Self)
   • Tuesday (2:00pm to 3:30pm)
   • Wednesday (2:00pm to 3:30pm)
3. BSSE 6th (ex-PPP Section A)
   • Wednesday (3:30pm to 5:00pm)
   • Thursday (3:30pm to 5:00pm)
4. BSSE 6th (ex-PPP Section B)
   • Tuesday (5:00pm to 6:30pm)
   • Thursday (2:00pm to 3:30pm)
5. BSSE 6th (ex-PPP Section C)
   • Tuesday (3:30pm to 5:00pm)
   • Wednesday (5:00pm to 6:30pm)

​​​