Queen's Logo

CISC/CMPE422, CISC835: Formal Methods in Software Engineering (Fall 2019)

Detailed course content

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

  1. Introduction, motivation and overview
  2. Background
    1. Languages: Propositional and first-order logic
    2. Analysis techniques: theorem proving
    3. Tools: Jape
  3. Formal specifications and their analysis
    1. Introduction to object modeling
      1. Languages: Class diagrams, first-order logic with relational calculus
      2. Analysis techniques: constraint solving
      3. Tools: Alloy Constraint Checker
  4. Finite state machines and their analysis
    1. Languages: Finite state machines, temporal logic (Computation Tree Logic)
    2. Analysis techniques: state space exploration (i.e., CTL model checking)
    3. Tools: nuSMV