Formal Specification in Z for the Container Control System

Running head: FORMAL SPECIFICATION IN Z
Formal Specification in Z for the Container Control
System
Name of the Student
Name of the University
Author’s note

1FORMAL SPECIFICATION IN Z
Introduction:
Z-is a formal specification notation that describes the systems that are purely
computer based. Zermelo-Fraenkel set theory and first order predicate logic are used by Z-
Language to present the system behaviour and operations. The PRG or programming research
group has developed this schema language.
The study has presented various Z-Schema notations for operations of Terminal
Container Control System. The initialization of all the global variables are presented in the
study. There are total eight operations presented as Z-notation in this study.
Z-Schema Notations:
initContainer
id: ℙ containerID
containerID: ID ⇸ containerID
known = domContainer
initContainer
ΞTERMINAL
Known = ∅
intTerminal
name: ℙ terminalName
terminalName: NAME ⇸ TERMINALNAME
storage: ℕ
storage: ℕ
known = domterminal
intQue
que: ℕ
existingVehicle: ℕ
que≤2

2FORMAL SPECIFICATION IN Z
intDeivery
vehicleID: ℕ
numberOfVehcile: ℕ
frieghtCompany: FRIEGHTCOMPANY
currentLoad: ℕ
ton: ℕ
qty: ℕ
numberOfVehcile ≤ 5
storage ≥ ton*qty
currentLoad ≤ storage′
intPickup
vehicleID: ℕ
vehicleID: VEHICLEID ⇸ Delivery
ton: ℕ
qty: ℕ
known = domvehicleid
Figure 1: Initializing Operation
(Source: Created by Author)
The above Z-notation shows the initialization of the variables. All the variables to be
used in the operations is initialized in the above section. The Known = ∅ means that the
terminal table is empty. There is no data in the terminal entity. The initialization states that
the number of vehicles loading or unloading container terminal must be 5 or less than five.
The number of que is have to be 2. The storage of the container must be greater than the
delivery amount.