ITECH7410 Software Engineering: Formal Z-Language Container System

This report provides a formal specification of a container control system using Z-Language, based on abstract Z schema conventions. It defines the state space as a collection of abstract data type states and details various operations executed within the terminal container control system. Each operation involves input and output variables, with relationships defined to enhance the relevance of Z-Language in software specification. The operations, described by Z-schemas, include addTerminal, acceptDelivery, findCompanyAccount, and more, some of which alter the system's state. The report covers initialization, where variables are declared with their characteristics and data types, and extends operations using data refinement. It thoroughly examines the states of the terminal container control system, utilizing the abstract method and accurately describing all input and output variables for each operation.

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:...................................................................................3
Initialization:..........................................................................................................................3
Operation 1:............................................................................................................................4
Operation 2:............................................................................................................................5
Operation 3:............................................................................................................................6
Operation 4:............................................................................................................................7
Operation 5:............................................................................................................................7
Operation 6:............................................................................................................................8
Operation 7:............................................................................................................................8
Operation 8:............................................................................................................................9
Conclusion:................................................................................................................................9
Bibliography:............................................................................................................................10

2Z-LANGUAGE
Introduction:
The Z schemas used in this article are based on the abstract z schema conventions.
The Z-Notation is the mathematical notation based software specification language that
models the systems. The Z is not a software programming language that can be compiled.
The Z is based on the mathematical notations named first-order predicate logic, lambda
calculus, and axiomatic set theory. The state space, is a collection of abstract data type states,
is a non-empty state.
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.
The proposed non empty space named state space is consists of various operations
that are executed in terminal container control system. Each of the operation is based on the
processing of input variables and resulting in output variables. The relation among the input
variables and output variables in an operation makes the Z more relevant to software
specification language. The whole article is only based on the operations carried out in the
terminal container control system in which the collection of abstract data type has been
defined using the data type name itself. Some of the operations has changed the state and
some does not. The operations that are described by the Z-schema in this article are
addTerminal, acceptDelivery, findCompanyAccount and more.

3Z-LANGUAGE
Z-Schema of Container Control System:
Initialization:
initContainer
id: ℙ containerIdentificationNumber
containerIdentificationNumber: ID ⇸ containerIdentificationNumber
known = domcontainername
initContainer
ΞTERMINAL
Known = ∅
intTerminal
name: ℙ nameOfTerminal
nameOfTerminal: NAME ⇸ NAMEOFTERMINAL
storingCapacityOfContainer: ℕ
known = domterminalnamea
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

4Z-LANGUAGE
The initialization is a very important part of the Z schema description. The variables
to be used in the whole operation are introduced in the initialization process. The
initialization is not an operation. The characteristics, value range, data type of the variables
are stated. The state of the Z-schema is also declared in the initialization phase. As the
abstract state does not get involved from the initialization phase, the change of state names
can be seen later. The terminal name is unique and is used for defining all the values of a
terminal differently. The capacity of the terminal is initialized. If there is no current
information for a specific state then it should be stated during the initialization phase also. All
the operations in the article have been extended using the data refinement.
Operation 1:
addTerminal
Δterminal1
nameOfTerminal?:
NAME
storingCapacityOfContainer?:
STORINGCAPACITYOFCONTAINER
wieghtAmount?:
WIEGHTAMOUNT
quantity?:
QUANTITY
∀i: 1…hwm. nameOfTerminal? ≠ nameOfTerminals(i)
hwm′ = hwm+1
nameOfTerminals′ = nameOfTerminals⊕{hwm′ ↦ nameOfTerminal?}
storingCapacityOfContainers
′ = storingCapacityOfContainers′
{hwm′ ↦
storingCapacityOfContainer?}
asas
as
The addTerminal operation change the state of terminal state. As mentioned at the
time of initialization, the terminal data set is empty. This operation is used for entering the
data in the terminal data set. The data refinement in the terminal state has been obtained by
alternating the state from the abstract state set. The operation enters the name, capacity and
other details into relevant variables for adding a new row in the data set. This implies that the
state change will happen in this Z-schema description. The quantity and wightAmount is the
limit up to which a driver can deliver or unload goods to or from the container. As the

5Z-LANGUAGE
terminal name will act as the unique identifier, the nameOfTerminals(i) has been used. The
serial number of terminals will be natural number therefore, ∀i: 1…hwm. nameOfTerminal?
has been used.
Operation 2:
addDelivery
ΔDelivery1
ΔQue1
vehicleIdentificationNumber: VEHICLEIDENTIFICATIONNUMBER
quantityOfVehicle: QUANTITYOFVEHICLE
currentLoad: CURRENTLOAD
wieghtAmount: WIEGHTAMOUNT
quantity: QUANTITY
queidentification: QUEIDENTIFICATION
∀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′ ↦ vehicleIdentificationNumber?}
Delivery operation is the key operation of terminal container control system. The
delivery projects the idea of normal delivery operations like something will carry some things
to a destination. As every system has unique features, the container control system also has
some conditions and limitations for its own delivery operation. As the operation will add new
data to the delivery and que state, z-schema describes the alteration of state through this
operation. The operation has a que state that plays a very important part in maintain the
delivery operation. If the number of trucks currently delivering goods to a terminal container
is more than 4 then next assignment truck is added to a que until at least a single truck stops
delivering. There will be total two ques for each terminal. The whole delivery process is
recorded based on the vehicle identifier and terminal details. The quantityOfVehicle ≤4 states

6Z-LANGUAGE
that if the delivering vehicle number is four or less than four then only the new truck will be
assigned to delivery, otherwise it will be added to que, existingVehicle′= existingVehicle +1)
vehicleIdentificationNumber = vehicleIdentificationNumber⊕{queIdentification′ ↦
vehicleIdentificationNumber?
Operation 3:
addPickup
Δpickup1
Δdelivery1
vehicleIdentificationNumber: VEHICLEIDENTIFICATIONNUMBER
frieghtCompanyName: FRIEGHTCOMPANYNAME
wieghtAmount: WIEGHTAMOUNT
quantity: QUANTITY
currentCapacity: CURRENTCAPACITY
∀i: 1…hwm⦁ vehicleIdentificationNumber ≠ vehicleIdentificationNumber(i)
hwm′ = hwm+1
currentLoadAtDelivery= wieghtAmount*quantity
currentCapacity ≥ currentLoad
quantityOfVehicle ≤4
⇒(vehicleIdentificationNumber′= vehicleIdentificationNumber⊕{hwm′ ↦ vehicleIdentificationNumber?})
quantityOfVehicle = 5
⇒(existingVehicle′= existingVehicle +1)
vehicleIdentificationNumber = vehicleIdentificationNumber⊕{queIdentification′ ↦ vehicleIdentificationNumber?}
The pickup is the integral process of delivery. The trucks will pickup goods that will
be delivered the terminal mentioned in the delivery operation. Each goods is delivered by a
specific freight company and the state will store that information. The abstract state data type
for this state implies that the pickup state will be changing the state. The pickup operation is
initiated when a vehicle is not in a que. The system will need to store how much load a
vehicle is delivering to the terminal. The current load must be lesser than the current free
storage of the terminal.

7Z-LANGUAGE
Operation 4:
addLeaveQueIdentification
Δque1
waitingTime?: ℙ
preferedTime?: ℙ
waitingTime≥ preferedTime
⇒ (existingVehicle′= existingVehicle -1
vehicleIdentificationNumber = vehicleIdentificationNumber
⊕{queIdentification′
↦ vehicleIdentificationNumber?})
Error: ′The driver left the que′
The drivers are allowed to leave the que if they do not want to want to wait until the
time of delivery. The system store the information of the vehicle which is leaving the que. As
each driver will have his individual truck, the system will only store the vehicle information.
The abstract state data type illustrates that the state of que will change after this operation.
This Z-schema describes that it does not affect delivery operation at all.
Operation 5:
unloadShip
Δdelivery1
ΔTerminal1
wieghtAmount?: X
quantity?: Y
unloadAmount?: UNLOADAMOUNT
unloadAmount = wieghtAmount*quantity
unloadAmount ≥ storingCapacityOfContainer
⇒ Error: ′not available′
unloadAmount ≤ storingCapacityOfContainer
⇒((vehicleIdentificationNumber′= vehicleIdentificationNumber⊕{hwm′ ↦ vehicleIdentificationNumber?})
The abstract state of Ship describes that terminal and delivery both the state will
change after this operation. This operation is also a delivery, but it illustrates delivering goods
from ship terminal container to a specific location. The operation will store the vehicle
information which are assisting in the unload process. The condition in this z-schema is that

8Z-LANGUAGE
the container must have some goods to be delivered. If the container is empty, the system will
generate error report and unload operation will stop.
Operation 6:
findTerminal
Ξterminal
name?: NAME
date1: DATE1
date2: DATE2
frieghtCompanyName: FRIEGHTCOMPANYNAME
wieghtAmount: WIEGHTAMOUNT
quantity: QUANTITY
frieghtCompanyName? ∈ known
date1 ≤ terminal(frieghtCompanyName, wieghtAmount, quantity) ≤ date2
This schema describes no change in the state. The information of delivering goods of
a freight company is found based on two given dates. The condition is that entered freight
company name must be known to the system.
Operation 7:
findShipTotalAccount
Ξterminal
name?: NAME
wieghtAmount: WIEGHTAMOUNT
quantity: QUANTITY
name? ∈ known
name! = terminal(quantity, wieghtAmount)
This abstract state set describes that state of terminal will not change. The state will
find the current load in the terminal if the entered terminal name is known.

9Z-LANGUAGE
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′
The delivery state will not change after this operation. The operation is carried out to
identify goods delivered by the freight company to a specific terminal.
Conclusion:
The article has presented the states of the terminal container control system in a very
particular way. The use of the abstract method has been properly utilized in every possible
state. The operations has described all the input and output variables accurately.

10Z-LANGUAGE
Bibliography:
Asadi, M., Soltani, S., Gašević, D., & Hatala, M. (2016). The effects of visualization and
interaction techniqueIDs on feature model configuration. Empirical Software
Engineering, 21(4), 1706-1743.
Bowen, J. P. (2016). The Z Notation: Whence the Cause and Whither the Course?. In
Engineering Trustworthy Software Systems (pp. 103-151). Springer, Cham.
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).