Formal System Specification using Z-Language

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′