ITECH7410 Software Engineering Methodologies Proof Reading Services

ITECH7410 Software Engineering Methodologies Proof Reading Services

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 behaviour 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 the 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) andEffective Workplace 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.

The container control system schemas:-

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

1.?- Declares a variablexto be a subset ofY.Its syntax isx:?Y

2.?- Indicates partial dependence of a variableyon a variablex.The syntax is of the formx?y

3.Δ–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.

4.Ξ– It is known as Xi and indicates that the current function does not alter system state

5.∪-Indicates a union between set A and B. Technically, it represents an addition of an element to a set X in a schema

6.∈- Indicates that an elementxis a member of a setY. Its syntax isx∈Y

7.∉-Indicates that an elementxis not a member of a setY. Its syntax isx∉Y

8.? –Is used to indicate input variablex. The syntax is of the formx?: TYPE

9.! – Is used to indicate output variablex. The syntax is of the formx!: 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 beingprocessed 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

Δ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!

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

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

 References:-

1.Klein, M. J., Sawicki, S., Roos-Frantz, F., & Frantz, R. Z. (2014, April). On the Formalisation of
2.an Application Integration Language Using Z Notation. In ICEIS (1) (pp. 314-319).
3.Partsch, H. A. (2012). Specification and transformation of programs: a formal approach to software testing. Springer Science & Business Media.
4.Sannella, D., & Tarlecki, A. (2012). Foundations of algebraic specification and formal software
5.development. Springer Science & Business Media.
6.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.
7.Smith, G. (2012). The Object-Z specification language (Vol. 1). Springer Science & Business Media.
8.Smith, G. (2012). The Object-Z specification language (Vol. 1). Springer Science & BusinessMedia.
9.Sommerville, I. (2013). Software Engineering: Pearson New International Edition. PearsonEducation Limited.
10.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.
11.Woodcock, J. (2014). Software engineering mathematics. CRC Press.