Characterising Sound Visualisations of Specifications using Micro-charts and Refinement
Authors
Loading...
Permanent Link
Publisher link
Rights
This is the author's accepted version of an article published in the Proceedings of the 24th Asia-Pacific Software Engineering Conference. © 2017 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.
Abstract
For validation or for communication with a client, it is useful to create a visualisation of a specification. It is important that the visualisation does not mislead the user. In this work we look at how to characterise the conditions for a micro-chart visualisation to be sound. This is done by introducing a new operator to the micro-chart semantics, allowing us to use Z data refinement to find a refinement relation between a Z specification and its (claimed sound) micro-chart visualisation. If the relation does not hold, then the visualisation is not sound.
Citation
Pilbrow, C., & Reeves, S. (2017). Characterising Sound Visualisations of Specifications using Micro-charts and Refinement. In J. Lv, H. (Jason) Zhang, M. Hinchey, & X. Liu (Eds.), Proceedings of the 24th Asia-Pacific Software Engineering Conference (pp. 612–617). Washington, DC, USA: IEEE. https://doi.org/10.1109/APSEC.2017.74
Series name
Date
Publisher
IEEE