Z-Notation Based Formal Specification for Container Control System

This report provides a detailed explanation of using Z-Notation for specifying a Container Control System. The Z-Notation, a formal specification language, is used to model and describe the software system, leveraging mathematical notations like set theory and predicate logic. The report outlines the Z-Schemas for the Container Control System, covering aspects such as initialization, terminal management, delivery, and pickup operations. Specific operations like adding terminals, deliveries, and pickups are defined using Z-Notation, including preconditions and error handling. The report also includes operations for managing the queue, unloading ships, and finding terminals and freight companies. The conclusion emphasizes the role of Z-schemas in describing processes, conditions, and error statements within the container control system, offering a structured and formal approach to software specification. Desklib provides access to this and other solved assignments to aid students in their studies.

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

1Z-LANGUAGE
Introduction:
The Z-Notation is considered as a formal specification language that are made for
modelling and describing the software systems. Standard mathematical notations like
axiomatic set theory, first-order predicate logic, and lambda calculus are used as the base of
Z-Notation.
The article is based on the Z-Notation description of Container Control System. The
system maintains the process of loading and unloading of goods in the container. Through the
Z-Notation the specifications of the proposed software is described by making Z-Schemas.
Z-Schema of Container Control System:
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

2Z-LANGUAGE
intDeivery
vehicleID: ℕ
numberOfVehcile: ℕ
frieghtCompany: FRIEGHTCOMPANY
currentLoad: ℕ
ton: ℕ
qty: ℕ
numberOfVehcile ≤ 5
storage ≥ ton*qty
currentLoad ≤ storage′
intPickup
vehicleID: ℕ
vehicleID: VEHICLEID ⇸ Delivery
ton: ℕ
qty: ℕ
known = domvehicleid
Operation 1:
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
Operation 2:

3Z-LANGUAGE
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?}
Operation 3:
addPickup
Δpickup1
Δdelivery1
vehicleID: VEHICLEID
frieghtCompany: FRIEGHTCOMPANY
ton: TON
qty: QTY
∀i: 1…hwm⦁ vehicleID ≠ vehicleID(i)
hwm′ = hwm+1
currentLoad = ton*qty
storage ≥ currentLoad
numberOfVehcile ≤4
⇒(vehicleID′= vehicleID⊕{hwm′ ↦ vehicleID?})
numberOfVehcile = 5
⇒(existingVehicle′= existingVehicle +1)
vehicleID = vehicleID⊕{que′ ↦ vehicleID?}
Operation 4:

4Z-LANGUAGE
addLeaveQue
Δaddpickup
waitingTime?: ℙ
preferedTime?: ℙ
waitingTime≥ preferedTime
Error: ′The driver left the que′
Operation 5:
unloadShip
ΔTerminal1
ton?: X
qty?: Y
unloadAmount?: UNLOADAMOUNT
unloadAmount = ton*qty
unloadAmount ≥ storage
⇒ Error: ′not available′
unloadAmount ≤ storage
⇒(unloadAmount′)
Operation 6:
findTerminal
Ξterminal
name?: NAME
date1: DATE1
date2: DATE2
frieghtCompany: FRIEGHTCOMPANY
ton: TON
qty: QTY
name? ∈ known
date1 ≤ terminal(frieghtCompany, ton, qty) ≤ date2
Operation 7:

5Z-LANGUAGE
findShipTotalAccount
Ξterminal
name?: NAME
ton: TON
qty: QTY
name? ∈ known
name! = terminal(qty, ton)
Operation 8:
findFreightCOmpany
Ξdelivery1
frieghtCompany?: FRIEGHTCOMPANY
ton: TON
qty: QTY
value1! = VALUE1
value2! = VALUE2
frieghtCompany? ∈ known
qty*ton ≥ value1
⇒(frieghtCompany! = terminal(qty, ton))
qty*ton ≤ value1
Error! = ′Not available′
Conclusion:
Through the above operations, presented through the z-notation states that container
controls system has several conditions for the whole process. Z-schemas perfectly describes
the processes, conditions and error statements.

6Z-LANGUAGE
Bibliography:
Abad, Z. S. H., Noaeen, M., & Ruhe, G. (2016, September). Requirements engineering
visualization: a systematic literature review. In Requirements Engineering Conference
(RE), 2016 IEEE 24th International (pp. 6-15). IEEE.
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).
Spivey, J. M., & Abrial, J. R. (1992). The Z notation (p. 90). Hemel Hempstead:
Prentice Hall.