SWEN324 (2019) - Software Correctness

Prescription

This course is concerned with the development of correct software, especially the use of formal requirements and specifications to develop high-integrity software. This has applications in several areas, such as safety-critical systems (e.g. commercial airliners, space systems, etc) and high-performance concurrent systems. The course will examine a range of principles and techniques which underpin a rigorous approach to the specification and implementation of software. A sequence of assignments and labs will see a range of tools being used to specify small software systems, and to check that they meet their requirements. NB: this course is first running in 2019.

Course learning objectives

Students who pass this course will be able to:

  1. Use mathematical structures such as sets, functions, relations and sequences to model software systems, and to state desired properties of such systems, including pre and postconditions, class invariants and loop invariants.
  2. Use mathematical reasoning to prove properties of the various formalisms studied in the course, including correctness properties of programs.
  3. Use tools such as Whiley and OpenJML to check correctness properties of software systems.
  4. Use formalisms such as regular expressions and context free grammars to describe the syntactic structure of artificial languages.
  5. Use state machine models such as finite acceptors and push down acceptors to construct recognisers for artificial languages.

Withdrawal from Course

Withdrawal dates and process:
https://www.victoria.ac.nz/students/study/course-additions-withdrawals

Lecturers

Teaching Format

Student feedback

This is a new course

Dates (trimester, teaching & break dates)

  • Teaching: 08 July 2019 - 13 October 2019
  • Break: 19 August 2019 - 01 September 2019
  • Study period: 14 October 2019 - 17 October 2019
  • Exam period: 18 October 2019 - 09 November 2019

Class Times and Room Numbers

08 July 2019 - 18 August 2019

  • Monday 14:10 - 15:00 – LT101, Maclaurin, Kelburn
  • Wednesday 14:10 - 15:00 – LT101, Maclaurin, Kelburn
02 September 2019 - 13 October 2019

  • Monday 14:10 - 15:00 – LT101, Maclaurin, Kelburn
  • Wednesday 14:10 - 15:00 – LT101, Maclaurin, Kelburn

Other Classes

There is a weekly tutorial Thursday 2-3pm in Murphy 101

Required

There is no set text in this course.

There are many books available, some online. There are many lecture notes, tutorials, etc online. See the course web site for recommendations.

Mandatory Course Requirements

In addition to achieving an overall pass mark of at least 50%, students must:

  • Achieve at least 40% average across the 6 assignments
  • Achieve at least a D on the exam

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
Assignment 1CLO: 12.5%
Assignment 2CLO: 12.5%
Assignment 3CLO: 12.5%
Assignment 4CLO: 12.5%
Assignment 5CLO: 12.5%
Assignment 6CLO: 12.5%
Exam (2 hours)CLO: 50%

Penalties

10% reduction per weekday after the deadline, or 2 weeks after the assignment is handed out (whichever is later)

Extensions

If you have significant medical or personal issues that may affect your ability to submit an assignment on time, contact the course organiser to discuss an extension. You may need documentation for significant cases.

Submission & Return

All assignments must be submitted via the ECS submission system. Marks and comments will be returned via the ECS marking system.

Group Work

There is no group work in this course

Workload

The expected workload for the course is about 10 hours per week. This includes the lectures, tutorial, assignment and reading/study time

Teaching Plan

The lecture topics and lecture slides will be available on the course web site (https://ecs.victoria.ac.nz/Courses/SWEN324_2019T2/LectureSchedule)
 
The expected topics to be covered include
Formal specification
Program verification
Data refinement
System specification and verification
Processes and interaction

Communication of Additional Information

All information about the course will be available at https://ecs.victoria.ac.nz/Courses/SWEN324_2019T2

Offering CRN: 30044

Points: 15
Prerequisites: COMP 103; ENGR 123 or MATH 161; 30 200-level COMP/NWEN/SWEN points;
Restrictions: SWEN 224
Duration: 08 July 2019 - 10 November 2019
Starts: Trimester 2
Campus: Kelburn