Show simple item record  

dc.contributor.advisorReeves, Steve
dc.contributor.advisorBowen, Judy
dc.contributor.authorPilbrow, Colin
dc.date.accessioned2019-12-10T00:23:23Z
dc.date.available2019-12-10T00:23:23Z
dc.date.issued2019
dc.identifier.citationPilbrow, C. (2019). Characterising sound visualisations of specifications using refinement (Thesis, Doctor of Philosophy (PhD)). The University of Waikato, Hamilton, New Zealand. Retrieved from https://hdl.handle.net/10289/13288en
dc.identifier.urihttps://hdl.handle.net/10289/13288
dc.description.abstractVisualisations can be used to help analyse, explore, and validate Z specifications. However, if visualisations contain errors or are used incorrectly then they can be misleading and harmful. The aim of this work is to characterise the soundness of visualisations of Z specifications. We achieve this by using refinement. We look for a refinement relation between a Z specification and its (claimed sound) visualisation. If the relation does not hold, then the visualisation is not sound. The main type of visualisation we investigate is state diagrams. These diagrams are useful for visualising the state and operations of Z specifications. We look at a variety of state diagrams styles before widening the scope to include μ-Chart visualisations and animated visualisations. We find that existing refinement methods should not be used for all types of visualisations. To characterise the soundness of partial visualisations we extend the standard rules to include unexamined states and restricted specifications. Finally, we include examples of the refinement rules being used on our visualisations. This lets us formally show whether each individual visualisation is sound or not.
dc.format.mimetypeapplication/pdf
dc.language.isoen
dc.publisherThe University of Waikato
dc.rightsAll items in Research Commons are provided for private study and research purposes and are protected by copyright with all rights reserved unless otherwise indicated.
dc.subjectspecification
dc.subjectZ notation
dc.subjectrefinement
dc.subjectstate diagram
dc.subjectvisualisation
dc.titleCharacterising sound visualisations of specifications using refinement
dc.typeThesis
thesis.degree.grantorThe University of Waikato
thesis.degree.levelDoctoral
thesis.degree.nameDoctor of Philosophy (PhD)
dc.date.updated2019-11-25T22:55:35Z
pubs.place-of-publicationHamilton, New Zealanden_NZ


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record