3 lectures per week, 50 minutes each (3-0-3)
Designation: Elective Course
Course Level: Undergraduate
Mathematical foundations for formal methods. Formal languages and techniques for specification and design, including specifying syntax using grammars and finite state machines. Analysis and verification of specifications and designs. Use of assertions and proofs. Automated program and design transformation.
Woodcock, J.C.P. and Davies, J. Using Z: Specification, Refinement, and Proof, Oxford university Press, available online, 1996. [Recommended]
Reference(s) and Other Material:
- Huth, M.R.A. and Ryan, M.D., Logic in Computer Science: Modelling and Reasoning about Systems (2nd Edition), Cambridge University Press, 2004.
Upon completion of this course, students will have the ability to:
- Realize the importance of formal methods in developing safetycritical applications.
- Develop clear, concise, and formal software requirementsspecifications.
- Reason about formal software requirements specifications.
- Apply proof techniques in establishing correctness of formal software requirements specifications.
- Importance of formal methods.
- Logic as a software specification language.
- Sets and types.
- Axiomatic definitions.
- Structural Induction.
- Pre & post conditions, invariants.