ITECH7410 - Software Engineering: Formal System Spec with Z

This report presents a formal system specification for a container control system using Z-Language. It includes eight operations: Enter_new_container_terminal, Accept_delivery, Accept_pickup, Leave_delivery_queue, Unload_ship, Container_terminal_account, Ships_total_account, and Freight_company_account. Each operation is defined using Z-schema, specifying preconditions and effects on the system state. The specifications cover initialization operations for container handles, terminals, delivery queues, and pickups, ensuring constraints such as storage capacity and vehicle limits are met. Error conditions are also specified to handle cases like unavailable ships or full delivery queues. This formal approach aims to provide a rigorous and unambiguous description of the system's behavior, facilitating verification and validation.

Running head: FORMAL SYSTEM SPECIFICATION USING Z-LANGUAGE
Formal System Specification using Z-Language
Name of the Student
Name of the University
Author’s Note:

1FORMAL SYSTEM SPECIFICATION USING Z-LANGUAGE
Table of Contents
Initialization operations:.................................................................................................1
Operation 1: Enter_new_container_terminal.................................................................2
Operation 2: Accept_delivery........................................................................................2
Operation 3: Accept_pickup..........................................................................................3
Operation 4: Leave_delivery_queue..............................................................................3
Operation 5: Unload_ship..............................................................................................4
Operation 6: Container_terminal_account.....................................................................4
Operation 7: Ships_total_account..................................................................................4
Operation 8: Freight_company_account........................................................................5
Bibliography:..................................................................................................................6

2FORMAL SYSTEM SPECIFICATION USING Z-LANGUAGE
In this report, total 8 operations of a container control system has been designed
through the use of Z language. The formal specifications for each of the operations have been
provided in the Z-schema as given in the section below:
Initialization operations:
initContainerhandle
id: ℙ containerid
containerid: ID ⇸ containerid
known = domContainer
initContainerterminal
Ξterminal
known = ∅
initTerminal
name: ℙ terminalName
terminalName: NAME ⇸ TERMINALNAME
storage: ℕ
storage: ℕ
known = domterminal
initQue
que: ℕ
existingVehicle: ℕ
que≤2
initDeivery
vehicleID: ℕ
numberOfVehcile: ℕ
frieghtCompany: FRIEGHTCOMPANY
currentLoad: ℕ
ton: ℕ
qty: ℕ
number_Of_Vehcile ≤ 5
storage ≥ ton*qty
currentLoad ≤ storage′

3FORMAL SYSTEM SPECIFICATION USING Z-LANGUAGE
initPickup
vehicleID: ℕ
vehicleID: VEHICLEID ⇸ Delivery
ton: ℕ
qty: ℕ
known = domvehicleid
Operation 1: Enter_new_container_terminal
Enter_new_container_terminal
Δ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: Accept_delivery
Accept_delivery
Δ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?}

4FORMAL SYSTEM SPECIFICATION USING Z-LANGUAGE
Operation 3: Accept_pickup
Accept_pickup
Δ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: Leave_delivery_queue
Leave_delivery_queue
Δaddpickup
waitingTime?: ℙ
preferedTime?: ℙ
waitingTime≥ preferedTime
Error: ′No trucks are there in the que′
Operation 5: Unload_ship
Unload_ship
ΔTerminal1
ton?: X
qty?: Y
unloadAmount?: UNLOADAMOUNT
unloadAmount = ton*qty
unloadAmount ≥ storage
⇒ Error: ′There are no ships available′
unloadAmount ≤ storage
⇒(unloadAmount′)

5FORMAL SYSTEM SPECIFICATION USING Z-LANGUAGE
Operation 6: Container_terminal_account
Container_terminal_account
Ξterminal
name?: NAME
date1: DATE1
date2: DATE2
frieghtCompany: FRIEGHTCOMPANY
ton: TON
qty: QTY
name? ∈ known
date1 ≤ terminal(frieghtCompany, ton, qty) ≤ date2
Operation 7: Ships_total_account
Ships_total_account
Ξterminal
name?: NAME
ton: TON
qty: QTY
name? ∈ known
name! = terminal(qty, ton)
Operation 8: Freight_company_account
Freight_company_account
Ξ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′

6FORMAL SYSTEM SPECIFICATION USING Z-LANGUAGE
Bibliography:
Basu, S., Sengupta, A., & Mazumdar, C. (2016). Modelling operations and security of cloud
systems using Z-notation and Chinese Wall security policy. Enterprise Information
Systems, 10(9), 1024-1046.
Grant, E. S., & Brown, T. (2016). Towards Rigorous Transformation Rules for Converting
UML Operation Signatures to Z Schema. In Proceedings of the International
MultiConference of Engineers and Computer Scientists (Vol. 1).
Woodcock, J. (2014). Software engineering mathematics. CRC Press.