SWE 321: Formal Methods And Models In Software Engineering

​

SWE 321: Formal Methods And Models In Software Engineering

 
Course Information
Class/Laboratory Schedule: 

3 lectures per week, 50 minutes each (3-0-3)

Designation: 
 Elective Course
Course Level: 
 Undergraduate
Prerequisites
Prerequisite Courses: 
ICS 202: Data Structures
ICS 253: Discrete Structures I
Catalog Description: 

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.

Textbook(s): 

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.
Course Outcomes: 

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.
Topics Covered: 
  • Importance of formal methods.
  • Logic as a software specification language.
  • Sets and types.
  • Axiomatic definitions.
  • Structural Induction.
  • Pre & post conditions, invariants.​