SOFTENG 752 : Formal Specification and Design

Engineering

2023 Semester Two (1235) (15 POINTS)

Course Prescription

Formal specification, design, and (automatic) analysis of software systems. Quality assurance through precise description and rigorous verification on the design. Introduction to the Z, OCL and CSP notations. Comparison of approaches, with emphasis on their practical application. Includes a substantial individual research project.

Course Overview

Secured software development has become a critical aspect in modern software engineering. This course aims at introducing formal modeling and verification techniques to ensure the correctness of software design. It covers the following topics:

- Introduction to Formal Methods : Knowledge of the roles and techniques of formal specification and verification in software Engineering.

- The B formal Specification Language : Set theory and predicate logic - quantifiers, sets, relations, functions, sequences, B language constructs  - States, invariant, operations and machine composition, etc.

- The Object Constraint Language (OCL) of UML : Formal syntax of the OCL language - context, invariant, pre-/post- conditions, types, navigation, etc. The use of the UML Specification Environment (USE) for validating OCL models.

- The Event based Modelling Language : Communicating Sequential Processes (CSP) : Formal semantics and syntax of the Communicating Sequential Processes (CSP) language – events, processes, concurrency and real-time constructs.

Associated modeling tools are used to support the practical applications of the formal verification and simulation. The students will be expected to apply different formal description notations in documenting and analyzing their software designs.

Course Requirements

Prerequisite: COMPSYS 302 or SOFTENG 306

Capabilities Developed in this Course

Capability 1: Disciplinary Knowledge and Practice
Capability 2: Critical Thinking
Capability 3: Solution Seeking
Capability 4: Communication and Engagement
Capability 5: Independence and Integrity
Capability 6: Social and Environmental Responsibilities

Learning Outcomes

By the end of this course, students will be able to:
  1. Describe Apply the mathematically based notations to formally document the design descriptions of software systems. (Capability 1.1, 2.1, 3.1, 3.2 and 4.3)
  2. Verify Using the associated tools to verify and analyse the correctness of the formal design models. (Capability 1.1, 2.1, 3.1, 3.2 and 6.1)
  3. Understand and apply Formal specification and verification techniques to software development in order to enhance the quality of design. (Capability 1.1, 2.1, 3.1, 3.2, 4.1, 4.2, 5.2 and 6.1)

Assessments

Assessment Type Percentage Classification
Assignments 30% Individual Coursework
Test 15% Individual Test
Final Exam 55% Individual Examination
Assessment Type Learning Outcome Addressed
1 2 3
Assignments
Test
Final Exam

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 this course, you can expect 3 hours of lectures, 3 hours of reading and thinking about the content, and 4 hours of work on assignments and test preparation per week.

Delivery Mode

Campus Experience

Attendance is expected at scheduled activities including tutorials to receive credit for components of the course.
Lectures will be available as recordings. Other learning activities including tutorials/labs will not be available as recordings.
The activities for the course are scheduled as a standard weekly timetable.

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 are expected to adhere to the guidelines outlined in the Health and Safety section of the Engineering Undergraduate Handbook.

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.

Feedback from current year teaching will be reflected in the course content of next year. For example, content on B-methods will be extended to remove the old content on Z notation, to which B is a new modeling language popularly used by the industry.

Academic Integrity

The University of Auckland will not tolerate cheating, or assisting others to cheat, and views cheating in coursework 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. This requirement also applies to sources on the internet. A student's assessed work may be reviewed against online source material using computerised detection mechanisms.

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 course assessment continues to meet the principles of the University’s assessment policy. Some adjustments may need to be made in emergencies. You will be kept fully informed by your course co-ordinator/director, 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 students may be asked to submit 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. In exceptional circumstances changes to elements of this course may be necessary at short notice. Students enrolled in this course will be informed of any such changes and the reasons for them, as soon as possible, through Canvas.

Published on 10/11/2022 09:59 a.m.