Thumbnail Image

Characterising sound visualisations of specifications using refinement

Visualisations 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.
Type of thesis
Pilbrow, 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/13288
The University of Waikato
All items in Research Commons are provided for private study and research purposes and are protected by copyright with all rights reserved unless otherwise indicated.