National University of Sciences and Technology
Home | Back
SE-867 Formal Methods
Campus MCS
Programs PG
Session Summer Semester 2016
Course Title Formal Methods
Course Code SE-867
Credit Hours 3+0
Pre-Requisutes MATH-161 Discrete Mathematics (Desirable not must)
Course Objectives Formal methods are increasingly used as powerful specification, verification and early debugging methods in the development of industrial SW and HW systems. This course provides an introduction to Formal Techniques and Tools for the specification and verification of Hardware and Software platforms. Apart from an introduction on formal techniques and their benefits, the course will also focus on formal verification and validation.
Detail Content

Course Out Line

                                                                              

1

Introduction to Formal Methods

2

Hoare Logic and Program Verification

3

Motivation for program verification

4

Partial and total correctness

5

Program variables and logical variables

6

ESC/Java

7

Proof calculus: A proof calculus for partial correctness, A proof calculus for total correctness, A proof calculus for concurrent programs.

8

Loop invariants

9

Weakest preconditions and verification condition generation

10

Own research: Monitoring and Proof-carrying code

11

Process Algebra and Equivalence Checking

12

Communicating systems: Semantics of communication behavior, Calculus of Communicating Systems (CCS),

13

Observable behavior

14

Observation equivalence: weak bisimulation

15

Concurrency Workbench (CWB)

16

Linear-time Temporal Logic (LTL)

17

Protocol Meta Language (Promela)

18

Automata over infinite words

19

Automata based verification

20

Computation Tree Logic (CTL)

Text/Ref Books

TextBook:

  1. Understanding Formal Methods by by Jean-Francois Monin, M.G. Hinchey.

Reference:

  1. "Z: An Introduction to Formal Methods" by Antoni Diller.
Time Schedule Summer Semester 2015
Faculty/Resource Person A/P Dr Sarmad Sadik
MCS-NUST, Islamabad, Pakistan
Discipline: Information Technology
Specialization: Computer Science