ITECH7410 – Software Engineering Methodologies Assignment


The purpose of this assessment is to provide students with the opportunity to apply knowledge and skills developed  during the semester with particular reference to the formal specification of a system through the use of Z notation.  Students complete the assignment in groups of two.  

As described in this course’s third study guide, Software Analysis, Modelling and Specification, a Formal  Specification (Technique) is one that has a rigorous mathematical basis and one of its advantages is that it can be  mathematically checked for completeness. The course’s fourth study guide, System and Software Design, also  states that by using formal methods it is possible to derive a formal design from a formal specification and then be  able to prove that the design and specification are functionally equivalent.  

Your text, Software Engineering: A Practitioners Approach (Pressman, 2010) indicates that formal methods provide  frameworks that allow people to specify, develop and verify systems in a structured and systematic way and that the  mathematical based specification language used in formal methods ensures a greater chance of consistency,  completeness and lack of ambiguity in a specification. Pressman also discusses formal specification languages and  their common components – syntax, semantics and sets of relations. Of the four formal specification languages he identifies – OCL, LARCH, VDM and Z – he provides useful discussion with respect to OCL and Z.  

In this assignment, you will use the Z specification language to provide the sets, relations and functions in schemas  to specify a subsystem relating to the theme of the smart campus. Your group can choose the subsystem based on  previous work each member has already completed. Your schemas should provide the stored data that the system  accesses and alters and identify the operations that are applied to change the state as well as the relationships that  occur within the system. Remember, as specified in Spivey’s 2001 text, The Z Notation: A Reference Manual,  schemas are utilized to illustrate both static and dynamic aspects of a system. Static aspects include such things as  the states a system occupies and the invariant relationships that continue to exist as the system moves between  states. Dynamic aspects include the changes of state that occur, possible operations and the relationships between  their inputs and outputs. Remember also you should always be conscious of the fact that a specification tries to  describe what the system must do without saying how it is to be done (Spivey, 2001).  

Keep all the above in mind as you read the following information. You are required to create a set of Z schema that  adequately describes the requirements of your chosen subsystem. Your assignment should include at least one 

Timelines and Expectations 

Marks: Assignment will be assessed based on a mark out of 100 

The following information is a summary from your Course Description: 

  • Percentage Value of Task: 20% of the course marks 
  • Due date as specified in Course Description, submit the assignment in the Moodle shell 
  • Minimum time expectation: 20 hours (per student) 

This is a group assignment. Groups must contain two or three students as approved by your tutor/lecturer.  

Learning Outcomes Assessed 

The following course learning outcomes are assessed by completing this assessment: 

S1. Critically analyse and use complex decision making to research and determine the appropriate  Software Engineering tools and methodologies to utilize in a given situation 

S2. Apply professional communication skills to support and manage the engineering of a large software  system 

S3 Review, critically analyse and develop artefacts to define processes for quality assurance, risk  management and communication in large software development projects 

S4 Implement quality assurance activities in order to verify user requirements and validate design  decisions 

A1 Analysis of a large system development problem to decide upon the best methodological approach 

A2 Development of appropriate artefacts to support and manage the software engineering process such  as change control and configuration management 


Demonstrate an understanding of particular concepts covered in lectures, tutorials, laboratories and reading to  provide the specification requested. This may require further reading and research beyond the material discussed in  class.

Assessment Details 

This assignment will be assessed by your lecturer/tutor. The assignment requires you to produce a formal  specification containing the components identified below.  

Assessable Tasks/Requirements 

You are to provide both a brief written description of your requirements and create a set of Z schemas that  adequately describes the subsystem formally. It should include at least one state space and at least 3-4 operations Each group member must individually write two operations. The group should also write an initialization operation  called Init.  

You should provide robust versions of each operation that are capable of handling any possible error conditions. 

You should also add a narrative to explain any schemas or logic that you have used. Authorship should be made  clear. You might be asked to explain and answer questions about your work. 

Additional Information 

General Comments 

The submission must be presented in a professional, clear and concise manner. If you need further system information please use your initiative and make reasonable and logical assumptions. Questions of a general nature  (for example to clarify some part of the assignment requirements) can also be sent to the discussion forum but these  should not in any way provide solutions or parts thereof. 


The following resources will assist you with this assignment: 

  • Weeks 4 and 5 study materials and Section 4 of study guide three; 
  • The Z Notation: A Reference Manual (Spivey, 2001); 
  • Chapter 21, sections 21.5, 21.6 and 21.7 of Pressman (2010); 
  • Solutions for problem 2 of week 6 tutorial problems;
  • The Z Resources section of your Moodle shell; and 
  • Introduction to Z Notation –


One group member should submit an electronic copy of the Formal Specification via Moodle. Partner students please refer to your course lecturer for submission instructions. Please refer to the Course Description for information regarding late assignments, extensions, special consideration, and plagiarism.   

Marking Criteria 

Work will be assessed according to the following: 

  • Your Formal Specification must complete the items detailed within the Assessable Tasks/Requirements section of this document. 
  • Each student should indicate which sections of the submitted work they authored. 
  • Your Formal Specification should be presented as business or management style report which adheres to academic writing presentation standards. 
Item Description Max. Marks
Global Variables Correct declaration and initialisation 5
State Space Schema Correct declaration and type for variables
Correct predicates
Init Operation Correct initialisation of variables 5
Operation Correct schema for entry, error and success Correct robust expression 10
Operation Correct schema for entry, error and success Correct robust expression 10
Operation Correct schema for entry, error and success Correct robust expression 10
Report Adheres to guidelines given for assignment (Any assumptions must be clearly stated and appropriate) 5
Total Mark 60
Course Mark 30
Column Column Column


Assessment marks will be made available in fdlMarks, Feedback to individual students will be provided via Moodle or as direct feedback during your tutorial class.  


Plagiarism is the presentation of the expressed thought or work of another person as though it is one’s own without properly acknowledging that person. You must not allow other students to copy your work and must take care to  safeguard against this happening. More information about the plagiarism policy and procedure for the university can be found at: 

Any support material must be compiled from reliable sources such as the academic resources in Federation University library which might include, but not be limited to: the main library collection, library databases and the BONUS+ collection  as well as any reputable online resources (you should confirm this with your tutor).