SWEN421 (2019) - Formal Software Engineering

Prescription

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:
https://www.victoria.ac.nz/students/study/course-additions-withdrawals

Lecturers

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: 04 March 2019 - 09 June 2019
  • Break: 15 April 2019 - 28 April 2019
  • Study period: 10 June 2019 - 13 June 2019
  • Exam period: 14 June 2019 - 29 June 2019

Class Times and Room Numbers

04 March 2019 - 14 April 2019

  • Tuesday 09:00 - 09:50 – 204, New Kirk, Kelburn
  • Friday 09:00 - 09:50 – 204, New Kirk, Kelburn
29 April 2019 - 09 June 2019

  • Tuesday 09:00 - 09:50 – 204, New Kirk, Kelburn
  • Tuesday 14:10 - 15:00 – 119, Cotton, Kelburn
  • Friday 09:00 - 09:50 – 204, New Kirk, Kelburn

Required

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

Assessment ItemDue Date or Test DateCLO(s)Percentage
Exercise.Week 4CLO: 1,2,3,4,520%
Specification 1Week 8CLO: 1,2,3,4,530%
Specification 2Week 12CLO: 1,2,3,4,550%

Penalties

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

Extensions

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.

Workload

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.victoria.ac.nz/Courses/SWEN421_2019T1/LectureSchedule

Communication of Additional Information

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

Offering CRN: 18661

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