ITECH7410 Software Engineering: Container Control System in Z

This report presents a formal specification of a container control system using Z notation. It includes an introduction to Z-language, detailing its use in specifying software workings and designs, particularly for critical software features. The assignment focuses on eight interconnected operations of a terminal container control system, each with specific conditions transformed into Z schemas. These schemas cover aspects such as initializing variables, adding terminals, managing deliveries and pickups, handling que management, unloading ships, and finding terminal and freight company information. The Z specifications detail state changes and conditions for each operation, concluding with the assertion that Z is a powerful tool for software specification, despite its inability to be directly compiled into executable code. Desklib provides students access to this and other solved assignments.

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

1Z-LANGUAGE
Introduction:
The use of the standardized notation has been increased in the recent past years due to
evolve in the Z-notation. The Z-notation allows the engineers to specify the software
workings and designs in a much better way. The critical and important software features are
easily captured in the z-notation. The models created based on the Z-schema automatically
gets better and accurate.
The whole assignment is based on the eight operations of terminal container control
system. The system operations are interconnected and use various common variables. The
system has various conditions that needs to be followed while transforming those operations
into Z. The Z also describe whether the state changes or ntot.
Z-Schema of Container Control System:
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

2Z-LANGUAGE
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 Z-notation is created based on the mathematical notations. The z only describes
the schema of the software and it does not have any computational feature. The system will
be using variables that needs to be initialized. This section has focused upon initializing the
variables that are to be used in the operations. The variables are input variables and output
variables. The connection between the input and output variables are the key of schema. The
error messages are not initialized as this messages are stated using the inbuilt methods.
In this section, the nature of the variables, like it is natural number, sentence or
something else, is described. The states are not described in this section as the states are not
part of initialization.
Operation 1:

3Z-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 above section of the schema consists of the variables. The variables are described
as input and output. In this operations, all the variables are input variables. The end user will
enter the name of the terminal and its storage capacity. The system will auto generate the
unique number of the schema automatically. The system will store all the terminal data. In
the initialization part, the terminal name is stated as phi to imply that no terminal data is
present currently in the system.
Operation 2:

4Z-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 driver will accept the delivery. The system will not accept the input from the
driver directly but the admin will enter whether the delivery is accepted. If the driver reject
the delivery request, it will bot registered. The system will allow only five vehicles to transfer
load to the container. If five vehicles are transferring load then the system will add the driver
into the que. If not then delivery will be initiated.
Operation 3:

5Z-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
The pickup operation initiates when a delivery is initiated. The driver will load goods
in the truck and deliver it to the container. The pickup operation is for describing the loading
of goods into the vehicles. The state change occur in this Z as the load is added to the
container storage.
Operation 4:
addLeaveQueIdentification
Δaddpickup
waitingTime?: ℙ
preferedTime?: ℙ
waitingTime≥ preferedTime
Error: ′The driver left the queIdentification′
The driver is allowed to leave the que if the waiting time is more than preferred time.
When a driver is added to a que, the system auto generate approximate waiting time. This z
describes change of state.
Operation 5:

6Z-LANGUAGE
unloadShip
ΔTerminal1
wieghtAmount?: X
quantity?: Y
unloadAmount?: UNLOADAMOUNT
unloadAmount = wieghtAmount*quantity
unloadAmount ≥ storingCapacityOfContainer
⇒ Error: ′not available′
unloadAmount ≤ storingCapacityOfContainer
⇒(unloadAmount′)
The ship unload is the opposite operation of delivery. The drivers pickup goods from
the ships ad deliver those to the destination. The operation describe the change of state as the
ship current storage changes.
Operation 6:
findTerminal
Ξterminal
name?: NAME
date1: DATE1
date2: DATE2
frieghtCompanyName: FRIEGHTCOMPANYNAME
wieghtAmount: WIEGHTAMOUNT
quantity: QUANTITY
name? ∈ known
date1 ≤ terminal(frieghtCompanyName, wieghtAmount, quantity) ≤ date2
This Z describes that no state will be changed. The name of the terminal is provided
by the user. The system will find the result based on the inputted name.
Operation 7:

7Z-LANGUAGE
findShipTotalAccount
Ξterminal
name?: NAME
wieghtAmount: WIEGHTAMOUNT
quantity: QUANTITY
name? ∈ known
name! = terminal(quantity, wieghtAmount)
The system will auto generate the total account of ship after the ship details are
entered. This Z describes no change of state as finding the total number and tonnage that a
particular ship has loaded from all container terminals in the total history of the system. The
name means the name of the ship. This value is provided by the user. Based on this input
value, the system will collect and show the data to the user.
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 terminal name is vital for presenting the output as users may not identify the id of
the business. The process suggests the situation that to run the schema, the system must
identify the user input freight company name. If the name is valid, then the system show the
goods brought from a specific freight company to the terminal for two values count1 and
count2.

8Z-LANGUAGE
Conclusion:
The study concludes that Z is a powerful tool for software specification. The software
operations has been effectively presented in the document. The Z schemas cannot be
compiled for getting a proper outcome. This whole thing is conceptual basis. Small
prototypes can be made based on the schema descriptions to justify the Z-notations. The state
change is a important factor of Z tool.

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