Formal System Specification using Z-Language

This report provides formal system specifications for a container control system using Z language. It includes 8 operations with their Z-schema and bibliography.

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.