Formally Verifying Interactive Systems: A Review

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


Although some progress has been made in the development of principles to guide the designers of interactive systems, ultimately the only proven method of checking how usable a particular system is must be based on experiment. However, it is also the case that changes that occur at this late stage are very expensive. The need for early design checking increases as software becomes more complex and is designed to serve volume international markets and also as interactions between operators and automation in safety-critical environments becomes more complex. This paper reviews progress in the area of formal verification of interactive systems and proposes a short agenda for further work.


User Interface Model Check Temporal Logic Interactive System Theorem Prove 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  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.Google 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 [2], pages 347–365.Google Scholar
  4. 4.
    J. R. Burch, E. M. Clarke, and K. L. McMillan. Symbolic model checking: 1020 states and beyond. In L/CS, 1990.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.
    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 [2], pages 105–122.Google Scholar
  7. 7.
    Alan Dix and Gregory Abowd. Modelling status and event behaviour of interactive systems. Software Engeneering Journal, 11 (6): 324 – 346, November 1996.Google Scholar
  8. 8.
    Alan Dix, Janet Finlay, Gregory Abowd, and Russell Beale. Human-Computer Interaction. Prentice Hall, 1993.Google Scholar
  9. 9.
    David Duke, Michael Harrison, Jöelle Coutaz, Laurence Nigay, Daniel Salber, Giorgio Faconti, Menica Mezzanotte, Fabio Paterno, and David Duce. The Amodeus system reference model. Technical Report System Modelling/D9, Amodeus Project, June 1995.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.
    D.J. Duke, P.J. Barnard, J. May, and D.A. Duce. Systematic development of the human interface. In Asia Pacific Software Engeneering Conference, pages 313 – 321. IEEE Computer Society Press, December 1995.Google Scholar
  12. 12.
    Urban Engberg, Peter Grønning, and Leslie Lamport. Mechanical verification of concurrent systems with TLA. In Computer Aided Verification, Proceedings of the Fourth International Workshop, CAV’92, volume 663 of Lecture Notes in Computer Science. Springer-Verlag, 1992.Google Scholar
  13. 13.
    Bob Fields, Peter Wright, and Michael Harrison. A method for user interface development in safety-critical applications. Human-Computer Interaction Group, University of York (unpublished ), 1996.Google Scholar
  14. 14.
    Mark Green. A survey of three dialogue models. ACM Transactions on Graphics, 5 (3): 243 – 275, July 1986.Google Scholar
  15. 15.
    John V. Guttag, James J. Horning, et al. Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer-Verlag, 1993.Google Scholar
  16. 16.
    Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16 (3): 872 – 923, May 1994.CrossRefGoogle Scholar
  17. 17.
    Nancy Leveson. Safeware: System Safety and Computers. Addison-Wesley Publishing Company, Inc., 1995.Google Scholar
  18. 18.
    José A. Mañas et al. Lite User Manual. LOTOSPHERE consortium, March 1992. Ref. Lo/WP2/N0034/V08.Google Scholar
  19. 19.
    Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer, 1995. Google Scholar
  20. 20.
    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 ofHCI’94, pages 327–338. Cambridge University Press, 1994.Google Scholar
  21. 21.
    R. De Nicola, A. Fantechi, S. Gnesi, and G. Ristori. An action-based framework for verifying logical and behavioural properties of concurrent systems. Computer Networks and ISDN Systems, 25 (7): 761 – 778, February 1993.MATHCrossRefGoogle Scholar
  22. 22.
    Philippe Palanque, Fabio Paterno, Remi Bastide, and Menica Mezzanote. Towards an integrated proposal for interactive systems design based on TLIM and ICO. In Bodart and Vanderdonckt [2], pages 162–187.Google Scholar
  23. 23.
    Fabio Paterno. A Method for Formal Specification and Verification of Interactive Systems. PhD thesis, Department of Computer Science, University of York, 1995.Google Scholar
  24. 24.
    S. Rajan, N. Shankar, and M.K. Srivas. An integration of model-checking with automated proof checking. In Computer-Aided Verification, CAV95, volume 939 of Lecture Notes in Computer Science, pages 84 – 97. Springer Verlag, July 1995.Google Scholar
  25. 25.
    Harold Thimbleby. User Interface Design. Frontier Series. ACM Press, 1990.Google Scholar
  26. 26.
    Hung-Ming Wang and Gregory D. Abowd. A tabular interface for automated verification of event-based dialogs. Technical Report CMU-CS-94-189, Department of Computer Science, Carnegie Mellon University, July 1994.Google Scholar

Copyright information

© Springer-Verlag/Wien 1997

Authors and Affiliations

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

Personalised recommendations