ITECH7410 Software Engineering Methodologies For Z Language

Answer:

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′

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?}

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′)

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