Z-Language Specification and Modeling of a Container Control System

This report provides a formal specification of a container control system using the Z-Notation. It begins with an introduction to Z-language as a formal specification language based on first-order predicate logic and axiomatic set theory. The core of the report focuses on modeling the container control system using Z-schemas, defining abstract data types, state spaces, and operations such as accepting delivery, picking up delivery, and handling terminal operations. Specific Z-schemas are presented for initializing the container system, adding terminals, managing deliveries and pickups, handling queue departures, unloading ships, and finding terminal and freight company information. Each operation includes pre- and post-conditions defined within the Z-notation to ensure system integrity and consistency. The report concludes that the defined operations effectively support the container control mechanism, enabling potential automation of backend processes, while acknowledging that additional processes could be included.

Running head: Z-LANGUAGE
Z-Language: Container Control System
Name of the Student
Name of the University

1Z-LANGUAGE
Table of Contents
Introduction:...............................................................................................................................2
Z-Schema of Container Control System:...................................................................................2
Conclusion:................................................................................................................................7
Bibliography:..............................................................................................................................9

2Z-LANGUAGE
Introduction:
The software systems are modelled and described using the z-notation. This language
is a formal specification language. The first-order predicate logic, axiomatic set theory, and
lambda calculus are used as the base of this formal specification mathematical notations.
The whole article is completely based on the modelling the software named container
control system using the Z-Notation. The operations like accepting delivery, picking up
delivery, finding infraction are described through this notation.
Z-Schema of Container Control System:
The abstract data type provided in the article is a collection of states called state
space. This state space of container control system is a non-empty state and various
operations. Every operation of container control system consist of input and output variables.
There are relationship between input and output variables. In the proposed container control
system Z, the abstract data type state set is defined by a schema named as data type itself.
initContainer
id: ℙ containerIdentificationNumber
containerIdentificationNumber: ID ⇸ containerIdentificationNumber
known = domcontainername
initContainer
ΞTERMINAL
Known = ∅
intTerminal
name: ℙ nameOfTerminal
nameOfTerminal: NAME ⇸ NAMEOFTERMINAL
storingCapacityOfContainer: ℕ
known = domterminalnamea

3Z-LANGUAGE
intQue
queIdentification: ℕ
existingVehicle: ℕ
queIdentification≤2
intDeivery
vehicleIdentificationNumber: ℕ
quantityOfVehicle: ℕ
frieghtCompanyName: FRIEGHTCOMPANYNAME
currentLoad: ℕ
wieghtAmount: ℕ
quantity: ℕ
quantityOfVehicle ≤ 5
storingCapacityOfContainer ≥ wieghtAmount*quantity
currentLoadAtDelivery≤ storingCapacityOfContainer′
intPickup
vehicleIdentificationNumber: ℕ
vehicleIdentificationNumber: VEHICLEIDENTIFICATIONNUMBER ⇸ Delivery
wieghtAmount: ℕ
quantity: ℕ
known = domvehicleIdentificationNumber
The collection of initial state of the container control system abstract data type is
specified by a different schema but has the same signature as the state space schema. The
above Z-schemas describe initial state of the terminal, delivery, pickup and more. For every
state schema in the operation there is at least one initial state.
Operation 1:

4Z-LANGUAGE
addTerminal
Δterminal1
nameOfTerminal?: NAME
storingCapacityOfContainer?:
STORINGCAPACITYOFCONTAIN
ER
wieghtAmount?:
WIEGHTAMOUNT
quantity?:
QUANTITY
∀i: 1…hwm. nameOfTerminal? ≠ nameOfTerminals(i)
hwm′ = hwm+1
nameOfTerminals′ = nameOfTerminals⊕{hwm′ ↦ nameOfTerminal?}
storingCapacityOfContainers′ = storingCapacityOfContainers′{hwm′ ↦ storingCapacityOfContainer?}
asas
as
The operations mentioned in the whole article like addTerminal are extended by the
data refinement. This is achieved by allowing the state space of Terminal operation to be
alternative from the abstract operation state space. The Δterminal1 states that the schema is
about state change. The schema has four variables. The first one is for storing the name of
terminal, the second one is for specifying the capacity of the container terminal, the third and
fourth is for specifying average loads put on the container.
Operation 2:

5Z-LANGUAGE
addDelivery
ΔDelivery1
ΔQueIdentification1
vehicleIdentificationNumber: VEHICLEIDENTIFICATIONNUMBER
quantityOfVehicle: QUANTITYOFVEHICLE
currentLoad: CURRENTLOAD
wieghtAmount: WIEGHTAMOUNT
quantity: QUANTITY
∀i: 1…hwm⦁ vehicleIdentificationNumber ≠ vehicleIdentificationNumber(i)
hwm′ = hwm+1
vehicleIdentificationNumber = known
currentLoadAtDelivery= wieghtAmount*quantity
quantityOfVehicle ≤4
⇒(vehicleIdentificationNumber′= vehicleIdentificationNumber⊕{hwm′ ↦ vehicleIdentificationNumber?})
quantityOfVehicle = 5
⇒(existingVehicle′= existingVehicle +1)
vehicleIdentificationNumber = vehicleIdentificationNumber⊕{queIdentification′ ↦ vehicleIdentificationNum
The schema is also describe the change of state. This schema describes that two states
will be changed. The first variable input shows the unique identifier of vehicle which is
assigned the delivery. The quantity of vehicle is for determining how many vehicles are
currently delivering goods to the container. The schema describes that no more than five
vehicles should doing delivery. If number of active vehicles in the delivery is five then last
delivery vehicle is added to the que else the vehicle starts delivery.
Operation 3:

6Z-LANGUAGE
addPickup
Δpickup1
Δdelivery1
vehicleIdentificationNumber: VEHICLEIDENTIFICATIONNUMBER
frieghtCompanyName: FRIEGHTCOMPANYNAME
wieghtAmount: WIEGHTAMOUNT
quantity: QUANTITY
∀i: 1…hwm⦁ vehicleIdentificationNumber ≠ vehicleIdentificationNumber(i)
hwm′ = hwm+1
currentLoadAtDelivery= wieghtAmount*quantity
storingCapacityOfContainer ≥ currentLoad
quantityOfVehicle ≤4
⇒(vehicleIdentificationNumber′= vehicleIdentificationNumber⊕{hwm′ ↦ vehicleIdentificationNumber?})
quantityOfVehicle = 5
⇒(existingVehicle′= existingVehicle +1)
vehicleIdentificationNumber = vehicleIdentificationNumber⊕{queIdentification′ ↦ vehicleIdentificationNum
This schema also describes that two states will be changed after successful completion
of operation. The pickup schema associated with the vehicle. The delivery is done by the
freight company so frieghtCompanyName has been considered as a variable. The abstract
schema states that a new pickup will add a new row. The fore, the pickup schema will check
active delivery vehicles like delivery schema. This operation will input the freight company
name for later tracking of pickup and deliveries.
Operation 4:
addLeaveQueIdentification
Δaddpickup
waitingTime?: ℙ
preferedTime?: ℙ
waitingTime≥ preferedTime
Error: ′The driver left the queIdentification′
This operation will change the state of pickup but in a different way than
acceptPickup schema. Here, the pickup schema describes loss of data. The drivers cannot
always wait as much as system predicts. The driver can chose to leave que if the waiting time

7Z-LANGUAGE
is more than usual or not satisfactory to driver. The system also generates a message after
successful completion of operation.
Operation 5:
unloadShip
ΔTerminal1
wieghtAmount?: X
quantity?: Y
unloadAmount?: UNLOADAMOUNT
unloadAmount = wieghtAmount*quantity
unloadAmount ≥ storingCapacityOfContainer
⇒ Error: ′not available′
unloadAmount ≤ storingCapacityOfContainer
⇒(unloadAmount′)
The ship unload is exactly opposite to delivery schema. The schema also describes the
change of state of terminal. The amount to be unloaded from the ship is presented as
variables named quantity and unloadAmount. The schema describes that unloadAmount
should not be storage capacity of container terminal.
Operation 6:
findTerminal
Ξterminal
name?: NAME
date1: DATE1
date2: DATE2
frieghtCompanyName: FRIEGHTCOMPANYNAME
wieghtAmount: WIEGHTAMOUNT
quantity: QUANTITY
name? ∈ known
date1 ≤ terminal(frieghtCompanyName, wieghtAmount, quantity) ≤ date2
The findTermianl schema describes that no state will be changed by this operation.
The data is found based on the two dates, one is date1 and the other is date2. The freight

8Z-LANGUAGE
company name is stored to see which freight company has delivered how much goods to the
terminal.
Operation 7:
findShipTotalAccount
Ξterminal
name?: NAME
wieghtAmount: WIEGHTAMOUNT
quantity: QUANTITY
name? ∈ known
name! = terminal(quantity, wieghtAmount)
This schema also describes that no state will be changed. The ship account is
determined based on the terminals it has. The system will check the name of the terminal
provided as input. The name of the terminal should be known. The terminals containing
goods quantity and wightAmount is calculated to find ship account.
Operation 8:
findFreightCOmpany
Ξdelivery1
frieghtCompanyName?: FRIEGHTCOMPANYNAME
wieghtAmount: WIEGHTAMOUNT
quantity: QUANTITY
value1! = VALUE1
value2! = VALUE2
frieghtCompanyName? ∈ known
quantity*wieghtAmount ≥ value1
⇒(frieghtCompanyName! = terminal(quantity, wieghtAmount))
quantity*wieghtAmount ≤ value1
Error! = ′Not available′
This schema describes that no state is changed after operation is done. Total amount
of goods delivered by the freight company is calculated using the frieghtCompanyName,
wieghtAmount, quantity input variables.

9Z-LANGUAGE
Conclusion:
The study concludes that the all the operations mentioned are effective enough to
support the operations of container control mechanism. The whole back process can be
automated suing the z-schema based operations. However, various other back processes are
not mentioned in the study.

10Z-LANGUAGE
Bibliography:
Bowen, J. P. (2016). The Z Notation: Whence the Cause and Whither the Course?. In
Engineering Trustworthy Software Systems (pp. 103-151). Springer, Cham.
Brakerski, Z., Gentry, C., & Vaikuntanathan, V. (2014). (Leveled) fully homomorphic
encryption without bootstrapping. ACM Transactions on Computation Theory
(TOCT), 6(3), 13.
Ding, D., Wang, Z., Ho, D. W., & Wei, G. (2017). Distributed recursive filtering for
stochastic systems under uniform quantizations and deception attacks through sensor
networks. Automatica, 78, 231-240.
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).
Wang, L., Cao, Z., de Melo, G., & Liu, Z. (2016). Relation classification via multi-level
attention cnns.
Wen, S., Huang, T., Zeng, Z., Chen, Y., & Li, P. (2015). Circuit design and exponential
stabilization of memristive neural networks. Neural Networks, 63, 48-56.