System Requirements

The Z schemas used in this article are based on the abstract z schema conventions. The Z-Notation is the mathematical notation based software specification language that models the systems. The Z is not a software programming language that can be compiled. The Z is based on the mathematical notations named first-order predicate logic, lambda calculus, and axiomatic set theory. The state space, is a collection of abstract data type states, is a non-empty state.

Every operation of container control system consist of input and output variables. There are relationship between input and output variables. In the proposed container control system Z, the abstract data type state set is defined by a schema named as data type itself.

The proposed non empty space named state space is consists of various operations that are executed in terminal container control system. Each of the operation is based on the processing of input variables and resulting in output variables. The relation among the input variables and output variables in an operation makes the Z more relevant to software specification language. The whole article is only based on the operations carried out in the terminal container control system in which the collection of abstract data type has been defined using the data type name itself. Some of the operations has changed the state and some does not. The operations that are described by the Z-schema in this article are addTerminal, acceptDelivery, findCompanyAccount and more.

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

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 initialization is a very important part of the Z schema description. The variables to be used in the whole operation are introduced in the initialization process. The initialization is not an operation. The characteristics, value range, data type of the variables are stated. The state of the Z-schema is also declared in the initialization phase. As the abstract state does not get involved from the initialization phase, the change of state names can be seen later. The terminal name is unique and is used for defining all the values of a terminal differently. The capacity of the terminal is initialized. If there is no current information for a specific state then it should be stated during the initialization phase also. All the operations in the article have been extended using the data refinement.

Learning Outcomes Assessed

addTerminal

Δterminal1

nameOfTerminal?: NAME

storingCapacityOfContainer?: storingCapacityOfContainer

wieghtAmount?: WIEGHTAMOUNT

quantity?: QUANTITY

∀i: 1…hwm. nameOfTerminal? ≠ nameOfTerminals(i)

hwm′ = hwm+1

nameOfTerminals′ = nameOfTerminals⊕{hwm′ ? nameOfTerminal?}

storingCapacityOfContainers′ = storingCapacityOfContainers′{hwm′ ? storingCapacityOfContainer?}

The addTerminal operation change the state of terminal state. As mentioned at the time of initialization, the terminal data set is empty. This operation is used for entering the data in the terminal data set. The data refinement in the terminal state has been obtained by alternating the state from the abstract state set. The operation enters the name, capacity and other details into relevant variables for adding a new row in the data set. This implies that the state change will happen in this Z-schema description. The quantity and wightAmount is the limit up to which a driver can deliver or unload goods to or from the container. As the terminal name will act as the unique identifier, the nameOfTerminals(i) has been used. The serial number of terminals will be natural number therefore, ∀i: 1…hwm. nameOfTerminal? has been used.

addDelivery

ΔDelivery1

ΔQue1

vehicleIdentificationNumber: vehicleIdentificationNumber

quantityOfVehicle: quantityOfVehicle

currentLoad: currentLoad

wieghtAmount: wieghtAmount

quantity: quantity

queidentification: QueIdentification

∀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′ ? vehicleIdentificationNumber?}

Delivery operation is the key operation of terminal container control system. The delivery projects the idea of normal delivery operations like something will carry some things to a destination. As every system has unique features, the container control system also has some conditions and limitations for its own delivery operation. As the operation will add new data to the delivery and que state, z-schema describes the alteration of state through this operation. The operation has a que state that plays a very important part in maintain the delivery operation. If the number of trucks currently delivering goods to a terminal container is more than 4 then next assignment truck is added to a que until at least a single truck stops delivering. There will be total two ques for each terminal. The whole delivery process is recorded based on the vehicle identifier and terminal details. The quantityOfVehicle ≤4 states that if the delivering vehicle number is four or less than four then only the new truck will be assigned to delivery, otherwise it will be added to que, existingVehicle′= existingVehicle +1)    vehicleIdentificationNumber = vehicleIdentificationNumber⊕{queIdentification′ ? vehicleIdentificationNumber?

addPickup

Δpickup1

Δdelivery1

vehicleIdentificationNumber: vehicleIdentificationNumber

frieghtCompanyName: frieghtCompanyName

wieghtAmount: wieghtAmount

quantity: quantity

currentCapacity: CURRENTCAPACITY

Z-Schemas for Container Control System

∀i: 1…hwm? vehicleIdentificationNumber ≠ vehicleIdentificationNumber(i)

hwm′ = hwm+1

currentLoadAtDelivery= wieghtAmount*quantity

currentCapacity ≥ currentLoad

quantityOfVehicle ≤4

⇒(vehicleIdentificationNumber′= vehicleIdentificationNumber⊕{hwm′ ? vehicleIdentificationNumber?})

quantityOfVehicle = 5

⇒(existingVehicle′= existingVehicle +1)

    vehicleIdentificationNumber = vehicleIdentificationNumber⊕{queIdentification′ ? vehicleIdentificationNumber?}

The pickup is the integral process of delivery. The trucks will pickup goods that will be delivered the terminal mentioned in the delivery operation. Each goods is delivered by a specific freight company and the state will store that information. The abstract state data type for this state implies that the pickup state will be changing the state. The pickup operation is initiated when a vehicle is not in a que. The system will need to store how much load a vehicle is delivering to the terminal. The current load must be lesser than the current free storage of the terminal.

addLeaveQueIdentification

Δque1

waitingTime?: ?

preferedTime?: ?

waitingTime≥ preferedTime

⇒ (existingVehicle′= existingVehicle -1

vehicleIdentificationNumber = vehicleIdentificationNumber⊕{queIdentification′ ? vehicleIdentificationNumber?})

Error: ′The driver left the que′

The drivers are allowed to leave the que if they do not want to want to wait until the time of delivery. The system store the information of the vehicle which is leaving the que. As each driver will have his individual truck, the system will only store the vehicle information. The abstract state data type illustrates that the state of que will change after this operation. This Z-schema describes that it does not affect delivery operation at all.

unloadShip

Δdelivery1

ΔTerminal1

wieghtAmount?: X

quantity?: Y

unloadAmount?: unloadAmount

unloadAmount = wieghtAmount*quantity

unloadAmount ≥ storingCapacityOfContainer

⇒ Error: ′not available′

unloadAmount ≤ storingCapacityOfContainer

⇒((vehicleIdentificationNumber′= vehicleIdentificationNumber⊕{hwm′ ? vehicleIdentificationNumber?})

The abstract state of Ship describes that terminal and delivery both the state will change after this operation. This operation is also a delivery, but it illustrates delivering goods from ship terminal container to a specific location. The operation will store the vehicle information which are assisting in the unload process. The condition in this z-schema is that the container must have some goods to be delivered. If the container is empty, the system will generate error report and unload operation will stop.

findTerminal

Ξterminal

name?: NAME

date1: date1

date2: date2

frieghtCompanyName: frieghtCompanyName

wieghtAmount: wieghtAmount

quantity: quantity

frieghtCompanyName? ∈ known

date1 ≤ terminal(frieghtCompanyName, wieghtAmount, quantity) ≤ date2

This schema describes no change in the state. The information of delivering goods of a freight company is found based on two given dates. The condition is that entered freight company name must be known to the system.

findShipTotalAccount

Ξterminal

name?: NAME

wieghtAmount: wieghtAmount

quantity: quantity

name? ∈ known

name! = terminal(quantity, wieghtAmount)

This abstract state set describes that state of terminal will not change. The state will find the current load in the terminal if the entered terminal name is known.

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 delivery state will not change after this operation. The operation is carried out to identify goods delivered by the freight company to a specific terminal.

Conclusion:

The article has presented the states of the terminal container control system in a very particular way. The use of the abstract method has been properly utilized in every possible state. The operations has described all the input and output variables accurately.

Asadi, M., Soltani, S., Gaševi?, D., & Hatala, M. (2016). The effects of visualization and interaction techniqueIDs on feature model configuration. Empirical Software Engineering, 21(4), 1706-1743.

Bowen, J. P. (2016). The Z Notation: Whence the Cause and Whither the Course?. In Engineering Trustworthy Software Systems (pp. 103-151). Springer, Cham.

Iqbal, M. Z., Arcuri, A., & Briand, L. (2015). Environment modeling and simulation for automated testing of soft real-time embedded software. Software & Systems Modeling, 14(1), 483-524.

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