Z Notation for Container Control System

This article discusses the use of Z Notation for Container Control System using mathematical expressions. It explores the various operations and schemas used in the system, including initializing operations, delivery operations, and account operations. The article also discusses the error reports generated by the system and the notation pattern used for describing the schema of each state.

Running head: Z Notation
Z Notation
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.............................................................................3
Operation 2: Accept_delivery....................................................................................................4
Operation 3: Accept_pickup......................................................................................................5
Operation 4: Leave_delivery_queue..........................................................................................6
Operation 5: Unload_Ship..........................................................................................................6
Operation 6: Container_terminal_account.................................................................................7
Operation 7: Ships_total_account..............................................................................................7
Operation 8: Freight_company_account....................................................................................8
Conclusion:................................................................................................................................8
Bibliography:..............................................................................................................................9

2Z NOTATION
Introduction:
The software applications developed at present days are consisting of high amount f
documentation such as interactive manuals, user guides, documents of design and many
more. The Z allows the system engineer to provide a model of the system in the form of
mathematical notation that can be used to formalize the idea of documentation requirements
(Abad, Noaeen & Ruhe, 2016). The Z-Language is used for creating the notations in z-
schema. The Z-Language is formal mathematical language that works on mathematical
expressions. The Z-language has various elements like paragraphs, schemas, logic, sets,
relations, functions, numbers, sequences and bags.
The article is based on the information of Container Control System using the Z-
Schema language. The Z-Notation is created based on the operations of container control
system. The initial operations are used for initializing the works.
Initializing Operation:
initTerminal
name: ℕ
containerStorage: ℕ
numberOfContainer: ℕ
ton: ℕ
numberOfContainer ≥ 0
ton ≥ 0
initDelivery
vehicleNumber: ℕ
queID: ℕ
vehcileIdentifier ≤ 5
queID ≤ 2
The initialization operations make the system processes initialize. The terminal
schema has name, storage, containerNumber and ton attribute. The containerNumber and ton

3Z NOTATION
must be greater than 0. The name identifies the name of the container so that system can
uniquely identify it during an operation. The Delivery schema is also initialised in this
section. The vehicle and que has integral part in delivery. The vehicleIdentifier means
number of vehicles are processing current delivery. It should always be less o equal to 5. As
this attribute is a Natural number it cannot be negative. These two schemas are the base of all
the operations.
Operation 1: Enter_new_container_terminal
initContainerTerminal
containerTerminal
known = ∅
addTerminal
ΔContainerTerminal1
name?: Name
containerStorage?: ContainerStorage
numberOfContainer?: NumberOfContainer
ton?: Ton
∀i: 1…hwm⦁name? ≠ names(i)
hwm' = hwm+1
name′ = names⊕{hwm′ ↦ names?}
containerStorage′ = containerStorages ⊕{hwm′ ↦ containerStorage?}
numberOfContainer = numberOfContainers ⊕ {hwm′ ↦ numberOfContainers?}
ton = tons ⊕ {hwm′ ↦ tons?}
This schema is used for recording a new terminal in the container system. It is
assumed that the terminal is empty at the beginning of this operation. The known = ∅, means
that system does not have any record of container. As the state of the containerControl will
change, the system. For each container system, the name, storage, containerNumber and ton
are added.

4Z NOTATION
Operation 2: Accept_delivery
acceptDelivery
ΔDelivery1
numberOfVehiclesInQue? : NumberOfVehiclesInQue
vehicleNumber? : VehicleNumber
∀i: 1…hwm⦁VehicleNumber? ≠ vehicleNumber(i)
hwm′ = hwm +1
currentLoad ≤ ton – containerStorage
numberOfContainer ≤4
⇒(vehicleNumbers′ = VehicleNumber ⊕ {hwm′ ↦ VehicleNumber })
numberOfContainer = 5
⇒ (numberOfVehiclesInQue ′ = numberOfVehiclesInQue +1)
The dynamic operations starts from here. The container control system will start
checking predefined conditions. The system will check if quantity of vehicle working for
loading is less than 5 or not. If the number is 5 then the system will add the new delivery
request to que along with the vehicle id. If the number of vehicles is less than 5 then the
vehicle will be assigned for loading container.
Operation 3: Accept_pickup
acceptPickup
ΔDelivery1
vehcileIdentifier? : VehicleNumber
companyID? : CompanyID
qty? : Qty

5Z NOTATION
tons? : Tons
∀i : 1…hwm⦁VehicleNumber? ≠ VehicleNumber(i)
hwm′ = hwm +1
currentLoad ≤ ton – containerStorage
numberOfContainer ≤4
⇒(vehicleNumbers′ = VehicleNumber ⊕ {hwm′ ↦ VehicleNumber }
Tons′= Loads ⊕ {hwm′ ↦ Tons}
companyID′ = companyID
⊕ {hwm′
↦ companyID }
qty′ = qty ⊕ {hwm′ ↦ qty}
currentLoad′ = currentLoad ⊕ {hwm′ ↦ currentLoad })
numberOfContainer = 5
⇒ (numberOfVehiclesInQue ′ = numberOfVehiclesInQue +1
Tons′= Loads ⊕ {hwm′ ↦ Tons}
companyID′ = companyID
⊕ {hwm′
↦ companyID }
qty′ = qty ⊕ {hwm′ ↦ qty}
currentLoad′ = currentLoad ⊕ {hwm′ ↦ currentLoad })
The pickup accept is the next phase of delivery operation. This operation will change
the state of delivery process. The attributes like vehicleIdentifier, frieghtCompany, quantity
and ton are used in this operation. The whole process is centric to vehicle identifier. If the
number is 5 then the system will add the new delivery request to que along with the vehicle
id. If the number of vehicles is less than 5 then the vehicle will be assigned for loading
container. The system will calculate the current load. The system will also check if the
current load is less than or equal to available storage in the container.
Operation 4: Leave_delivery_queue
leaveDeliveryQueID
ΔqueID1
vehcileIdentifier? : VehicleNumber
waitingTime?: WaitingTime
preferredWaitingTime? : PreferredWaitingTime
error!: ℙ
preferredWaitingTime ≤ waitingTime
⇒(numberOfVehiclesInQue′ = numberOfVehiclesInQue - 1)
numberOfVehiclesInQue′ = ∅
⇒ error = No truck available in queID

6Z NOTATION
The driver will leave delivery que of waiting time is more than preferred time. As
each truck has only one driver, the system will consider the driver as vehicle for data integrity
purpose. The system will also show, the error message of the que is empty.
Operation 5: Unload_Ship
unloadShip
ΔcontainerTerminal1
qty?: X
ton? : Y
error!: Report
qty?* ton? ≥ containerStorage
⇒ error!= no space available
qty?* ton? ≤ containerStorage
⇒(containerStorages′ = containerStorages ⊕ {hwm′ ↦ qty?* ton? })
The vehicles does the job of unloading the ships. The system calculates which vehicle
is unloading which container and how much amount of goods are unloaded. The system will
calculate the amount of product by multiplying the quantity with ton. The storage is also
updated when the vehicle unload the ship.
Operation 6: Container_terminal_account
findComntainerTerminalAccount
ΞcontainerTerminal1
startDate! : Date
endDate! : Date
companyID? : CompanyID
qty? : Qty
tons? : Tons
companyID? ∈ known
Date! = endDate!- startDate!
Date! = containerTerminal(companyID?, qty?, tons?)
Find container terminal account does not change the state of operation. The data find
in the operation will be restricted by two dates. The operation will identify the amount of

7Z NOTATION
product delivered by a freightCompany within given deadline. The user of the system will
enter the deadlines.
Operation 7: Ships_total_account
findShipTotalAccount
ΞcontainerTerminal
name! = Name
qty? : Qty
tons? : Tons
name? ∈ known
name! = containerTerminal(qty?, tons?)
The shipment account is identified using the name of the container, quantity and ton.
The name of the container must be known. The system must find the storage of the container
based on the name of the container.
Operation 8: Freight_company_account
findCompanyIDAccount
ΞcontainerTerminal
name! = Name
companyID? : CompanyID
qty? : Qty
tons? : Tons
count1!: X
count2!: Y
companyID?
∈ known
qty?* ton? ≤ count1
qty?* ton? ≥ count2
companyID! = containerTerminal(qty?, tons?)
Finding the fright company does not also change the state of Delivery. The system
finds how much amount of products are delivered by the freight company from beginning.
The system first checks the freight company name.

8Z NOTATION
Conclusion:
The above study concludes that the system will effectively handle the process of the
container control system. The system will handle all the operations properly. The system will
generate proper error reports when predefined metrics are not met. The specification
statements looks similar to each other. It is because a specific notation pattern has been
followed for describing the schema of each state.

9Z NOTATION
Bibliography:
Abad, Z. S. H., Noaeen, M., & Ruhe, G. (2016). Requirements engineering visualization: a
systematic literature review. In Requirements Engineering Conference (RE), 2016
IEEE 24th International (pp. 6-15). IEEE.
Iqbal, M. Z., Arcuri, A., & Briand, L. (2015). Environment modeling and simulation for
automated testing of soft real-time embedded software. Software & Systems
Modeling, 14(1), 483-524.
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).
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).
Spivey, J. M., & Abrial, J. R. (1992). The Z notation (p. 90). Hemel Hempstead: Prentice
Hall.
Zamli, K. Z., Alkazemi, B. Y., & Kendall, G. (2016). A tabu search hyper-heuristic strategy
for t-way test suite generation. Applied Soft Computing, 44, 57-74.