by Wu Chun Pong. / Thesis (M.Phil.)--Chinese University of Hong Kong, 1993. / Includes bibliographical references (leaves 86-[91]). / Chapter 1 --- Introduction --- p.1 / Chapter 1.1 --- Formal Specification Methods --- p.1 / Chapter 1.2 --- The Z notation --- p.2 / Chapter 1.3 --- Overview of Thesis --- p.3 / Chapter 2 --- The Specification Language Z --- p.5 / Chapter 2.1 --- Background --- p.5 / Chapter 2.2 --- Structure and Characteristics --- p.6 / Chapter 2.3 --- Object Orientation in Z --- p.10 / Chapter 2.3.1 --- Hall's style --- p.11 / Chapter 2.3.2 --- Schuman and Pitt's variant --- p.11 / Chapter 2.3.3 --- Object-Z --- p.12 / Chapter 2.4 --- Execution in Z --- p.13 / Chapter 2.5 --- Animation of Z Specifications --- p.15 / Chapter 2.5.1 --- Prolog --- p.15 / Chapter 2.5.2 --- Translation Z into Prolog --- p.18 / Chapter 2.5.3 --- Related Works --- p.19 / Chapter 3 --- Incorporating Real Numbers in Z --- p.22 / Chapter 3.1 --- Dedekind Cut --- p.23 / Chapter 3.2 --- Cantor's definition --- p.23 / Chapter 3.3 --- Practical approach --- p.24 / Chapter 4 --- Constraint Logic Programming and CLP(R) --- p.26 / Chapter 4.1 --- Constraint Logic Programming --- p.26 / Chapter 4.2 --- CLP(R) --- p.27 / Chapter 4.3 --- Example of CLP(R) --- p.29 / Chapter 5 --- The ZCLP(R) Animation System --- p.31 / Chapter 5.1 --- Design Philosophy --- p.31 / Chapter 5.2 --- Implementation Strategy --- p.34 / Chapter 5.3 --- Z editor (ZEDIT) --- p.36 / Chapter 5.4 --- Prolog Library for set operation (ZCLIB) --- p.37 / Chapter 5.4.1 --- Basic needs for the Library --- p.37 / Chapter 5.4.2 --- Rules for the library --- p.38 / Chapter 5.4.3 --- Limitation of the Library --- p.43 / Chapter 5.5 --- Z to CLP(R) Translator (ZCGEN) --- p.44 / Chapter 5.5.1 --- Procedure for translation --- p.45 / Chapter 5.5.2 --- Demonstration --- p.47 / Chapter 5.5.3 --- Rules for translation --- p.48 / Chapter 5.5.4 --- Limitations of the Translator --- p.50 / Chapter 5.6 --- Z to LATEX translator (ZLATEX) --- p.52 / Chapter 6 --- Examples --- p.54 / Chapter 6.1 --- A Simple Banking System --- p.54 / Chapter 6.1.1 --- Bags --- p.54 / Chapter 6.1.2 --- Specifications --- p.56 / Chapter 6.2 --- A Graphics Example --- p.61 / Chapter 6.2.1 --- Defining a Rectangle --- p.62 / Chapter 6.2.2 --- Drawing a Rectangle --- p.63 / Chapter 6.2.3 --- Defining a Circle --- p.63 / Chapter 6.2.4 --- Specifications --- p.64 / Chapter 6.3 --- Specifications Writing Experience --- p.76 / Chapter 7 --- Conclusion --- p.79 / Chapter 7.1 --- Contributions --- p.79 / Chapter 7.2 --- Difficulties --- p.83 / Chapter 7.3 --- Further Works --- p.84 / Bibliography --- p.86

In the development of information systems for business, structured approaches are widely used in practice. Structured approaches provide a prescription and guidelines for how to go about the process of developing an information system, are relatively easy to learn and provide tools which are well suited to their task. However, the products of structured approaches are sometimes seen to be vague and imprecise since requirements are written using natural language or represented in the form of models which do not have a formal foundation. This vagueness or ambiguity can be the source of problems later in development of the information system. A possible solution to this is to represent requirements using formal methods since these are seen as precise and unambiguous. However, formal methods are typically only a mathematical language for representing requirements. They are often regarded as difficult to learn and use. Even though formal methods of one sort or another have been in existence for many years they are not popular and appear unlikely to become popular in the future. One possible approach to providing the advantages of structured approaches and formal methods is to provide translation procedures from the products of structured approaches to a formal description in a suitable formal language. The work in this thesis follows this theme and is aimed at the creation of a translation procedure from an Object Role Model (ORM) schema to a Z specification. An object role model schema is the end product of a process called the Natural Language Information Analysis Method (NIAM) which is used to produce an information model for an information system. NIAM is a method which has been used successfully in industry since the mid 1970s and continues to be used today. This thesis provides a translation procedure from ORM to Z which is less arbitrary and more comprehensive than previous conversion procedures in the literature. It establishes a systematic method for (i) choosing suitable types and variables for a Z specification and (ii) predicates that express all the standard constraints available in ORM modelling. The style of representation in Z preserves ORM�s concepts in a way that aids traceability and validation. The natural language basis of ORM, namely the use of elementary facts, is preserved. Furthermore, an ORM schema differentiates between abstract concepts and the means by which these concepts are represented symbolically and this thesis provides a representation in Z that maintains the distinction between conceptual objects and their symbolic representation. Identification schemes of entity types are also translated into the Z specification but it is left as an option in the translation procedure. Guiding and evaluating the work conducted here are a published set of criteria for the evaluation of a conceptual schema. These have helped in making decisions regarding the translation procedure and for assessing my work and that of others.

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)