ITECH7410: Z-Language Formal Specification of Container Control System

This report details the formal specification of a terminal container control system using Z-language. It begins with an introduction to Z notation and its application in modeling system states and operations. The report then presents the Z-schema for the terminal container control system, including the initialization of variables such as terminal containers, product delivery queues, and product pickups. Several operations are defined using Z notation, including adding a new terminal, adding a product delivery, adding a product pickup, managing the product delivery queue, unloading a ship, and finding terminal and freight company information. The report concludes by highlighting the scalability and executability of Z notation for system specification, noting its suitability for modeling complex operations and data, while also acknowledging that Z is a specification language and not directly compiled. The provided notations are designed for accuracy and to manage operation-related data effectively.

Running head: Z-LANGUAGE: TERMINAL CONTAINER CONTROL SYSTEM
Z-Language: Terminal Container Control System
Name of the Student
Name of the University

1Z-LANGUAGE: TERMINAL CONTAINER CONTROL SYSTEM
Table of Contents
Introduction:...............................................................................................................................2
Z-Schema of Terminal Container Control System:...................................................................2
Conclusion:................................................................................................................................8
Bibliography:..............................................................................................................................9

2Z-LANGUAGE: TERMINAL CONTAINER CONTROL SYSTEM
Introduction:
The Z can be considered as the model based notation that represent states. These
states are consisted of values and variables. Some of the operations can change the state and
some does not. The Z-Models are also abstract data type as it can be characterized through
the operations. The Z is also used the functional style. The Z language should be considered
as method, it is just a notation for software specification modelling that supports various
methods.
The article represents states of container control system modelled using Z. The
initialization of all the variables of terminal container control system. Various operations in
the article change the state of variables and some operations do not.
Z-Schema of Terminal Container Control System:
initTerminalcontainer
id: ℙ terminalcontainerID
capacity: ID ⇸ terminalcontainerID
known = domTerminalcontainer
initTerminalcontainer
ΞTERMINALCONTAINER
Known = ∅
intTerminal
TerminalName: ℙ TERMINALNAME
terminalName: NAME ⇸ TERMINALNAME
capacity: ℕ
known = domterminal

3Z-LANGUAGE: TERMINAL CONTAINER CONTROL SYSTEM
intProductDeliveryque
productDeliveryque: ℕ
workingVehicleQuantity: ℕ
productDeliveryque≤2
intDeivery
deliveryID: ℕ
vehicleRegNo: ℕ
workingVehicleAmount: ℕ
frieghtCompanyName: FRIEGHTCOMPANYNAME
calculatedLoad: ℕ
weight: ℕ
quantity: ℕ
workingVehicleAmount ≤ 5
capacity ≥ weight*quantity
calculatedLoad ≤ capacity′
intProductPickup
vehicleRegNo: ℕ
vehicleRegNo: VEHICLEREGNO ⇸ ProductDelivery
weight: ℕ
quantity: ℕ
known = domvehicleRegNo
In this section, all the variables to be used in the system is initialized. It is a well
known fact that initialization of variables is a very important part of software domain. The
characteristics of the variables has been presented in the above z-notations like what kind of
variable it is, what should be its value and more.
Operation 1:

4Z-LANGUAGE: TERMINAL CONTAINER CONTROL SYSTEM
addTerminal
Δterminal1
terminalName?: NAME
capacity?: CAPACITY
∀i: 1…hwm. terminalName? ≠ terminalNames(i)
hwm′ = hwm+1
terminalNames′ = terminalNames⊕{hwm′ ↦ terminalName?}
capacities′ = capacities′{hwm′ ↦ capacity?}
This operation is run when a new terminal is added to the system. The terminal1 is
used so that the whole process remain unbiased. All the details of the operation will be
collected from the user. hwm′ = hwm+1 represents that a new row is added for new terminal.
Operation 2:
addProductDelivery
ΔProductDelivery1
ΔProductDeliveryque1
deliveryID: DELIVERYID
vehicleRegNo: VEHICLEREGNO
workingVehicleAmount: WORKINGVEHICLEAMOUNT
calculatedLoad: CALCULATEDLOAD
weight: WEIGHT
quantity: QUANTITY
∀i: 1…hwm⦁ deliveryID ≠ deliveryID(i)
hwm′ = hwm+1
vehicleRegNo = known
calculatedLoad = weight*quantity
workingVehicleAmount ≤4
⇒(vehicleRegNo′= vehicleRegNo⊕{hwm′ ↦ vehicleRegNo?})
workingVehicleAmount = 5
⇒(workingVehicleQuantity′= workingVehicleQuantity +1)
vehicleRegNo = vehicleRegNo⊕{productDeliveryque′ ↦ vehicleRegNo?}
This operation changes the state of productDelivery and productDeliveryQue. If the
delivery is accepted then the vehicle deliver the product to the terminal. The delivery is only

5Z-LANGUAGE: TERMINAL CONTAINER CONTROL SYSTEM
added when there is no more than 4 vehicle currently delivering goods. In case all five trucs
are delivering product, the system adds the vehicle, ready for delivery to que.
Operation 3:
addProductPickup
ΔproductPickup1
ΔproductDelivery1
vehicleRegNo: VEHICLEREGNO
frieghtCompanyName: FRIEGHTCOMPANYNAME
weight: WEIGHT
quantity: QUANTITY
∀i: 1…hwm⦁ vehicleRegNo ≠ vehicleRegNo(i)
hwm′ = hwm+1
calculatedLoad = weight*quantity
capacity ≥ calculatedLoad
workingVehicleAmount ≤4
⇒(vehicleRegNo′= vehicleRegNo⊕{hwm′ ↦ vehicleRegNo?})
workingVehicleAmount = 5
⇒(workingVehicleQuantity′= workingVehicleQuantity +1)
vehicleRegNo = vehicleRegNo⊕{productDeliveryque′ ↦ vehicleRegNo?}
The productpickup operation is similar to productdelivery, it’s just more based on the
ground level conditions. The system checks if the current load to be delivered by the vehicle
is less or equal to available storage capacity of terminal. It also checks also the number of
currently delivering vehicles.
Operation 4:

6Z-LANGUAGE: TERMINAL CONTAINER CONTROL SYSTEM
addLeaveProductDeliveryque
ΔproductDelivery1
waitingTime?: ℙ
preferedTime?: ℙ
numberOfVehicleInQue?: numberOfVehicleInQue
waitingTime≥ preferedTime
numberOfVehicleInQue′ = numberOfVehicleInQue -1
Error: ′The driver left the productDeliveryque′
This operation changes the productDeliveryQue. Suppose the driver does not want to
wait for the time system estimated. The driver can leave the que and system
Operation 5:
unloadShip
ΔTerminal1
weight?: X
quantity?: Y
unloadAmount?: UNLOADAMOUNT
unloadAmount = weight*quantity
unloadAmount ≥ capacity
⇒ Error: ′not available′
unloadAmount ≤ capacity
⇒(unloadAmount′)
The ship unload operation changes the state of terminal and increases the available
storage capacity. The amount of products to be unloaded from the ship terminal is dependent
on the system.
Operation 6:

7Z-LANGUAGE: TERMINAL CONTAINER CONTROL SYSTEM
findTerminal
Ξterminal
name?: NAME
date1: DATE1
date2: DATE2
frieghtCompanyName: FRIEGHTCOMPANYNAME
weight: WEIGHT
quantity: QUANTITY
name? ∈ known
date1 ≤ terminal(frieghtCompanyName, weight, quantity) ≤ date2
Operation 7:
findShipTotalAccount
Ξterminal
name?: NAME
weight: WEIGHT
quantity: QUANTITY
name? ∈ known
name! = terminal(quantity, weight)
Operation 8:
findFreightCOmpany
ΞproductDelivery1
frieghtCompanyName?: FRIEGHTCOMPANYNAME
weight: WEIGHT
quantity: QUANTITY
value1! = VALUE1
value2! = VALUE2
frieghtCompanyName? ∈ known
quantity*weight ≥ value1
⇒(frieghtCompanyName! = terminal(quantity, weight))
quantity*weight ≤ value1
Error! = ′Not available′

8Z-LANGUAGE: TERMINAL CONTAINER CONTROL SYSTEM
Conclusion:
The Z-notation is very scalable executable notation. This notation has the capacity of
supporting any operation of any system. The Z is not programming language and that is why
it cannot be compiled. The notations described in the system is very accurate and able to
sustain all the operation related data.

9Z-LANGUAGE: TERMINAL CONTAINER CONTROL SYSTEM
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.