XML-based formal specification comprehension

Abstract

Specification comprehension is an analytical process of a specification model. During this process the specification model can be improved. In this thesis, our concept of specification comprehension comes from the idea of program understanding, aiming at utilizing some techniques to display the static and dynamic properties of a specification. In this thesis, we propose a framework of specification comprehension for Z-family languages (Z/Object-Z/TCOZ), particularly TCOZ. The environment of Z-family we exploit is ZML. Three techniques helping the comprehension of a Z family specification are introduced: query, visualization and animation. The query of a Z-family specification is similar to the query of a program. Through the process of query, we attempt to display some static properties of the specification, such as properties about a class, an operation, or a cross-reference between classes.The visualization of a Z-family specification is achieved by UML projection. This projection transfers the textual specification into UML diagrams, e.g. statecharts, which illustrate the relationship between the classes of this specification. The animation of a Z-family specification aims at displaying the dynamic properties of the specification. It utilizes the transformation from Z-family language to Java language to achieve an animated mapping of the original Z-family document. Then through this animated document, some dynamic properties of the original one can be illustrated easily and directly. A case tool is implemented in this thesis. This case tool provides an environment to display and edit the Z-family specification, implements the query and animation functions and also links the visualization function as a module of it. This tool also supports schema checking and simple logic and semantic checking.