Formal Specification for Container Control System using Z Notation

This document is a formal specification for a container control system using the Z notation. The functionalities of the container control system have been modeled along with schemas for error handling.

Software engineering methodologies
The formal specification for the container control system using the z notation

Software engineering methodologies
Abstract
This document is a formal specification for a container control system. Complex, large or critical
systems require the use of formal specification techniques to ensure flawless functioning through
the elimination or errors and to control the cost of development. For the target system in this
document the mathematical Z notation has been utilized. The Z notation is mathematical in
nature and comprises of the typed first-order predicate logic and the Zermelo-Fraenkel set
theory. The functionalities of the container control system have been modeled along with
schemas for error handling.

Software engineering methodologies
Introduction
Formal specifications are used to develop an abstract view of the system without going into the
details of implementation (Partsch, 2012). This assists in developing a clear logic, in a precise
manner, of how the system will operate. This is achieved through the employment of
mathematical notations borrowed from formal logic and the set theory (Sommerville, 2013).
Consequently, formal specifications reduce the development costs and ambiguity during system
development (Sommerville et al., 2012).
The Z notation
The formal specification technique known as Z notation models the behavior of the proposed
system. It does so by decomposing the system into small units which are known as schemas.
Mathematical notations from the set theory and predicate logic are used to model the schemas
(Klein, Sawicki, Roos-Frantz & Frantz, 2014). These schemas represent static and dynamic
aspects of the proposed system. Static aspects are the possible states the system may be in at any
given time (state space) and relationships between those states.
A typical schema consists of a title, declaration part, where variables are declared, and a
predicate part. The predicate section defines conditions which must be met during operation and
the relationship between variables and functions. The figure below illustrates:
Figure 1: Structure of a schema
SchemaName
Variable declarations
Predicate(s)
The predicate part is optional and is assumed to be true when absent.

Software engineering methodologies
The container control system schemas
The Z notations used for the library system schema include:-
ℙ - Declares a variable x to be a subset of Y. Its syntax is x: ℙY
⇸ - Indicates partial dependence of a variable y on a variable x. The syntax is of the form x⇸y
Δ – It is known as a delta and shows that the current function causes a change in system state,
for example when a new item is added.
Ξ – It is known as Xi and indicates that the current function does not alter system state
∪- Indicates a union between set A and B. Technically, it represents an addition of an element to
a set X in a schema
∈- Indicates that an element x is a member of a set Y. Its syntax is x∈Y
-∉ Indicates that an element x is not a member of a set Y. Its syntax is x∉ Y
? –Is used to indicate input variable x. The syntax is of the form x?:TYPE
! – Is used to indicate output variable x. The syntax is of the form x!:TYPE
Container control system Initial schema
The schema below depicts the initial state of the container control system whereby no data has
been captured yet. In other words, the system is devoid of any data.
Init
Container_control_system
known=∅
Container_Terminal state space

Software engineering methodologies
Container_Terminal
known:ℙNAME
container_capacity:NUMBER
tonnage_capacity:WEIGHT
capacity:container_capacity↦tonnage_capacity
known=dom NAME
The schema above depicts the domain (key identifier), which is ‘NAME’ and ranges, which are
the variables associated with an instance.
Enter_new_container_terminal
Enter_new_container_terminal
Δ Container_control_system
name? : NAME
container_capacity?:NUMBER
tonnage_capacity?:WEIGHT
name? ∉ NAME
NAME′ = NAME∪ {name?↦(container_capacity?,tonnage_capacity?}
The above schema shows that when a new container is added to a terminal the name should not
already exist in the terminal relations set. Only then can the system accept the new instance and
associated tuple.

Software engineering methodologies
Delivery state space
delivery
known:ℙGLOBAL_NO
terminal : NAME
freight_company?SOURCE
quantity:NUMBER
tonnes:WEIGHT
count:INTEGER
vehicle_identifier:IDENTIFICATION
current_deliveries:INTEGER
known= dom GLOBAL_NO
The above schema depicts the deliveries domain and associated ranges. These are the key
identifier (GLOBAL_NO) and the variables associated with an instance.

Software engineering methodologies
Accept_delivery schema
Accept_delivery
ΔContainer_control_system
id?:GLOBAL_NO
terminal? : NAME
freight_company?: SOURCE
quantity?:NUMBER
tonnes?:WEIGHT
count?:INTEGER
truck_registration?:REGISTRATION
current_deliveries?:INTEGER
current_quantity:NUMBER
current_tonnage:WEIGHT
message!:REPORT
id? ∉ known
if current_quantity==container_capacity∨ current_tonnage==tonnage_capacity then
message= capacity_full
if( (quantity+current_quantity)>container_capacity)∨((tonnes+current_tonnage)>tonnage_capacity)
then
message= capacity_exceeded
if current_deliveries ==5 then
message=queue_delivery
else
known′ = known ∪ { id? ↦ terminal?↦freight_company?↦quantity?↦tonnes↦count
↦vehicle_identifier}
Message=success
In the above schema, the delivery instance should not already exist in the system. The system
first checks if the terminal’s capacity is full, in terms of either quantity or tonnage and displays
an error message if the condition is met. It then checks if the terminal’s capacity will be
exceeded, also in terms of either quantity or tonnage when the new delivery is added and
displays an error message if the condition is met. Finally, the system checks if the delivery trucks
currently being processed are five in number and queues the incoming delivery if the condition is
met.

Software engineering methodologies
Pickup state space
pickup
known:ℙGLOBAL_NO
terminal: NAME
truck_registration:REGISTRATION
freight_company?DESTINATION
quantity: NUMBER
tonnes: WEIGHT
count: INTEGER
current_pickups: INTEGER
known=dom GLOBAL_NO
The schema above the domain and ranges of the pickup state space, that is, the key identifier
(GLOBAL_NO) and associated variables respectively.

Software engineering methodologies
Accept pickup schema
Accept_pickup
ΔContainer_control_system
id?:GLOBAL_NO
terminal? : NAME
truck_registration?:REGISTRATION
freight_company?: SOURCE
quantity?:NUMBER
tonnes?:WEIGHT
count?:INTEGER
current_pickups?:INTEGER
message!:REPORT
id∉known
if current_pickups ==5 then
message=queue_pickup
else
known′=known∪{ id?↦( terminal?, truck_registration?,freight_company?,quantity?, tonnes?,count?)}
Message=success
The above schema shows that when pickups currently ongoing involves five trucks, then the
pending pickup is queued by the system. Otherwise, the new pick up is captured and stored and a
success message displayed.
Ships state space
ships
known:ℙNAME
nationality: SOURCE
containers: INTEGER
tonnage: WEIGHT
known=dom NAME
The above schema depicts the ships state space with its domain (key identifier) and ranges
(variables).

Software engineering methodologies
Unload_ship schema
Unload-ship
ΔContainer_control_system
name:NAME
terminal:NAME
quantity:INTEGER
tonnage:WEIGHT
container_capacity:INTEGER
tonnage_capacity:WEIGHT
message!:REPORT
if deliveries_ not_ finished ∧ pickups _not_ finished then
message=deliveries_and_pick_ups_not_finished
if (quantity>container_capacity) ∨ (tonnage>tonnage_capacity) then
message= capacity_exceeded
The above schema shows that when all deliveries and pickups are not finished, no unloading
should take place. Furthermore, if the containers’ quantity or tonnage exceeds the terminal's
capacity the system displays an error message.
Container_terminal_account schema
Container_terminal_account
ΞContainer_control_system
total_quantity:INTEGER
total_tonnage:WEIGHT
count!:INTEGER
report!: total_quantity↦ total_tonnage
count! (i…n): CONTAINER|report!

Software engineering methodologies
Ships-total-account
ΞContainer_control_system
total_quantity:INTEGER
total_tonnage:WEIGHT
count!:INTEGER
report!: total_quantity↦ total_tonnage
count! (i…n): CONTAINER|report!
Freight-company-account
ΞContainer_control_system
total_quantity:INTEGER
total_tonnage:WEIGHT
count!:INTEGER
report!: total_quantity↦ total_tonnage
count! (i…n): CONTAINER|report!
Error handling schemas
REPORT ::=capacity_full|capacity_exceeded|queue_delivery|success|queue_pickup|
deliveries_and_pick_ups_not_finished|incorrect_registration
capacity_full
result!:REPORT
result!=capacity_full
capacity_exceeded
result!:REPORT
result!= capacity_exceeded

Software engineering methodologies
queue_delivery
result!:REPORT
result!:queue_delivery
success
result!:REPORT
result!:success
queue_pickup
result!:REPORT
result!:queue_pickup
deliverie_pickups_not_finished
result!:REPORT
result!: deliverie_pickups_not_finished
incorrect_registration
result!:REPORT
result!:incorrect_registration
Conclusion
From research findings formal specification techniques are extremely useful when it comes to
engineering of large, complex systems. They are extremely useful tools in the software and
industrial engineering disciplines. Research and improvements are ongoing as they continue to
be more defined and developed.

Software engineering methodologies
References
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).
Partsch, H. A. (2012). Specification and transformation of programs: a formal approach to
software development. Springer Science & Business Media.
Sannella, D., & Tarlecki, A. (2012). Foundations of algebraic specification and formal software
development. Springer Science & Business Media.
Singh, M., Sharma, A. K., & Saxena, R. (2016). Formal Transformation of UML Diagram: Use
Case, Class, Sequence Diagram with Z Notation for Representing the Static and
Dynamic Perspectives of System. In Proceedings of International Conference on
ICT for Sustainable Development(pp. 25-38). Springer, Singapore.
Smith, G. (2012). The Object-Z specification language (Vol. 1). Springer Science & Business
Media.
Smith, G. (2012). The Object-Z specification language (Vol. 1). Springer Science & Business
Media.
Sommerville, I. (2013). Software Engineering: Pearson New International Edition. Pearson
Education Limited.
Sommerville, I., Cliff, D., Calinescu, R., Keen, J., Kelly, T., Kwiatkowska, M., ... & Paige, R.
(2012). Large-scale complex IT systems. Communications of the ACM, 55(7), 71-
77.
Woodcock, J. (2014). Software engineering mathematics. CRC Press.