Delivery in day(s): 5
ITECH7410 Software Engineering Methodologies Oz Assignments
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) and Effective 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
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 variable x to be a subset of Y. Its syntax is x: ?Y
2.? - Indicates partial dependence of a variable y on a variable x. The syntax is of the form x?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 element x is a member of a set Y. Its syntax is x∈Y
7.∉ - Indicates that an element x is not a member of a set Y. Its syntax is x∉ Y
8.? –Is used to indicate input variable x. The syntax is of the form x?: TYPE
9.! – 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.
Container_Terminal state space:-
The schema above depicts the domain (key identifier), which is ‘NAME’ and ranges, which are the variables associated with an instance.
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:-
The above schema depicts the deliveries domain and associated ranges. These are the key identifier (GLOBAL_NO) and the variables associated with an instance.
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
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:-
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:-
The above schema depicts the ships state space with its domain (key identifier) and ranges (variables).
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.
Error handling schemas:-
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.
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 & Business Media.
9.Sommerville, I. (2013). Software Engineering: Pearson New International Edition. Pearson Education 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.