Guide to Project for Supervisors
School of Engineering and Information Technology
ITECH7410 - Software Engineering Methodologies Assignment 2, 2018/17
__________________________________________________________________________________
CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 1 of 11
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.
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 Container Control System (CCS) 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
elationships 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 CCS. Your assignment should include at least one state space and provide schema for the
prescribed functions (including e
or handling) described below.
School of Engineering and Information Technology
ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17
__________________________________________________________________________________
CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 2 of 11
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 12, Thursday 4:00pm
Minimum time expectation: 20 hours (per student)
This is a group assignment. Groups must contain two students.
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
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.
School of Engineering and Information Technology
ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17
__________________________________________________________________________________
CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 3 of 11
Assessment Details
This assignment will be assessed by your lecture
tutor. The assignment requires you to produce a formal
specification containing the components identified below.
Background – Container Control System (CCS)
As a Software Engineering consultant, your task is to develop a formal specification in Z for the Container Control
System (CCS). The CCS is a new computerized system to be developed for the storage and handling of accounts
for freight companies and truck container deliveries/pickups to/from the Port of Melbourne (PoM) container terminals.
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 (we do not for example track individual containers but only truck deliveries
and pickups and ship loading and unloading and we assume one container size only (standard twenty-foot
equivalent unit (TEU)):
Container Terminal
The PoM cu
ently has four container terminals in Melbourne but the system must be written to seamlessly handle at
least twice that number.
Each terminal has a unique name and storage capacity (in number of containers and tonnes) that must be stored in
the proposed system.
The system must maintain the cu
ent tonnage and cu
ent number of containers in the container terminal.
When the container terminal is full no further deliveries of containers can be made to that container terminal and no
unloading of containers from ships can occur before some are loaded onto a ship for shipping to their destination or
some are picked up by trucks and taken away from the terminal.
Only five trucks can deliver into a particular container terminal at any one time and only five trucks can pick up
containers from the container terminal at any one time. During busy times each container terminal maintains two
queues of trucks - waiting to deliver and waiting to pick up.
Trucks wanting to deliver should only be entered into the waiting queue when there is sufficient room in the container
terminal for all the container(s) that the truck holds i.e. the system needs to know that the cu
ent storage plus all the
loads cu
ently in the queue will not exceed the container terminal’s capacity tonnage or number of containers
capacity.
School of Engineering and Information Technology
ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17
__________________________________________________________________________________
CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 4 of 11
For simplicity, we will say that a berth is always available for a ship to load or unload.
A container terminal cannot load more containers onto a ship than are cu
ently stored at the terminal.
A container terminal cannot unload more containers from a ship than there is available space at the terminal.
When a container terminal is loading containers onto a ship, operational and safety considerations dictate that no
trucks can deliver any containers to that container terminal (i.e. they must wait in the delivery queue).The system will
ensure that all deliveries and pickups cu
ently executing are completed before loading starts.
Similarly when a container terminal is unloading containers from a ship, operational and safety considerations dictate
that no trucks can pick up any containers from that container terminal (i.e. they must wait in the pickup queue). The
system will ensure that all deliveries and pickups cu
ently executing are completed before unloading starts.
Trucks
The system maintains a list of registered trucks, their registration, owner and their empty weight (in tonnes).
As each loaded truck a
ives at the container terminal, it is weighed to ascertain the weight of the containers on the
truck. This is calculated as the difference between the weight of the loaded truck and its empty weight. The number
of containers on the truck is also registered.
If there is sufficient room in the container terminal then the container(s) are placed in the container terminal and a
ecord is kept of the number and tonnage delivered against both the truck registration number and the freight
company providing the container(s).
When container(s) are placed on a truck to take them away from the terminal, the truck is weighed to ascertain the
weight of the containers on the truck and the number of containers taken away is also recorded.
Freight Companies
The system will maintain a record of each freight company that assigns trucks to deliver containers to the container
terminal and also each freight company that allocates trucks to pick up containers from the terminal.
Details to be kept include the freight company’s name, address and phone number.
Ships
The system will keep a record of all ships that have been registered to load or unload containers for the PoM.
The ship’s name, nationality (flag) and capacity (in number of containers and tonnes) will be stored.
School of Engineering and Information Technology
ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17
__________________________________________________________________________________
CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 5 of 11
The ship's captain can specify the number of containers and the tonnage to be loaded/unloaded onto/from the ship.
When loading a ship, the number of containers and tonnage to be loaded cannot be greater than the ships capacity
and cannot be more than the available number of containers and tonnage in storage. The ship cannot load until all
cu
ently executing deliveries and pickups have completed (any new truck deliveries and pickups are placed in the
appropriate queue). The system will keep a record of the number of containers and tonnage loaded onto the ship
and adjust the remaining storage capacity in the container terminal and ship appropriately.
When unloading a ship, the number of containers and tonnage to be unloaded cannot be greater than the remaining
storage capacity in the container terminal. The ship cannot unload until all cu
ently executing deliveries and pickups
have completed (any new truck deliveries and pickups are placed in the appropriate queue).The system will keep a
ecord of the number of containers and tonnage unloaded from the ship and adjust the remaining storage capacity in
the container terminal and ship appropriately.
Date