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:
- Apply design by Contract to build high integrity code (BE graduate attributes 3(a), 3(c)).
- Review and enhance requirements and be able to trace requirements throughout the design process (BE graduate attributes 3(f), 3(d)).
- Understand relation between testing and verification and manage their relative costs and benefits (BE graduate attributes 3(a), 3(d), 3(f)).
- Write TLA+ specifications, temporl properties and model check
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:
There will be three lectures per week and three assesed assignments will be set during the trimester.
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
Set Texts and Recommended Readings
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 Item||Due Date or Test Date||CLO(s)||Percentage|
|Exercise.||March 29th||CLO: 1,2,3,4,5||20%|
|Specification 1||May 17th||CLO: 1,2,3,4,5||30%|
|Specification 2||June 21st||CLO: 1,2,3,4,5||50%|
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.
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
Communication of Additional Information
All online material for this course can be accessed at https://ecs.wgtn.ac.nz/Courses/SWEN421_2020T1/
Links to General Course Information
- Academic Integrity and Plagiarism: https://www.wgtn.ac.nz/students/study/exams/integrity-plagiarism
- Academic Progress: https://www.wgtn.ac.nz/students/study/progress/academic-progess (including restrictions and non-engagement)
- Dates and deadlines: https://www.wgtn.ac.nz/students/study/dates
- Grades: https://www.wgtn.ac.nz/students/study/progress/grades
- Special passes: Refer to the Assessment Handbook, at https://www.wgtn.ac.nz/documents/policy/staff-policy/assessment-handbook.pdf
- Statutes and policies, e.g. Student Conduct Statute: https://www.wgtn.ac.nz/about/governance/strategy
- Student support: https://www.wgtn.ac.nz/students/support
- Students with disabilities: https://www.wgtn.ac.nz/st_services/disability/
- Student Charter: https://www.wgtn.ac.nz/learning-teaching/learning-partnerships/student-charter
- Terms and Conditions: https://www.wgtn.ac.nz/study/apply-enrol/terms-conditions/student-contract
- Turnitin: http://www.cad.vuw.ac.nz/wiki/index.php/Turnitin
- University structure: https://www.wgtn.ac.nz/about/governance/structure
- VUWSA: http://www.vuwsa.org.nz
Offering CRN: 18661
Prerequisites: SWEN 324 (or 224); 30 300-level pts from (COMP, SWEN)
Duration: 02 March 2020 - 28 June 2020
Starts: Trimester 1