##### HI6006 Competitive Strategy Editing Service

Delivery in day(s): 4

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 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 x∈S, where x is an element which exists in the set S.

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.

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

?- 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 Aand 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*

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

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*

*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*_*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 **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*

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

**Unload_ship schema**

*Unload*-*ship*

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

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.

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 ACM*, *55*(7), 71-77.