Queen's Logo

CISC422: Formal Methods in Software Engineering (Winter 2012)

Detailed course content

[Home] [Content] [Schedule] [Readings] [Assignments] [Tools]

  1. Introduction, motivation and overview
  2. Background
    1. Propositional logic
    2. First-order predicate logic
    3. Introduction to theorem proving
    4. Tools: Jape
  3. Formal specifications and their analysis
    1. Introduction to Z
    2. Introduction to object modeling
      1. Automatic analysis of object models using Alloy
      2. Tools: Alloy Constraint Checker
    3. Introduction to UML and OCL (possibly not covered this year)
      1. Validating UML models and OCL constraints
      2. Tools: USE
  4. Finite state machines and their analysis
    1. Modeling systems using finite state machines
    2. Temporal logics CTL
    3. Explicit CTL model checking
    4. Binary decision diagrams (time permitting)
    5. Symbolic CTL model checking (time permitting)
    6. Tools: nuSMV
Last modified: Sat Jan 7 22:37:55 EST 2012