Z Notation: A Case Study of Container Control System

This article discusses the Z Notation and its application in Container Control System. It explains the eight operations involved in the system and their interrelation. The article also highlights the importance of Z-schemas in understanding the internal nature of software programs.

Running head: Z Notation
Z Notation: A Case Study of Container Control System
Name of the Student
Name of the University
Author’s note

1Z NOTATION
Table of Contents
Introduction:...............................................................................................................................2
Initializing Operation:................................................................................................................2
Operation 1: Enter_new_container_terminal.............................................................................4
Operation 2: Accept_delivery....................................................................................................5
Operation 3: Accept_pickup......................................................................................................6
Operation 4: Leave_delivery_queue..........................................................................................7
Operation 5: Unload_Ship..........................................................................................................7
Operation 6: Container_terminal_account.................................................................................8
Operation 7: Ships_total_account..............................................................................................8
Operation 8: Freight_company_account....................................................................................9
Conclusion:................................................................................................................................9
Bibliography:............................................................................................................................10

2Z NOTATION
Introduction:
The Z-Notation has been evolved in the recent years so that software specification and
design can be done in a better way through identifying a standard set of notations. The Z-
notations does not only allow better capture of specification but also gathers the vital features
of the software methods. The Z permits the application designer to give a model of the model
as scientific notation that can be utilized to formalize the possibility of documentation
necessities. The Z-notation is utilized for making the notations in z-schema. The Z-notation is
formal numerical language that deals with scientific articulations. The Z-notation has
different components like passages, rationale, sets, schemas, relations, capacities, numbers,
arrangements and packs.
The study is completely based on the eight operations of terminal container control
system. These eight operations are inter related and uses most of the common variables
through entire life-cycle. The first operation adds the terminal and the following state
changing operations entails the lifecycle of the terminal. The last three operations are non-
state changing that means these three are used for collecting information, not entering new
data or altering existing one.
Initializing Operation:
The Z is not a programing that can be compiled for getting output against provided
inputs. Rather Z should be considered as the blueprint of a software that shows the structure
of the operations in the software. Various notations in the Z has individual meaning and many
notations are used for creating a Z-specification of particular software method. The Z-
specification utilize the mathematical notations for describing the properties of a software
program in an accurate manner. The notations entails what the program does along with
suggesting how it is actually done. This makes the Z-specification better than formal

3Z NOTATION
specification. The usage of the vast range of complex mathematical notation makes this
possible. The Z-specification is used as reliable and single reference pint for evaluating the
customer needs and developing programs for fulfilling those needs. The Z is consisting of
schemas that are decomposed from the specifications. The schemas are more understandable,
small in size and easily creatable. This is why, the Z specifications are always divided into z-
specifications first. The Schema is able to describe both the dynamic and static characteristics
of the software program. The static aspects are occupied states and invariant relations that are
maintained for supporting state alterations. The dynamic properties are potential operations of
the software program, relation among the operation input and output and state alterations.
initTerminal
name: ℕ
storage: ℕ
containerNumber: ℕ
ton: ℕ
containerNumber ≥ 0
ton ≥ 0
initDelivery
queVehicleNumber: ℕ
que: ℕ
queVehicleNumber ≤ 5
que ≤ 2
In this section, the variables are initialized before starting any operation. The
initialization allows to name the sets even without suggesting containing objects. The
initialization is done to all the global variables. The nature of the variables are stated in this
phase. The initialization is not an operation. This should be seen as the initiation of variables
before declaring the constructor or methods. The initialization states that vehicle numbers
must be less than five and que should be maximum two.

4Z NOTATION
Operation 1: Enter_new_container_terminal
initContainerTerminal
containerTerminal
known = ∅
addTerminal
ΔContainerTerminal1
name?: Name
storage?: Storage
containerNumber?: ContainerNumber
ton?: Ton
∀i: 1…hwm⦁name? ≠ names(i)
hwm' = hwm+1
name′ = names⊕{hwm′ ↦ names?}
storage′ = storages ⊕{hwm′ ↦ storage?}
containerNumber = containerNumbers ⊕ {hwm′ ↦ containerNumbers?}
ton = tons ⊕ {hwm′ ↦ tons?}
The variables are declared in the bottom part of the schema. The above section shows
the variables and whether it is user input or available data. The below section is for
operations. The Z-schema describes that state change is done in this operation. The container
terminal initialization states that the terminal data is empty. The first data will be entered
through the addTerminal operation. The name, storage, container number and more variables
are act as input. As this is the first data in the database, there is no existing value. The
terminal data are collected completely from the users. The system stores the terminal data and
it becomes available for other following operations. It can be assumed that if a terminal is
added, it cannot be deleted as the organization may want this data as historical data to create
new working strategies.

5Z NOTATION
Operation 2: Accept_delivery
acceptDelivery
ΔDelivery1
queVehicleNumber? : QueVehicleNumber
vehicleIdentifier? : VehicleIdentifier
∀i: 1…hwm⦁VehicleIdentifier? ≠ vehicleIdentifier(i)
hwm′ = hwm +1
currentLoad ≤ ton – storage
containerNumber ≤4
⇒(vehicleIdentifiers′ = VehicleIdentifier ⊕ {hwm′ ↦ VehicleIdentifier })
containerNumber = 5
⇒ (queVehicleNumber ′ = queVehicleNumber +1)
The delivery operation is done by one or more vehicles. Each delivery is done from a
source to a container. A vehicle will do the work of delivering products. Each time a deliver
is done, the system needs to initiates the pick operation. The schema describes change of
state.

6Z NOTATION
Operation 3: Accept_pickup
acceptPickup
ΔDelivery1
vehcileIdentifier? : VehicleIdentifier
freightCompany? : FreightCompany
qty? : Qty
tons? : Tons
∀i : 1…hwm⦁VehicleIdentifier? ≠ VehicleIdentifier(i)
hwm′ = hwm +1
currentLoad ≤ ton – storage
containerNumber ≤4
⇒(vehicleIdentifiers′ = VehicleIdentifier ⊕ {hwm′ ↦ VehicleIdentifier }
Tons′= Loads ⊕ {hwm′ ↦ Tons}
freightCompany′ = freightCompany
⊕ {hwm′
↦ freightCompany }
qty′ = qty ⊕ {hwm′ ↦ qty}
currentLoad′ = currentLoad ⊕ {hwm′ ↦ currentLoad })
containerNumber = 5
⇒ (queVehicleNumber ′ = queVehicleNumber +1
Tons′= Loads ⊕ {hwm′ ↦ Tons}
freightCompany′ = freightCompany
⊕ {hwm′
↦ freightCompany }
qty′ = qty ⊕ {hwm′ ↦ qty}
currentLoad′ = currentLoad ⊕ {hwm′ ↦ currentLoad })
The schema describes state change. The pickup acknowledge is the following period
of conveyance task. This activity will change the state of conveyance process. The
characteristics like vehicleIdentifier, frieghtCompany, amount and ton are utilized in this
activity. The entire procedure is driven to vehicle identifier. In the event that the number is 5
then the framework will add the new conveyance demand to que alongside the vehicle id. In
the event that the quantity of vehicles is under 5 then the vehicle will be allocated for
stacking container. The framework will figure the present load. The framework will likewise
check if the present load is not exactly or equivalent to accessible capacity in the container.

7Z NOTATION
Operation 4: Leave_delivery_queue
leaveDeliveryQue
Δque1
vehcileIdentifier? : VehicleIdentifier
waitingTime?: WaitingTime
preferredWaitingTime? : PreferredWaitingTime
error!: ℙ
preferredWaitingTime ≤ waitingTime
⇒(queVehicleNumber′ = queVehicleNumber - 1)
queVehicleNumber′ = ∅
⇒ error = No truck available in que
The driver will leave conveyance que of holding up time is more than favoured time.
As each truck has just a single driver, the framework will consider the driver as vehicle for
information respectability reason. The framework will likewise appear, the mistake message
of the que is vacant. The schema describes state change.
Operation 5: Unload_Ship
unloadShip
ΔcontainerTerminal1
qty?: X
ton? : Y
error!: Report
qty?* ton? ≥ storage
⇒ error!= no space available
qty?* ton? ≤ storage
⇒(storages′ = storages ⊕ {hwm′ ↦ qty?* ton? })
The trucks does the activity of emptying the ship. The framework computes which
vehicle is emptying which holder and how much measure of merchandise are emptied. The
framework will figure the measure of item by increasing the amount with ton. The capacity is
additionally refreshed when the vehicle empty the ship.

8Z NOTATION
Operation 6: Container_terminal_account
findComntainerTerminalAccount
ΞcontainerTerminal1
startDate! : Date
endDate! : Date
freightCompany? : FreightCompany
qty? : Qty
tons? : Tons
count1!: X
count2!: Y
freightCompany? ∈ known
Date! = endDate!- startDate!
qty?* ton? ≤ count1
qty?* ton? ≥ count2
Date! = containerTerminal(freightCompany?, qty?, tons?)
It outputs the total number and tonnage of containers delivered to a particular
container terminal by ALL freight companies in a specified time period (in this simplified
system, that is the total quantity and tonnes delivered between two specified global count
values.
Operation 7: Ships_total_account
findShipTotalAccount
ΞcontainerTerminal
name! = Name
qty? : Qty
tons? : Tons
name? ∈ known
name! = containerTerminal(qty?, tons?)
This schema is used for finding the total number and tonnage that a particular ship has
loaded from ALL container terminals in the total history of the system. The name means the
name of the ship. This value is provided by the user. Based on this input value, the system
will collect and show the data to the user.

9Z NOTATION
Operation 8: Freight_company_account
findFreightCompanyAccount
ΞcontainerTerminal
name! = Name
freightCompany? : FreightCompany
qty? : Qty
tons? : Tons
count1!: X
count2!: Y
freightCompany?
∈ known
qty?* ton? ≤ count1
qty?* ton? ≥ count2
freightCompany! = containerTerminal(qty?, tons?)
This operations describes that no state is changed for the schema. The terminal name
is essential for showing the output as users may not recognize the id of the company. The
operation implies the condition that to run the schema, the system must recognize the user
input freight company name. If the name is valid, then the system show the goods delivered
from a particular freight company to the terminal for two values count1 and count2.
Conclusion:
The above descriptions concludes that Z-schemas are great tool for understanding the
internal nature of the software programs. The Z has provided an idea about the states that has
been extensively used for implying change in database. The operations were interconnected
therefore many common variables has been utilized. Various operations were just opposite of
each other, those operations used the same variables along with some conditional values. The
implementation of the Z has become a great approach for describing the software operations.
The study has stated all the operations in the terminal container control system properly.
However, those operations were competitively simple than real life system operations. Two
or three complex operations could have made possible to apply more complex z-notations.

10Z NOTATION
Bibliography:
Ali, T. (2018). Z Notation Formalization of Blockchain Healthcare Document Sharing Based
on CRBAC. JOURNAL OF INFORMATION COMMUNICATION TECHNOLOGIES
AND ROBOTICS APPLICATIONS (JICTRA).(Formally known as NICE Research
Journal of Computer Science). ISSN# 2226-3683, 9, 16-29.
Bowen, J. P. (2016). The Z Notation: Whence the Cause and Whither the Course?. In
Engineering Trustworthy Software Systems (pp. 103-151). Springer, Cham.
El Miloudi, A. K., & ETTOUHAMI, A. (2015). A multi-view approach for formalizing UML
State Machine Diagrams Using Z Notation. WSEAS Transaction on Computers, 14,
72-78.
Klein, M. J., Sawicki, S., Roos-Frantz, F., & Frantz, R. Z. (2014, April). On the
Formalisation of an Application Integration Language Using Z Notation. In ICEIS (1)
(pp. 314-319).