Formal specification of software systems has been very promising. Critics against the end results of formal methods, that is, producing quality software products, is certainly 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. / Computer Science / M. Sc. (Computer Science)

Formal specification of software systems has been very promising. Critics against the end results of formal methods, that is, producing quality software products, is certainly 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. / Computer Science / M. Sc. (Computer Science) / D. Phil. (Computer Science)

The growing need for computer software in different sectors of activity, (health, agriculture, industries, education, aeronautic, science and telecommunication) together with the increasing reliance of the society as a whole on information technology, is placing a heavy and fast growing demand on complex and high quality software systems. In this regard, the anticipation has been on non-functional requirements (NFRs) engineering and formal methods. Despite their common objective, these techniques have in most cases evolved separately. NFRs engineering proceeds firstly, by deriving measures to evaluate the quality of the constructed software (product-oriented approach), and secondarily by improving the engineering process (process-oriented approach). With the ability to combine the analysis of both functional and non-functional requirements, Goal-Oriented Requirements Engineering (GORE) approaches have become de facto leading requirements engineering methods. They propose through refinement/operationalisation, means to satisfy NFRs encoded in softgoals at an early phase of software development. On the other side, formal methods have kept, so far, their promise to eliminate errors in software artefacts to produce high quality software products and are therefore particularly solicited for safety and mission critical systems for which a single error may cause great loss including human life. This thesis introduces the concept of Complementary Non-functional action (CNF-action) to extend the analysis and development of NFRs beyond the traditional goals/softgoals analysis, based on refinement/operationalisation, and to propagate the influence of NFRs to other software construction phases. Mechanisms are also developed to integrate the formal technique Z/Object-Z into the standardised User Requirements Notation (URN) to formalise GRL models describing functional and non-functional requirements, to propagate CNF-actions of the formalised NFRs to UCMs maps, to facilitate URN construction process and the quality of URN models. / School of Computing / D. Phil (Computer Science)