ITECH7410 Software Engineering: Z Notation for Container Control

This document presents a formal specification of a container terminal control system using Z notation. It includes the initialization of variables and states, along with definitions of various operations such as adding a terminal, accepting delivery, accepting pickup, leaving the delivery queue, unloading a ship, and finding terminal/ship/company accounts. Each operation is described with pre and post conditions, and error handling is included where appropriate. The specification aims to provide a rigorous and unambiguous description of the system's behavior, facilitating formal verification and design derivation.

Running head: FORMAL SPECIFICATION IN Z
Z Notation: Terminal Container Control System
Name of the Student
Name of the University
Author’s note

1FORMAL SPECIFICATION IN Z
ContainerTerminal
known: ℙ containerName
storageCapacity: containerName ⇸ NAME
known = domContainer
Container
ΞTERMINAL
Known = ∅
Que
que: ℕ
queLength: ℕ
que≤2
Deivery
truckID: ℕ
activeVehicle: ℕ
frieghtCompany: FRIEGHTCOMPANY
presentLoad: ℕ
ton: ℕ
qty: ℕ
activeVehicle ≤ 5
availableStorage ≥ ton*qty
presentLoad ≤ availableStorage ′
Figure 1: Initialization of Variables and States
(Source: Created by Author)
The initialization is done for every global variable in the system. The container
storage capacity will be different for every terminal container. Every major states in the Z of
Container Control System has been initialized. The range of the variables has also been stated
in the initialization of the Z.

2FORMAL SPECIFICATION IN Z
addTerminal
Δterminal1
terminalName?: NAME
storageCapacity?:
STORAGECAPACITY
ton?:
TON
qty?:
QTY
∀i: 1…hwm. terminalName? ≠ terminalNames(i)
hwm′ = hwm+1
terminalNames′ = terminalNames⊕{hwm′ ↦ terminalName?}
storages′ = storages′{hwm′ ↦ storage?}
asas
as
Figure 2: Operation 1 – Enter New Container Terminal
(Source: Created by Author)
The rows of the values will start from 1 to without a limit. The terminal state will
change after the operation will be executed. Each terminal name and storage capacity will be
recorded into system through this operation.
addDelivery
ΔDelivery1
ΔQue1
truckID: TRUCKID
activeVehicle: ACTIVEVEHICLE
presentLoad: PRESENTLOAD
ton: TON
qty: QTY
∀i: 1…hwm⦁ truckID ≠ truckID(i)
hwm′ = hwm+1
truckID ∈ known
terminalName ∈ known
presentLoad = ton*qty
activeVehicle ⇔ 5
⇒(queLength′= queLength +1)
truckID = truckID⊕{que′ ↦ truckID?} (truckID′= truckID⊕{hwm′ ↦ truckID?})
activeVehicle < 5
⇒(truckID′= truckID⊕{hwm′ ↦ truckID?})
Figure 3: Operation 2 - Accept_delivery

3FORMAL SPECIFICATION IN Z
(Source: Created by Author)
The Z will result into change of two states if the operation is executed. There is
condition in the operation that active vehicle quantity must not exceed five and no more than
five trucks can be active in the process for every container.
intDelivery
ΔDelivery1
deliveryID? : DeliveryID
truckID? : TruckID
companyID? : CompanyID
qty? : Qty
tons? : Tons
∀i : 1…hwm⦁ deliveryID? ≠ deliveryID (i)
hwm′ = hwm +1
truckID ∉ known
⇒( truckIDs′ = TruckID
⊕ {hwm′
↦ TruckID})
truckID ∈ known
terminalName ∈ known
presentLoad ≤ availableStorage
⇒(truckIDs′ = TruckID ⊕ {hwm′ ↦ TruckID}
Tons′= Loads ⊕ {hwm′ ↦ Tons}
companyID′ = companyID ⊕ {hwm′
↦ companyID }
qty′ = qty ⊕ {hwm′ ↦ qty}
presentLoad′ = presentLoad ⊕ {hwm′ ↦ presentLoad })
presentLoad > availableStorage
⇒ (Error!: “Available storeage is less than currrent load”)⇒
⇒
Figure 4: Operation 3 – Accept Pickup
(Source: Created by Author)
The vehicle number will be entered into the system if it is not known. The Z entails
that the state will change after operation execution. The present load is a very essential part of
pickup as the load to be taken by the vehicle should be less than available storage. As the
pickup is only done after vehicle is not in que, the pick will be assigned directly.

4FORMAL SPECIFICATION IN Z
leaveQue
Δdelivery1
konwn: ℙ waitingTime
konwn: ℙ preferedTime
waitingTime≥ preferedTime
⇒(Error!: ′The driver left the que′)
Figure 5: Operation 4 - Leave_delivery_queIDue
(Source: Created by Author)
The driver can leave the que if he/she does not want to wait for the delivery to start.
This is the integral part of inserting a vehicle to que. This operation occurs before a vehicle is
entered into the que. This Z can change the state.
unloadShip
ΔDelivery1
qty?: X
ton? : Y
error!: Report
qty?* ton? ≥ containerStorage
⇒ error!= no space available
qty?* ton? ≤ containerStorage
⇒( storageCapacity′ = storageCapacity ⊕ {hwm′ ↦ qty?* ton? })
Figure 6: Operation 5 – Unload Ship
(Source: Created by Author)
The unload ship is also a delivery task but it occurs in opposite direction. The
containers on ships are emptied by the trucks.

5FORMAL SPECIFICATION IN Z
findTerminal
Ξterminal
name?: NAME
date1: DATE1
date2: DATE2
frieghtCompany: FRIEGHTCOMPANY
ton: TON
qty: QTY
name? ∈ known
date1 ≤ terminal(frieghtCompany, ton, qty) ≤ date2
Figure 7: Operation 6 – Container Terminal Account
(Source: Created by Author)
The total amount of load delivered by all the freight companies are found. This Z does
not alter state.
findShipTotalAccount
ΞcontainerTerminal
name! = Name
qty? : Qty
tons? : Tons
name? ∈ known
name! = containerTerminal(qty?, tons?)
Figure 8: Operation 7 - Ships_total_account
(Source: Created by Author)
The entire amount of load sent to a specific ship is found.

6FORMAL SPECIFICATION IN Z
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?)
Figure 9: Operation 8 - Freight_company_account
(Source: Created by Author)
The individual supplied loads from individual freight companies.

7FORMAL SPECIFICATION IN Z
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, pp.16-29.
Klein, M.J., Sawicki, S., Roos-Frantz, F. and Frantz, R.Z., 2014, April. On the Formalisation
of an Application Integration Language Using Z Notation. In ICEIS (1) (pp. 314-319).