ITECH7410 Software Engineering Methodologies Proof Reading Services

ITECH7410 Software Engineering Methodologies Proof Reading Services

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.

Advantages of Z notation

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.

Disadvantages of Z notation

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 container control system schemas

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 x∈Y

∉- 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_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==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

id∉known

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

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.

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