Formal specification of software systems has been very promising. Critics against the end results of formal methods, that is, producing quality software products, iscertainly rare. Instead, reasons have been formulated to justify why the adoption of the technique in industry remains limited. Some of the reasons are:
- Steap learning curve; formal techniques are said to be hard to use.
- Lack of a step-by-step construction mechanism and poor guidance.
- Difficulty to integrate the technique into the existing software processes.
Z is, arguably, one of the successful formal specification techniques that was extended to Object-Z to accommodate object-orientation. The Z notation is based
on first-order logic and a strongly typed fragment of Zermelo-Fraenkel set theory. Some attempts have been made to couple Z with semi-formal notations such as UML.
However, the case of coupling Object-Z (and also Z) and the Use Case Maps(UCMs) notation is still to be explored. A Use Case Map (UCM) is a
scenario-based visual notation facilitating the requirements definition of
complex systems. A UCM may be generated either from a set of informal requirements, or from use cases normally expressed in natural language. UCMs have the potential
to bring more clarity into the functional description of a system. It may furthermore eliminate possible errors in the user requirements. But UCMs are
not suitable to reason formally about system behaviour. In this dissertation, we aim to demonstrate that a UCM can be transformed into Z and Object-Z, by providing a transformation
framework. Through a case study, the impact of using UCM as an intermediate step in the process of producing a Z and Object-Z specification is explored.
The aim is to improve on the constructivity of Z and Object-Z, provide more guidance, and address the issue of integrating them into the existing Software
Requirements engineering process.
- Please feel free to discuss this article directly on this page. Constructive comments are welcomed! Please sign your TWiki name.
- mscmas.pdf: Masters thesis