Advertisement

Using automated reasoning in the design of an audio-visual communication system

  • José C. Campos
  • Michael D. Harrison
Conference paper
Part of the Eurographics book series (EUROGRAPH)

Abstract

Formal reasoning about how users and systems interact poses a difficult challenge. Interactive systems design provides a context in which the subjective area of human understanding 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 systems. 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 specifications 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 SMV, and in the analysis of the role which different verification techniques might have during the development of interactive systems.

Keywords

Model Check Interactive System Theorem Prover Finite State Machine Automate Reasoning 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Victoria Bellotti, Ann Blandford, David Duke, Allan MacLean, Jon May, and Laurence Nigay. Interpersonal access control in computer-mediated communications: A systematic analysis of the design space. Human-Computer Interaction, 11: 357–432, 1996.Google Scholar
  2. 2.
    Peter Bumbulis. Combining Formal Techniques and Prototyping in User Interface Construction and verification. PhD thesis, University of Waterloo, 1996.Google Scholar
  3. 3.
    José C. Campos. Automated Reasoning and Interactive Systems Development. DPhil thesis, Department of Computer Science, University of York, 1999. in preparation.Google Scholar
  4. 4.
    José C. Campos and Michael D. Harrison. Detecting interface mode complexity with interactor specifications. submitted, 1998.Google Scholar
  5. 5.
    José C. Campos and Michael D. Harrison. The role of verification in interactive systems design. In Markopoulos and Johnson [15], pages 155–170.Google Scholar
  6. 6.
    Bruno d’Ausbourg. Using model checking for the automatic validation of user interfaces systems. In Markopoulos and Johnson [15], pages 242–260.Google Scholar
  7. 7.
    Alan Dix, Janet Finlay, Gregory Abowd, and Russell Beale. Human-Computer Interaction. Prentice-Hall, 1993.Google Scholar
  8. 8.
    G. Doherty, J. C. Campos, and M. D. Harrison. Representational reasoning and verification. In J. I. Siddiqi, editor, Proceedings of the BCS-FACS Workshop: Formal Aspects of the Human Computer Interaction,pages 193–212. SHU Press, 1998. ISBN 0 86339 7948.Google Scholar
  9. 9.
    Gavin Doherty and Michael D. Harrison. A representational approach to the specification of presentations. In Harrison and Tones [14], pages 273–290.Google Scholar
  10. 10.
    David J. Duke and Michael D. Harrison. Abstract interaction objects. Computer Graphics Forum, 12 (3): 25–36, 1993.CrossRefGoogle Scholar
  11. 11.
    Matthew B. Dwyer, Vicki Can, and Laura Hines. Model checking graphical user interfaces using abstractions. In Mehdi Jazayeri and Helmut Schauer, editors, Software Engineering — ESEC/FSE ‘87, number 1301 in Lecture Notes in Computer Science, pages 244–261. Springer, 1997.Google Scholar
  12. 12.
    G. Faconti and F. Paternb. An approach to the formal specification of the components of an interaction. In C. Vandoni and D. Duce, editors, Eurographics ‘80, pages 481–494. North-Holland, 1990.Google Scholar
  13. 13.
    Bob Fields, Nick Merriam, and Andy Dearden. DMVIS: Design, modelling and validation of interactive systems. In Harrison and Tones [14], pages 29–44.Google Scholar
  14. 14.
    M. D. Harrison and J. C. Torres, editors. Design, Specification and Verification of Interactive Systems ‘87, Springer Computer Science. Springer-Verlag/Vien, June 1997.Google Scholar
  15. 15.
    P. Markopoulos and P. Johnson, editors. Design, Specification and Verification of Interactive Systems ‘88, Springer Computer Science. Springer-Verlag/Vien, 1998.Google Scholar
  16. 16.
    K. L. McMillan. The SMV system. Carnegie-Mellon University, draft edition, February 1992.Google Scholar
  17. 17.
    S. Owre, N. Shankar, and J. M. Rushby. User Guide for the PVS Specification and Verification System. Computer Science Laboratory, SRI Internatinal, Menlo Park CA 94025, USA, (beta release) edition, March 1993.Google Scholar
  18. 18.
    Fabio D. Paternb. A Method for Formal Specification and Verification of Interactive Systems. PhD thesis, Department of Computer Science, University of York, 1995.Google Scholar
  19. 19.
    Mark Ryan, José Fiadeiro, and Tom Maibaum. Sharing actions and attributes in modal action logic. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software, volume 526 of Lecture Notes in Computer Science, pages 569–593. Springer-Verlag, 1991.Google Scholar

Copyright information

© Springer-Verlag/Wien 1999

Authors and Affiliations

  • José C. Campos
    • 1
  • Michael D. Harrison
    • 1
  1. 1.Human-Computer Interaction Group Department of Computer ScienceUniversity of YorkCanada

Personalised recommendations