Characterising sound visualisations of specifications using refinement

Abstract

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.