Advertisement

The role of verification in interactive systems design

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

Abstract

In this paper we argue that using verification in interactive systems development is more than just checking whether the specification of the system has all the required properties; and that changing the focus from a global specification into partial, property oriented, specifications can provide a number of advantages and make verification act as an aid to decision making. We also present a compiler that allows for the verification of interactor specifications to be done in SMV, as well as a simple case study where verification is used to inform a design decision.

Keywords

Model Check Interactive System Finite State Machine Interactor Notation Simple Case Study 
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.
    Gregory D. Abowd, Hung-Ming Wang, and Andrew F. Monk. A formal technique for automated dialogue development. In Proceedings of the First Symposium of Designing Interactive Systems — DIS’95, pages 219–226. ACM Press, August 1995.Google Scholar
  2. 2.
    F. Bodart and J. Vanderdonckt, editors. Design, Specification and Verification of Interactive Systems ’96, Springer Computer Science. Springer-Verlag/Vien, June 1996.MATHGoogle Scholar
  3. 3.
    Peter Bumbulis, P. S. C. Alencar, D. D. Cowan, and C. J. P. Lucena. Validating properties of component-based graphical user interfaces. In Bodart and Vanderdonckt Design, Specification and Verification of Interactive Systems ’96, Springer Computer Science. Springer-Verlag/Vien, June 1996, pages 347–365.Google Scholar
  4. 4.
    José C. Campos and Michael D. Harrison. Formal verification of interactive systems: A review. In Harrison and Torres Design, Specification and Verification of Interactive Systems ’97, Springer Computer Science. Springer-Verlag/Vien, June 1997, pages 109–124.Google Scholar
  5. 5.
    E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, April 1986.MATHCrossRefGoogle Scholar
  6. 6.
    Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas. A tutorial introduction to PVS. Presented at WIFT’95: Workshop on Industrial-Strength Formal Specification Techniques, April 1995. http://www.csl.sri.com/sri-csl-fm.html/sri-csl-fm.html.Google Scholar
  7. 7.
    Bruno d’Ausbourg, Guy Durrieu, and Pierre Roche. Deriving a formal model of an interactive system from its UIL description in order to verify and to test its behaviour. In Bodart and Vanderdonckt Design, Specification and Verification of Interactive Systems ’97, Springer Computer Science. Springer-Verlag/Vien, June 1997, pages 105–122.Google Scholar
  8. 8.
    A. M. Dearden and M. D. Harrison. Risk analysis, impact and interaction modelling. In Bodart and Vanderdonckt Design, Specification and Verification of Interactive Systems ’97, Springer Computer Science. Springer-Verlag/Vien, June 1997, pages 229–247.Google Scholar
  9. 9.
    David J. Duke and Michael D. Harrison. Abstract interaction objects. Computer Graphics Forum, 12(3):25–36, 1993.Google Scholar
  10. 10.
    D.J. Duke, P.J. Barnard, J. May, and D.A. Duce. Systematic development of the human interface. In Asia Pacific Software Engineering Conference, pages 313–321. IEEE Computer Society Press, December 1995.Google Scholar
  11. 11.
    Bob Fields, Michael D. Harrison, and Peter Wright. THEA: Human error analysis for requirements definition. Technical Report YCS 249, Department of Computer Science, University of York, Heslington, York, YOl 5DD, England, 1997.Google Scholar
  12. 12.
    Bob Fields, Nick Merriam, and Andy Dearden. DMVIS: Design, modelling and validation of interactive systems. In Harrison and Torres Design, Specification and Verification of Interactive Systems ’97, Springer Computer Science. Springer-Verlag/Vien, June 1997, pages 29–44.Google Scholar
  13. 13.
    John V. Guttag, James J. Horning, et al. Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer-Verlag, 1993.MATHCrossRefGoogle Scholar
  14. 14.
    M. Harrison, R. Fields, and P. C. Wright. The user context and formal specification in interactive system design (invited paper). In C. R. Roast and J. I. Siddiqi, editors, BCS-FACS Workshop on Formal Aspects of the Human Computer Interface, electronic Workshops in Computing. Springer, September 1996. http://www.springer.co.uk/ewic/workshops/FAHCI/.Google Scholar
  15. 15.
    M. D. Harrison and J. C. Torres, editors. Design, Specification and Verification of Interactive Systems ’97, Springer Computer Science. Springer-Verlag/Vien, June 1997.MATHGoogle Scholar
  16. 16.
    C. B. Jones. The search for tractable ways of reasoning about programs. Technical Report UMCS-92–4–4, Department of Computer Science, University of Manchester, June 1992.Google Scholar
  17. 17.
    K. L. McMillan. The SMV system. Carnegie-Mellon University, draft edition, February 1992.Google Scholar
  18. 18.
    M. Mezzanotte and F. Paternó. Verification of properties of human-computer dialogues with an infinite number of states. In C. R. Roast and J. I. Siddiqi, editors, BCS-FACS Workshop on Formal Aspects of the Human Computer Interface, electronic Workshops in Computing. Springer, September 1996. http://www.springer.co.uk/ewic/workshops/FAHCI/.Google Scholar
  19. 19.
    Andrew F. Monk and Martin B. Curry. Discount dialogue modelling with Action Simulator. In G. Cockton, S. W. Draper, and G. R. S. Weir, editors, People and Computer IX -Proceedings of HCI’94, pages 327–338. Cambridge University Press, 1994.Google Scholar
  20. 20.
    Fabio Paternó. A Method for Formal Specification and Verification of Interactive Systems. PhD thesis, Department of Computer Science, University of York, 1995.Google Scholar
  21. 21.
    John Rushby. Model checking and other ways of automating formal methods. Position paper for panel on Model Checking for Concurrent Programs, Software Quality Week, San Francisco, May/June 1995.Google Scholar

Copyright information

© Springer-Verlag Wien 1998

Authors and Affiliations

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

Personalised recommendations