Queen's School of Computing

CISC 422/3.0 Formal Methods in Software Engineering

Original Author: Juergen Dingel
Last Revised: October 17, 2006

Calendar Description

Mathematical methods for describing software behaviour and structure. Topics include (but are not limited to) the following: Requirements specification. Module specification: axiomatic, algebraic, and trace specifications. Abstract models. Verification. Specification-based validation.

Prerequisite: CISC 327/3.0.

Objectives

Software development inevitably requires the design and analysis of a number of different artifacts. Formal methods allow mathematically precise yet concise formulation of some of these artifacts. For instance, formulas in predicate logic capture operational requirements, state machines describe the behaviour of code fragments and protocols, and object models capture static designs. The advantage of using these formal notations is that they typically improve the overall quality of the artifacts by removing ambiguities and imprecisions, and enabling automatic analyses that establish desirable properties or uncover undesirable properties. Consequently, the use of formal methods is indicated in domains in which the software has to meet very high quality standards and failure cannot be tolerated such as air-traffic control. Moreover, the abstraction and automation capabilities of some formal techniques present a powerful weapon against the ever-increasing complexity of software. Indeed, in Model-Driven Development (MDD), a development methodology advocated by, for instance, the Object Modelling Group and IBM, formal models of the software and its requirements form the primary artifacts from which the code is automatically generated.

This course is an introduction to the use of formal methods for the specification, design, and automatic analysis of software systems. The course will present a variety of specification notations (propositional and predicate logic, Z, Alloy, UML/OCL, temporal logic), and discuss corresponding analysis techniques (theorem proving, constraint checking, animation, model checking) using existing commercial and research tools (Jape, Z/Eves, Alloy, USE, SMV). The course is most suited for students with a general background in computer science or electrical engineering and an interest in the theory and practise of software development.

Topics

Introduction, Objectives and Overview

Background

  • Propositional logic
  • First-order predicate logic
  • Introduction to theorem proving
  • Typical tool: Jape

Formal specifications and their analysis

  • Introduction to a formal specification framework, such as Z, VDM, or B
  • Introduction to object modeling
    • Automatic analysis of object models
    • Typical tool: Alloy Constraint Checker
  • Introduction to UML and OCL
    • Validating UML models and OCL constraints
    • Typical tool: USE

Finite state machines and their analysis

  • Modeling systems using finite state machines
  • Temporal logics, CTL
  • Explicit CTL model checking
  • Binary decision diagrams (time permitting)
  • Symbolic CTL model checking (time permitting)
  • Typical tool: nuSMV

Possible Textbooks

  • Logic in Computer Science: modelling and reasoning about systems. Michael Huth and Mark Ryan; 427 pages (2nd edition). Cambridge University Press. June 2004.
  • Software Reliability Methods. Doron Peled. Springer-Verlag. 2001.
  • Software Abstractions: Logic, Language, and Analysis. Daniel Jackson. MIT Press. 350 pages. April 2006.
  • Model Checking. Edmund M. Clarke, Orna Grumberg and Doron A. Peled. MIT Press. 330 pages. January 2000.