School of Engineering and Information Technology
ITECH7410 - Software Engineering Methodologies
__________________________________________________________________________________
Assignment 2 – Formal System
Specification
Overview
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 or three.
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 the Wheat Truck Control (WTC) System described below. 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 WTC. Your assignment should include at least one state space and provide schema for the prescribed functions (including error handling) described below.
__________________________________________________________________________________ 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: Week 11, Thursday 4:00pm
Minimum time expectation: 20 hours
This is a group assignment. Groups must contain either two or three students.
Learning Outcomes Assessed
The following course learning outcomes are assessed by completing this assessment:
K1 Critique and evaluate the latest directions in Software Engineering Methodologies
K2 Analyse and apply complex decision making to determine the appropriate methodology to apply to different development situations
K3. Develop a good understanding of processes to ensure quality in the engineering of large software systems
K4 Develop a good understanding of the principles of commonly used Software Engineering Methodologies
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
Requirements
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.
Background – Wheat Truck Control (WTC) System
As a Software Engineering consultant, your task is to develop a formal specification in Z for the Wheat Truck Control (WTC) System. The WTC is a new computerized system to be developed for the storage and handling of accounts for wheat farmers and truck deliveries to the Poortland Wheat Board (PWB) silos.
This system could be quite complicated. However, to simplify the system for this assignment only the following detail will be included in the proposed system:
Silos
The Board currently has ten (10) wheat silos around the country but the system must be written to seamlessly handle at least twice that number.
Each silo has a unique name and storage capacity (in tonnes) that must be stored in the proposed system.
The system must maintain the current amount of wheat stored in the silo.
When the silo is full no further deliveries of wheat can be made to that silo before some is off-loaded onto a ship for export overseas.
A silo cannot off-load more wheat onto a ship than is currently stored.
When a silo is off-loading to a ship, operational and safety considerations dictate that no trucks can unload to that silo.
Only one ship can be handled at a time at each silo.
Only one truck can unload into a particular silo at any one time. Therefore during busy times each silo also maintains a queue of trucks waiting to unload.
Trucks wanting to unload should only be entered into the waiting queue when there is sufficient room in the silo for
__________________________________________________________________________________
the wheat that the truck holds i.e. the system needs to know that the current storage plus all the loads currently in the queue will not exceed the silo’s capacity. Ships
The system will keep a record of all ships that have been registered to transport wheat overseas for the PWB. The ship’s name, nationality and capacity (in tonnes) will be stored.
The ship's captain can specify the amount of wheat to be off-loaded onto the ship. The amount to be offloaded cannot be greater than the ships capacity and cannot be more than the available grain in storage.
The system will keep a record of the amount of wheat off-loaded to the ship and adjust the remaining storage capacity in the ship appropriately.
Trucks
The system maintains a list of registered trucks, their owner and their empty weight (in tonnes).
As each loaded truck arrives at the silo, it is weighed to ascertain the amount of wheat in the truck. This is calculated as the difference between the weight of the loaded truck and its empty weight.
If there is sufficient room in the silo then the wheat is off-loaded into the silo and a record is kept of the amount offloaded against both the truck registration number and the farmer providing the wheat.
Farmers
The system will maintain a record of each farmer that supplies wheat to the silo.
Details to be kept include the farmer’s name, address and phone number.
Date and Time
Normally the date and time of each operation (truck delivery or ship off-loading) would be recorded. However to simplify this assignment those aspects will be ignored. Instead, a sequential count of each operation for each silo should be kept. Therefore, there should be a history of the order of truck unloading and ship off-loading operations that take place for each silo.
The system would be able to say for example, that silo POORTLAND_1, count 999 involved 25 tonnes of wheat delivered by the truck registered TONKA owned by Jack Black from farmer Bob Smith. Then the operation with a count of 1000 was an off-loading operation of 125,000 tonnes to the ship -Southern Aurora-.
__________________________________________________________________________________
There is also a need to keep track of the operation order between silos. Therefore a global sequential number of the operations at silos should be kept as well. The following table gives an example of what is required:
Global No Silo Count Operation Vehicle
Reg Name Tonnes Farmer
12336 POORTLAND_1 999 Load TONKA 25 Smith, Bob
12337 MELBOURNE 555 Load DUPLO 20 Jones, Mark
12338 POORTLAND_1 1000 Off-Load Southern Aurora 125,000
12339 MELBOURNE 556 Load LEGGO 50 Simons,
Jill
12340 POORTLAND_1 1001 Load TONKA 25 Jones, Mark
...
Assessable Tasks/Requirements
You are to create a set of Z schemas that adequately describes the WTC system. It should include at least one state space and the following operations:
• An initialization operation called Init.
• An operation Enter_new_silo that an operator uses to enter the details of a new silo into the system.
Assume the new silo is currently empty.
• An operation Accept_delivery that an operator uses to signal to the system to begin off-loading x tonnes of wheat from a truck. Note that the system must do a check to see if that storage capacity is available in the silo. If it is not then an error message must be output and no truck unloading occurs. Additional information needed by this routine is the truck registration and the farmer’s name. If successful, this operation stores all necessary details into the system for that delivery. If a truck is already unloading then this new truck will be placed in a queue waiting for its turn to unload.
• An operation Leave_queue. This operation is run by the system operator each time there is a queue for a silo and the driver of a specified truck decides that the anticipated waiting time is too long and leaves the queue. The operation outputs to the operator the list of trucks in the queue after the specified truck is removed. If no trucks are left in the queue a reasonable error message should be produced.
__________________________________________________________________________________
• An operation Silo_account that outputs the total amount of wheat in tonnes delivered to a particular silo by ALL farmers in a specified time period (in this simplified system, that is all tonnes delivered between two specified global count values e.g. 10000 and 10500).
• An operation Ships_total_account that outputs the total amount of wheat that a particular ship has taken from ALL silos in the total history of the system.
• An operation Farmers_account that outputs the total amount of wheat delivered to ALL silos between two specified global count values.
You should provide robust versions of each operation that are capable of handling any possible error conditions. For example, if the ship or truck is not correctly registered in the system an appropriate error message must be given.
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.
Readings
The following readings 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;
• Introduction to Z Notation - http://www.youtube.com/watch?v=qfEe9luJmVE
__________________________________________________________________________________
Submission
One group member should submit an electronic copy of the WTC 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. A reminder all academic regulations can be accessed via the university’s website, see: http://federation.edu.au/staff/governance/legal/feduni-legislation/feduni-statutes-and-regulations
Marking Criteria
Work will be assessed according to the following:
• Your WTC Formal Specification must complete the items detailed within the Assessable Tasks/Requirements section of this document.
• Your WTC Formal Specification should be presented as business or management style report which adheres to academic writing presentation standards. Where applicable, it must contain high quality academic presentation, expression and features as outlined in:
o Federation University’s
? Assignment Layout and Appearance Guidelines;
? General Guide to Writing and Study Skills,
? General Guide to Referencing; and
o Features of Academic Writing (from UEfAP.com)
__________________________________________________________________________________
Marking Rubric
Student Name and No Marker
Date
Item Description Max.
Marks Student Mark
Global Variables Correct declaration and initialisation 5
State Space Schema Correct declaration and type for variables
Correct predicates 10
Init Operation Correct initialisation of variables 5
Enter_new_silo Operation Correct schema for entry, error and success
Correct robust expression 10
Accept_delivery Operation Correct schema for test of available room, successful delivery and error
Correct robust expression 15
Leave_queue
Operation Correct schema for removal of truck, list of trucks in queue and error
Correct robust expression 15
Silo_account Operation Correct declaration and type for variables
Correct predicates 10
Ships_total_account Operation Correct schema for report and error (no ship in system)
Correct robust expression 10
Farmers_account Operation Correct declaration and type for variables
Correct predicates 10
Report Adheres to guidelines given for assignment and stated at https://federation.edu.au/current-students/learningand-study/online-help-with/study-skills-and-writingguides (Any assumptions must be clearly stated and appropriate) 10
Total Mark 100
__________________________________________________________________________________
Course Mark 20
Comments:
Feedback
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
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:
http://federation.edu.au/students/learning-and-study/online-help-with/plagiarism.
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).
References
Pressman, R.S. (2010). Software Engineering: A Practitioners Approach (7th ed). McGraw-Hill. ISBN: 978007-126782-3
Spivey, J.M. (2001). The Z Notation: A Reference Manual (2nd ed.). Oxford, England : Author. ( http://spivey.oriel.ox.ac.uk/mike/zrm/zrm.pdf)
Page