An editor and transformation system for a Z animation case tool.

In order to remain competitive, modem systems developers are increasingly under pressure to produce software solutions to complex problems faster and cheaper, whilst at the same time maintaining a high level of quality in the delivered product. One of the key quality measures is the delivery of a system that meets the customer's requirements. Failure to meet the customer's requirements may engender significant re-design, which in turn will cost money, delay product introduction and may seriously damage the developer's credibility. For these reasons, the problem of developing a precise and unambiguous statement of requirements for a proposed system is perhaps one of the most challenging problems within software engineering today. Formal, model-based specification languages such as the Z notation have been widely adopted within the context of requirements engineering, to provide a vehicle for the development of precise and unambiguous specifications. However, the mathematical foundation upon which these notations are based often makes them unapproachable and difficult to assimilate by a non-specialist reader. The problem then faced is that if the customer cannot understand the semantics of the specification, how can the customer agree that the specification is indeed a true reflection of the requirements for the desired system? Several researchers have proposed that rapid prototyping and animation of specifications can be used to increase the customer's understanding of the formal specification. This is achieved by executing specification components on candidate data and observing that the behaviour is as expected. However this requires that the original formal specification be reliably transformed into a representation capable of being executed within a computer system. To achieve this aim requires the support of computer-based tools able to assist the requirements engineer in capturing, manipulating and transforming the formal specification in an efficient and consistent manner. This thesis describes the research and development of the TranZit tool, which is a Z notation editor, checker and transformation system. TranZit supports the efficient capture and maintenance of Z notation specifications using the Windows Graphical User Interface, supported by a suite of powerful language-driven features. In addition TranZit contains a highly integrated and optimised syntax and type checker, combining traditional compiler design techniques with innovative use of object-oriented data structures and methods, to assist the requirements engineer in ensuring the internal consistency of the captured specification. Most importantly, TranZit contains a novel transformation engine, which is capable of transforming a captured Z specification into an executable representation based on extensions to LISP, suitable for direct execution in an animation environment. This process is supported by an eclectic strategy combining automated transformation with user assistance, to overcome many of the well-documented problems associated with transforming non-executable clauses in formal specifications.