Improvements in the Requirements Specification Using Z Language and Its Successor

Abstract

Z (pronounced Zed!) is a Formal Specification language that works at a high level of abstraction so that even complex behaviors can be described precisely and concisely, which is also used to specify the functional requirement of the system. A functional specification is a formal document used to describe in details for software developers a product's intended capabilities, appearance, and interactions with users. The Z notation is a strongly typed, mathematical, specification language. It is not an executable notation; it cannot be interpreted or compiled into a running program. The Z notation is a model-based specification language based on set theory and first-order predicate logic. It provides rich data structures and facilities to define operations on them. An abstract Z specification of an Automated Teller Machine (ATM) environment is defined in this thesis. This specification is used to represent the state of the world and the operations defined on it. The Z schemas are written by using Z/Word tool, supports all types of notations which are used in Z language. Then, attempt to ensure that some constraints on this system are not violated. For this, converted the Z specification into an Alloy model that can be put into the Alloy Analyzer for fully automatic analysis. Alloy is a formal language deeply rooted in Z. Alloy's writing mechanisms are designed to have the flexibility of Z's schema calculus, but are based on different idioms. Combining Z specification to C++ code to provide a prototyping facility by integrating the execution of code into the interpretation of a specification. That is, it is not aimed as a code generation system, but kind of a tool for analyzing specification (including syntax, semantic and type checking) and for helping a software developer in obtaining code from specification.