Formal Specification in Z for the Container Control System

This study presents various Z-Schema notations for operations of Terminal Container Control System. The initialization of all the global variables are presented in the study. There are total eight operations presented as Z-notation in this study.

Running head: FORMAL SPECIFICATION IN Z
Formal Specification in Z for the Container Control
System
Name of the Student
Name of the University
Author’s note

1FORMAL SPECIFICATION IN Z
Introduction:
Z-is a formal specification notation that describes the systems that are purely
computer based. Zermelo-Fraenkel set theory and first order predicate logic are used by Z-
Language to present the system behaviour and operations. The PRG or programming research
group has developed this schema language.
The study has presented various Z-Schema notations for operations of Terminal
Container Control System. The initialization of all the global variables are presented in the
study. There are total eight operations presented as Z-notation in this study.
Z-Schema Notations:
initContainer
id: ℙ containerID
containerID: ID ⇸ containerID
known = domContainer
initContainer
ΞTERMINAL
Known = ∅
intTerminal
name: ℙ terminalName
terminalName: NAME ⇸ TERMINALNAME
storage: ℕ
storage: ℕ
known = domterminal
intQue
que: ℕ
existingVehicle: ℕ
que≤2

2FORMAL SPECIFICATION IN Z
intDeivery
vehicleID: ℕ
numberOfVehcile: ℕ
frieghtCompany: FRIEGHTCOMPANY
currentLoad: ℕ
ton: ℕ
qty: ℕ
numberOfVehcile ≤ 5
storage ≥ ton*qty
currentLoad ≤ storage′
intPickup
vehicleID: ℕ
vehicleID: VEHICLEID ⇸ Delivery
ton: ℕ
qty: ℕ
known = domvehicleid
Figure 1: Initializing Operation
(Source: Created by Author)
The above Z-notation shows the initialization of the variables. All the variables to be
used in the operations is initialized in the above section. The Known = ∅ means that the
terminal table is empty. There is no data in the terminal entity. The initialization states that
the number of vehicles loading or unloading container terminal must be 5 or less than five.
The number of que is have to be 2. The storage of the container must be greater than the
delivery amount.

3FORMAL SPECIFICATION IN Z
addTerminal
Δterminal1
terminalName?: NAME
storage?:
STORAGE
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)
As there is no terminal data is present, to start the operation a terminal must be
added to the database. The terminal name and storage capacity is stored in the database.
addDelivery
ΔDelivery1
ΔQue1
vehicleID: VEHICLEID
numberOfVehcile: NUMBEROFVEHCILE
currentLoad: CURRENTLOAD
ton: TON
qty: QTY
∀i: 1…hwm⦁ vehicleID ≠ vehicleID(i)
hwm′ = hwm+1
vehicleID = known
currentLoad = ton*qty
numberOfVehcile ≤4
⇒(vehicleID′= vehicleID⊕{hwm′ ↦ vehicleID?})
numberOfVehcile = 5
⇒(existingVehicle′= existingVehicle +1)
vehicleID = vehicleID⊕{que′ ↦ vehicleID?}
Figure 3: Operation 2 - Accept_delivery
(Source: Created by Author)

4FORMAL SPECIFICATION IN Z
The accept delivery means that a new delivery detail will be added to the database.
The current load of the delivery is estimated through the quantity and amount to be delivered.
If the active number of vehicle is 5 then the vehicle is added to the que, otherwise it is
assigned for delivery.
acceptPickup
ΔDelivery1
vehcileIdentifier? : VehicleNumber
companyID? : CompanyID
qty? : Qty
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 })
Figure 4: Operation 3 - Accept_pickup
(Source: Created by Author)
Accept pickup means that a delivery truck will receive goods from c freight company.
The system will store which company is send how much product and the associated driver.

5FORMAL SPECIFICATION IN Z
leaveQue
Δaddpickup
waitingTime?: ℙ
preferedTime?: ℙ
waitingTime≥ preferedTime
Error: ′The driver left the que′
Figure 5: Operation 4 - Leave_delivery_queIDue
(Source: Created by Author)
The driver can chose to leave the que if the waiting time is longer than expected. The
system will reduce the amount of vehicle present in the que by deleting the driver who wants
to leave.
unloadShip
ΔcontainerTerminal1
qty?: X
ton? : Y
error!: Report
qty?* ton? ≥ containerStorage
⇒ error!= no space available
qty?* ton? ≤ containerStorage
⇒(containerStorages′ = containerStorages ⊕ {hwm′ ↦ qty?* ton? })
Figure 6: Operation 5 - Unload_Ship
(Source: Created by Author)
The ship unload is just opposite to accept delivery. The trucks empties the trucks. The
system will show error also if the ship has no container and unload operation is still
persuaded.

6FORMAL 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 system will allow the user to identify the amount of goods delivered by the
system. These delivery amount is determined within dates.
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 system first check the name of the container which is on a ship. Then find out the
total account of that ship by identifying the quantity and amount of products delivered to that
ship’s containers.

7FORMAL 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)
These operation is done to output the total number and tonnage of containers
delivered to and the total number and tonnage picked up from ALL container terminals for
each freight company between two specified global count values.
Conclusion:
The above description of Z-language notations clearly states that proposed notation of
programming language is able to handle the operations perfectly. Z was intended for
individuals, not machines. For a considerable length of time Z was solely a pencil-and-paper
documentation. Z energizes a style where equations are commented on generously with
writing. Z records for the most part incorporate more writing than formal content.
Tenderfoots can be threatened by the presence of Z: a blend of boxes, content, Greek letters,
and designed pictorial images. In any case, the documentation is anything but difficult to
learn; once absorbed, its points of interest turn out to be clear. The cases and pictorial images
in Z enable your eye to get a handle on the structure of the model even before you read it. Z

8FORMAL SPECIFICATION IN Z
really incorporates two documentations. The first is the documentation of common discrete
arithmetic. The second documentation gives structure to the numerical content: it gives a few
organizing builds called passages. The most obvious sort of Z section is a large scale like
shortened form and naming develop called the outline. Z characterizes a pattern math you can
use to manufacture huge outlines from little ones. The pattern is the component that most
recognizes Z from other formal documentations. The proposed Z-Schema notations does not
cover all the necessary operations or many basic level operations of container control system.

9FORMAL SPECIFICATION IN Z
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).