# ITECH7410 Software Engineering Methodologies Proof Reading Services

## Introduction

Formal specifications are used to describe systems in a clear and precise manner using mathematical notations borrowed from formal logic and the set theory (Somerville, 2013). They provide an abstraction of the system from a high level point of view (Partsch, 2012). This means that the users and developers know what the system is going to do before they go into the specific details of how that will be achieved. The specification acts as a kind of central repository because business analysis developers, testers and users all refer to it at one point or another in the system’s lifecycle.

In general, formal specifications reduce the overall cost of system development and reduces ambiguity and therefore errors as the system keeps getting developed (Sommerville et al., 2012).

### The Z notation

The Z notation is a formal specification method which models the behavior of the proposed system in decomposed, small units known as schemas. Schemas are depicted using mathematical notations from the set theory and predicate logic (Klein, Sawicki, Roos-Frantz & Frantz, 2014).

Schemas represent the dynamic and static aspects of the system. The dynamic aspects include the operations that can be carried out, relationships between inputs and outputs and changes of state. The static aspects include the possible states the system can be in (state space) and the relationships between them.

The structure of a schema consists of the title of the schema, the declaration part, where variables are declared, and the predicate section, where conditions and relationship between variables and functions are specified. The figure below illustrates.

Figure 1: Structure of a schema

SchemaName

Variable declarations

Predicate(s)

The predicate part can be optional and is assumed to be true when absent.

Variables are declared in the form x:T, where x is the variable and T is the data type. Predicates use mathematical symbols from the set theory and logic to represent an expression. Z notation particularly employs the Zermelo-Fraenkel set theory and the typed first order predicate logic for these expressions. An example of a predicate could be xS, where x is an element which exists in the set S.

### 1. It produces human readable system specification and therefore can be used as a basis for documentation

2. The Z notation makes a large specification manageable by decomposing it using schemas into small units

3. Z notation has been widely accepted as the industry standard for formal specification and can be comfortably used in whichever context, be it software engineering or the manufacturing industry.

### As a formal specification technique, it requires a considerable amount of effort and experience to use it in a practical and beneficial way

The Z toolset is still not very advanced. Typechecking and proof reading tools are still being developed and have not really been standardized.

### The Z notations used for the library system schema include:-

?- Declares a variablex to be a subset of Y. Its syntax is x:?Y

?- Indicates partial dependence of a variabley 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 Aand B. Technically, it represents an addition of an element to a set X in a schema

- Indicates that an elementx is a member of a set Y. Its syntax is xY

- Indicates that an elementx is not a member of a set Y. Its syntax is x Y

?-Indicates a difference between two sets A and B, with A being the larger set which contains all the elements present in set B. The syntax is A?B

? –Is used to indicate input variable x. Syntax is of the form x?:TYPE

! – Is used to indicate output variable x. 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

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.

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.

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_capacitycurrent_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==5then

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

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.

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

idknown

if current_pickups==5then

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

name:NAME

terminal:NAME

quantity:INTEGER

tonnage:WEIGHT

container_capacity:INTEGER

tonnage_capacity:WEIGHT

message!:REPORT

if deliveries_not_finishedpickups_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 exceed 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!

Ships-total-account

Freight-company-account

Current trends in Z formal method

Object Z is a new object oriented formal specification technique based on the earlier developed Z notation. It is therefore, in essence, an extension of Z (Smith, 2012). The view of the system is that of objects communicating with one another. It is necessary, therefore, that all the object oriented principles are followed including encapsulation, polymorphism, inheritance and persistence.

Singh, Sharma, and Saxena (2016) have proposed a new approach of integrating UML and Z notation. This comes about as a result ofrigorous use of mathematics in formal methods. Therefore, they suggested that a bridge is required between UML and formal methods to overcome the insufficiencies. Research and development continues.

#### Conclusion

Formal specification techniques have been seen to be useful in large scale system development as they reduce ambiguity and therefore errors in the final deliverable. This makes them invaluable tools both in the software and industrial engineering fields. As can be seen in the previous sections, these techniques keep being improved through research and development.

#### References

1. Klein, M. J., Sawicki, S., Roos-Frantz, F., & Frantz, R. Z. (2014). On the Formalisation of an Application Integration Language Using Z Notation. In ICEIS (1) (pp. 314-319).
2. Partsch, H. A. (2012). Specification and transformation of programs: a formal approach to software development. Springer Science & Business Media.
3. Singh, M., Sharma, A. K., & Saxena, R. (2016). Formal Transformation of UML Diagram: UseCase, 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.
4. 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.
5. Sommerville, I., Cliff, D., Calinescu, R., Keen, J., Kelly, T., Kwiatkowska, M., ... & Paige, R. (2012). Large-scale complex IT systems. Communications of the ACM55(7), 71-77.