SWEN421 (2020) - Formal Software Engineering


This course addresses the use of mathematical logic in the specification and construction for software systems. It presents an introduction to the area of formal methods; the formal specification of software systems; the refinement of specifications to code; and their semantic foundations.

Course learning objectives

Students who pass this course should be able to:

  1. Apply design by Contract to build high integrity code (BE graduate attributes 3(a), 3(c)).
  2. Review and enhance requirements and be able to trace requirements throughout the design process (BE graduate attributes 3(f), 3(d)).
  3. Understand relation between testing and verification and manage their relative costs and benefits (BE graduate attributes 3(a), 3(d), 3(f)).
  4. Write TLA+ specifications, temporl properties and model check

Course content

You will learn the languages TLA+ and PlusCal that are used by Amazon to design the communication protocols that underpin their secure cloud computing.
 This will require an understanding of first order logic. The course will try to follow a hands on approach to learning where every it is possible. Nonetheless  a high degree of abstract thinking will be needed.

Required Academic Background

You must be a competent programmer and confident in your ability to pick up a new language. You need the ability to think rigorously about abstract ideas including specifications . You must be able to express your understanding of the programs requirements in First Order Logic and you need a good grasp of the the relation between specification and code.

Withdrawal from Course

Withdrawal dates and process:


David Streader (Coordinator)

Teaching Format

There will be three lectures per week and three assesed assignments will be set during the trimester.

Student feedback

Student feedback on University courses may be found at:  www.cad.vuw.ac.nz/feedback/feedback_display.php

Dates (trimester, teaching & break dates)

  • Teaching: 02 March 2020 - 07 June 2020
  • Break: 13 April 2020 - 27 April 2020
  • Study period: 08 June 2020 - 11 June 2020
  • Exam period: 12 June 2020 - 27 June 2020

Class Times and Room Numbers

02 March 2020 - 22 March 2020

  • Monday 10:00 - 10:50 – 118, Cotton, Kelburn
  • Tuesday 10:00 - 10:50 – 118, Cotton, Kelburn
  • Thursday 10:00 - 10:50 – 118, Cotton, Kelburn
27 April 2020 - 31 May 2020

  • Tuesday 10:00 - 10:50 – , , Kelburn
27 April 2020 - 28 June 2020

  • Monday 10:00 - 10:50 – , , Kelburn
  • Thursday 10:00 - 10:50 – , , Kelburn
01 June 2020 - 28 June 2020

  • Tuesday 10:00 - 10:50 – 104, Alan MacDiarmid Building, Kelburn


There is no assigned textbook for SWEN 421 but there are two books that have been made freely available, by the authors, in pdf form. Links to web pages and papers that should be read can be found on the lecture schedule.

Mandatory Course Requirements

There are no mandatory course requirements for this course.

If you believe that exceptional circumstances may prevent you from meeting the mandatory course requirements, contact the Course Coordinator for advice as soon as possible.


Assessment ItemDue Date or Test DateCLO(s)Percentage
Exercise.March 29thCLO: 1,2,3,4,520%
Specification 1May 17thCLO: 1,2,3,4,530%
Specification 2June 21stCLO: 1,2,3,4,550%


Work submitted late incurs a 5% penalty per day. Special considerations at the course coordinators discretion, or sickness backed up by a doctors note.


Students must hand in the assigned work on or before the time indicated on the lecture schedule. Late work will only be accepted for medical reasons with a note from your doctor.

Submission & Return

All work is submitted through the ECS submission system, accessible through the course web pages. Marks and comments will be returned through the ECS marking system, also available through the course web pages.

Group Work

We encourage you to talk with each other about the course and the assignments, and to help each other when you are stuck. But work that you submit for your assignments should represent your own work.


In order to maintain satisfactory progress in SWEN 421, you should plan to spend an average of 10 hours per week on this paper. A plausible and approximate breakdown for these hours would be:

  • Lectures and tutorials: 3 hours
  • Readings: 2 hours
  • Assignments: 5 hours

Teaching Plan

See: https://ecs.wgtn.ac.nz/Courses/SWEN421_2020T1/LectureSchedule

Communication of Additional Information

All online material for this course can be accessed at https://ecs.wgtn.ac.nz/Courses/SWEN421_2020T1/

Offering CRN: 18661

Points: 15
Prerequisites: SWEN 324 (or 224); 30 300-level pts from (COMP, SWEN)
Duration: 02 March 2020 - 28 June 2020
Starts: Trimester 1
Campus: Kelburn