Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/13819
Title: XML-based formal specification comprehension
Authors: HUANG XIAONING
Keywords: specification, formal language, Z/Object-Z/TCOZ, UML, statechart, animation
Issue Date: 27-Mar-2004
Source: HUANG XIAONING (2004-03-27). XML-based formal specification comprehension. ScholarBank@NUS Repository.
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.
URI: http://scholarbank.nus.edu.sg/handle/10635/13819
Appears in Collections:Master's Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
thesis.pdf1.21 MBAdobe PDF

OPEN

NoneView/Download

Page view(s)

304
checked on Dec 11, 2017

Download(s)

159
checked on Dec 11, 2017

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.