Representational Reasoning and Verification
G. J. Doherty, J. Creissac Campos (visit this page for up to date information) & M. D. Harrison
In J. I. Siddiqi, editor(s), Proceedings of the BCS-FACS Workshop: Formal Aspects of the Human ComputerInteraction, SHU Press, pages 193-212. September, 1998.
Formal approaches to the design of interactive systems, such as the principled design approach rely on reasoning about properties of the system at a very high level of abstraction. Such specifications typically provide little scope for reasoning about presentations and the representation of information in the presentation. Theories of distributed cognition place a strong emphasis on the roleof representations in the cognitive process, but it is not clear how such theories can be applied to design.
In this paper we show how a formalisation can be used to encapsulate representational aspects, affording us an opportunity to integrate representational reasoning into the design process. We have shown in  how properties over the abstract state place requirements on the presentation if the properties are to be valid at the perceptual level, and we have presented a model for such properties. We base our approach on this model, and examine in more detail the issue of verification. Given the widespread consensus that proper tool support is a prerequisite for the adoption of formal techniques, we apply a higher-order logic theorem prover to the analysis.