CA.SFU.FAS.UCC/Papers:2005-68

New Course Proposal:
CMPT 477
(Cross-Listed with CMPT 777)
Introduction to Formal Verification

Eugenia Ternovska

• Calendar Information

  Course Number: CMPT 477 (cross-listed with 777)
  Credit Hours: 3 Vector: 3-0-0
  Course Description:

  The goal of formal verification is to prove correctness or to find mistakes in software and other systems. This course introduces, at an accessible level, a formal framework for symbolic model checking, one of the most important verification methods. The techniques are illustrated with examples of verification of reactive systems and communication protocols. Students learn to work with a model checking tool such as NuSMV.

  Prerequisite: CMPT 275
  Recommended: None
  Corequisite: None
  Special Instructions: None
  

  Course(s) dropped if if this course is approved: None

  
  

• Rationale for Introduction of this Course

  • Reliability and safety of software in critical applications is a major concern in security, medical applications, telecommunication industry etc. Formal verification is among the most promising techniques for addressing this concern. Formal verification is everyday practice in hardware design, and major software companies are actively pursuing this direction.

  • Similar courses (with the same textbook) is taught in dozens if not hundreds of universities around the world including Princeton, CMU, Cambridge, McGill and Toronto.

  • The course is useful for all students -- it introduces a rigorous approach to software engineering.

  • It is a natural addition to our software engineering program -- it's about building correct and reliable systems.

  • The course provides a connection with research interests of several faculty members in the department. Through this course, a few very good students were attracted to our graduate program.

  • Students really like this course. They learn a formal, mathematically transparent theory, and immediately see how it works in practice by designing and verifying their own systems.

  Will this be a required or elective course in the curriculum?

  Elective for now. I intend to propose it as a required course for the software engineering stream in the future. It would increase the proportion of courses with formal content in this stream, which is currently quite low.

  Probable enrollment when offered? Around 30

• Scheduling for Introduction of this Course

  Indicate Semester and Year this course would be first offered and planned frequency of offerings thereafter.

  Spring 2006 and annually thereafter

  Which of your present CFL faculty have the expertise to offer this course? Will the course be taught by sessional or limited term faculty?

  E. Ternovska

  Are there any proposed student fees associated with this course other than tuition fees?

  No

  Is this course considered a `duplicate' of any current or prior course under the University's duplicate course policy? Specify, as appropriate.

  No

• Resource Implications

  Senate has approved (S.93-11) that no new course should be approved by Senate until funding has been committed for necessary library materials. Each new course proposal must be accompanied by a library report and, if appropriate, confirmation that funding arrangements have been addresssed. Does the course require specialized space or equipment not readily available in the department or university, and if so, how will these resources be provided?

  The library already has both the required and the recommended books. Computing resources: CSIL (Computer Science Instructional Lab)

• Course Outline

  OBJECTIVE and DESCRIPTION:

  Please note that this course is cross listed with CMPT 777

  Real software systems are extremely complex. In the software industry, formal verification methods are increasingly used to verify that a model of a software system satisfies the requirements. The course concentrates on contemporary applications of logic to the verification of software systems. The objective is to introduce, at an accessible level, a mathematical framework for symbolic model checking, one of the most important verification methods. The techniques are illustrated with examples of verification of reactive systems and communication protocols. Students learn to work with the model checking tool SMV.

  TOPICS:

  • model checking as a verification technique
  • model checking with Computational Tree Logic (CTL)
  • representing practically relevant specifications in CTL
  • the NuSMV (``symbolic model verifier'') system
  • alternatives and extensions of CTL
  • model checking with fairness
  • efficient representation of boolean functions - binary decision diagrams
  • use of binary decision diagrams in symbolic model checking
  • model checking for the relational mu-calculus

  GRADING:

  • Four assignments (paper-pencil and programming): 40%
  • Midterm: 20 %
  • Final Exam: 40 %

  TEXTBOOKS: Logic in Computer Science: Modelling and Reasoning about Systems, Michael R. A. Huth and Mark D. Ryan, Cambridge University Press, 2nd edition.

  REFERENCES: Model Checking, E. M. Clarke, O. Grumberg and D. Peled, MIT Press, 2000