Using automated reasoning in the design of an audio-visual communication system
J. Creissac Campos (visit this page for up to date information) & M. D. Harrison

In D. J. Duke and A. Puerta, editor(s), Design, Specification and Verification of Interactive Systems '99, Springer-Verlag/Wien, pages 167-188. June, 1999.

ISBN: 3-211-83405-2

Formal reasoni ng about how users and systems interact poses a difficult challenge. Interactive systems design provides a context in which the subjective area of human understandin g meets the objectivity of computer systems logic. We present results of a case study in the use of automated reasoning to aid the formal analysis of interactive sys tems. We show how we can use human-factors issues to generate properties of interest, and how we can use model checking and theorem proving to analyse our specificat ions against those properties. This is part of ongoing work in the development of a tool to allow the automatic translation of interactor based specifications into S MV, and in the analysis of the role which different verification techniques might have during the development of interactive systems.