COMPSYS 705 : Formal Methods for Safety Critical Software
Engineering
2025 Semester Two (1255) (15 POINTS)
Course Prescription
Course Overview
This is an interdisciplinary course inspired by software engineering and formal methods. However, this course has been adapted for applicability for computer systems engineering, mechatronics, bio- engineering and medical devices domains. Executable biology refers to executable computational models that mimic biological processes. In this course we will present a range of executable models inspired by formal methods especially for medical device validation. The range of formal methods considered here include a synchronous Statechart called SCChart for pacemaker modelling, a tool called Uppaal for pacemaker verification and a tool called Piha for the design of the cardiac conduction system, which will be validated using the SPIN model checker.
The course is taught in two parts:
Part 1-Fundamentals of model-based design founded on formal methods.
• Automatic verification of closed and open systems using model checking and module checking.
• Modelling and verification of a pacemaker using UPPAAL.
• Run-time verification and enforcement of safety-critical systems.
• Formal modelling and verification using process algebras and bisimulation.
• Introduction to Cyber-Physical Systems (CPS).
Part 2-Industrial successes of formal methods
• Linear Temporal Logic and its industrial applications
• Satisfiability Modulo Theory
• Proof carrying code
• Correctness of software programs
Course Requirements
Capabilities Developed in this Course
| Capability 2: | Sustainability |
| Capability 3: | Knowledge and Practice |
| Capability 4: | Critical Thinking |
| Capability 5: | Solution Seeking |
| Capability 6: | Communication |
Learning Outcomes
- Apply mathematical techniques to embedded system design (Capability 3.1 and 4.1)
- Analyse embedded systems for correctness and safety (Capability 3.2 and 4.2)
- Explain and critically evaluate solutions of safety critical system design (Capability 2.1, 5.1 and 6.1)
- Communicate comprehensively, the design and analysis of embedded systems (Capability 6.1)
- Recognise, analyse and evaluate software program defects and apply techniques to solve them (Capability 3.1, 4.1 and 4.2)
Assessments
| Assessment Type | Percentage | Classification |
|---|---|---|
| Final Exam | 50% | Individual Examination |
| Assignments | 50% | Individual Coursework |
| 2 types | 100% |
| Assessment Type | Learning Outcome Addressed | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| 1 | 2 | 3 | 4 | 5 | ||||||
| Final Exam | ||||||||||
| Assignments | ||||||||||
Teaching & Learning Methods
This is an advanced course that covers research informed content combined with state of the art tools for the verification of safety-critical software. The pedagogy involves many step by step tutorial style exercises and labs to enhance the understanding of this matehmatical content with practical applications.
Workload Expectations
This course is a standard 15 point course and students are expected to spend 10 hours per week involved in each 15 point course that they are enrolled in.
For each week in this course, you can expect 3 hours of lectures, up to 1 hour tutorial and labs, while the remaining time is spent on reading, thinking, developing solutions for the assignments and preparations for the test.
Delivery Mode
Campus Experience
Attendance is expected at scheduled activities including labs/tutorials to complete/receive credit for components of the course. Lectures will be available as recordings. Other learning activities including tutorials/labs will be available as recordings. The course will not include live online events including group discussions/tutorials. Attendance on campus is required for the test. The activities for the course are scheduled as a standard weekly timetable/block delivery.
Learning Resources
Course materials are made available in a learning and collaboration tool called Canvas which also includes reading lists and lecture recordings (where available).
Please remember that the recording of any class on a personal device requires the permission of the instructor.
Health & Safety
Students must ensure they are familiar with their Health and Safety responsibilities, as described in the university's Health and Safety policy
Student Feedback
At the end of every semester students will be invited to give feedback on the course and teaching through a tool called SET or Qualtrics. The lecturers and course co-ordinators will consider all feedback and respond with summaries and actions.
Your feedback helps teachers to improve the course and its delivery for future students.
Class Representatives in each class can take feedback to the department and faculty staff-student consultative committees.
Based on the 2024 feedback, the 50% test has been replaced by a 50% final exam.
Academic Integrity
The University of Auckland will not tolerate cheating, or assisting others to cheat, and views cheating in coursework, tests and examinations as a serious academic offence. The work that a student submits for grading must be the student's own work, reflecting their learning. Where work from other sources is used, it must be properly acknowledged and referenced. A student's assessed work may be reviewed against electronic source material using computerised detection mechanisms. Upon reasonable request, students may be required to provide an electronic version of their work for computerised review.
Class Representatives
Class representatives are students tasked with representing student issues to departments, faculties, and the wider university. If you have a complaint about this course, please contact your class rep who will know how to raise it in the right channels. See your departmental noticeboard for contact details for your class reps.
Inclusive Learning
All students are asked to discuss any impairment related requirements privately, face to face and/or in written form with the course coordinator, lecturer or tutor.
Student Disability Services also provides support for students with a wide range of impairments, both visible and invisible, to succeed and excel at the University. For more information and contact details, please visit the Student Disability Services’ website http://disability.auckland.ac.nz
Special Circumstances
If your ability to complete assessed coursework is affected by illness or other personal circumstances outside of your control, contact a member of teaching staff as soon as possible before the assessment is due.
If your personal circumstances significantly affect your performance, or preparation, for an exam or eligible written test, refer to the University’s aegrotat or compassionate consideration page https://www.auckland.ac.nz/en/students/academic-information/exams-and-final-results/during-exams/aegrotat-and-compassionate-consideration.html.
This should be done as soon as possible and no later than seven days after the affected test or exam date.
Learning Continuity
In the event of an unexpected disruption we undertake to maintain the continuity and standard of teaching and learning in all your courses throughout the year. If there are unexpected disruptions the University has contingency plans to ensure that access to your course continues and your assessment is fair, and not compromised. Some adjustments may need to be made in emergencies. You will be kept fully informed by your course co-ordinator, and if disruption occurs you should refer to the University Website for information about how to proceed.
Student Charter and Responsibilities
The Student Charter assumes and acknowledges that students are active participants in the learning process and that they have responsibilities to the institution and the international community of scholars. The University expects that students will act at all times in a way that demonstrates respect for the rights of other students and staff so that the learning environment is both safe and productive. For further information visit Student Charter https://www.auckland.ac.nz/en/students/forms-policies-and-guidelines/student-policies-and-guidelines/student-charter.html.
Disclaimer
Elements of this outline may be subject to change. The latest information about the course will be available for enrolled students in Canvas.
In this course you may be asked to submit your coursework assessments digitally. The University reserves the right to conduct scheduled tests and examinations for this course online or through the use of computers or other electronic devices. Where tests or examinations are conducted online remote invigilation arrangements may be used. The final decision on the completion mode for a test or examination, and remote invigilation arrangements where applicable, will be advised to students at least 10 days prior to the scheduled date of the assessment, or in the case of an examination when the examination timetable is published.