CISC/CMPE422, CISC835: Formal Methods in Software Engineering (Fall 2019) Readings (Lecture notes, slides, tool descriptions, examples, papers) [Home] [Content] [Schedule] [Readings] [Assignments]

"Required" marks readings that are required for the course.

General

• Course Overview. J. Dingel. Powerpoint slides of lectures during Week 1, Fall 2019.
• Optional:
  • Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. How Amazon Web Services Uses Formal Methods. Communications of the ACM 58(4):66-73. April 2015.
  • Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, John Fitzgerald. Formal methods: Practice and experience. ACM Computing Surveys 41(4). Oct 2009.
  • Various popular science articles, including:
    • The Coming Software Apocalypse. The Atlantic. Sept 26, 2017.
    • Why Software Fails. R.N. Charette. IEEE Software Spectrum. Sept 2005.

Introduction and logic review

• Required (in courseware): Propositional and Predicate Logic: A Review. J. Dingel. Lecture notes for CISC422. Pages 11 - 57.
• Examples of predicate logic models. J. Dingel. Powerpoint slides of lecture on Oct 2, 2019
• Web tutorial from "Logic in Computer Science", M. Huth and M. Ryan:
  • Chapter 1: Propositional Logic
  • Chapter 2: Predicate Logic
• Jape
  • The Jape web page. B. Sufrin and R. Bornat.
  • Jape for CISC422. J. Dingel.
  • Natural Deduction Proof and Disproof in Jape.

Formal specifications and their analysis

• Required (in courseware): Introduction to the Formal Specification of Software Systems. J. Dingel. Lecture notes for CISC422. Pages 59 - 129.
• Specifications vs implementations and Alloy intro. J. Dingel. Powerpoint slides of lectures on Oct 3 and 4, 2019.
• Alloy
  • Alloy Web site
  • The Alloy book (written by Daniel Jackson, the author of Alloy) is available online through the Books24x7 service which is free for Queen's students. Go here to get started.
• Some sample Alloy specifications used in class or in courseware:
  • family.als
  • lists.als (as used in class)
  • Graphs: without Graph objects and with Graph objects (also in courseware)
  • Stacks: Without ordering, with ordering (to support reasoning about sequences of operations) (also in courseware)
  • River crossing puzzle: Without ordering, with ordering (to support reasoning about sequences of operations) (also in courseware)
  • Portia's Puzzle (for Shakespeare fans)
  • Air Traffic System (also in courseware)
  • Parcel Router
  • Binary Tree
  • Course Requirements
• More sample Alloy specifications can be found here and here
• Slide on 'How to use Alloy' is here (used Oct 30/31)
• Slides on Alloy syntax and semantics are here (used Oct 30/31)
• A sample midterm on Alloy can be found here (the Alloy model for Questions 1 and 2 can be found here, and an Alloy model with which the instance shown in Question 3 can be generated more quickly is here; you can use this model to check your answers).

Finite state machines and their analysis

• Required (in courseware): Introduction to Temporal Logic Model Checking. J. Dingel. Lecture notes for CISC422. Pages 131 - 193.
• Required (on web): NuSMV 2.6 User manual. A. Cimatti and M. Roveri. In html
• Some instructions on using NuSMV at Queen's are here.
• Sample SMV programs used in class:
  • first
  • seasons
  • counters
  • models of mutual exclusion discussed in the notes
  • here's a program that shows the use of arrays sort
  Note that some of the above documents contain several programs. To run these programs, each program has to be put into a separate file.
• Slides on CTL and CTL model checking algorithm are here (used Nov 25, 27, and 28)