Skip to main content
SpringerLink
Log in

Formal Interactive Systems Analysis and Usability Inspection Methods: Two Incompatible Worlds?

  • Conference paper
  • First Online:
Interactive Systems Design, Specification, and Verification (DSV-IS 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1946))

Abstract

We present our view on how a formal technique for the analysis of interactive systems can be used to support ‘discount’usability inspection methods. As a demonstration, we present a snapshot of our work on supporting heuristic evaluation and on the analysis of selected usability properties. Our method focuses on the exhaustive analysis of functional properties. We claim that the benefits gained by a formal approach like the one presented here justify its extra costs. Moreover, we believe these costs can be kept comparably low by making the analysis technique flexible enough to support a number of other (informal) analysis techniques throughout the different stages of the design process.

In fact, for some types of safety-critical systems the use of formal design techniques is required by authorities (see, for example, UK MoD Defense Standard 00-56, safety integrity level S4 of systematic failure integrity).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J. Nielsen and R. L. Mack, Usability Inspection Methods, John Wiley & Sons, Inc. 1994

    Google Scholar 

  2. Virzi, R. A., Usability Inspection Methods, in Handbook of Human-Computer Interaction, K. Helander, Landauer T. K., and Prabhu P., Editors. 1997, chapter 29, Elsevier Science B. V.

    Google Scholar 

  3. Harel, D., Statecharts: A visual formalism for complex systems. Science of Computer Programming, 1987: p. 231–274.

    Google Scholar 

  4. McMillan, K. L., Symbolic model checking. 1993: Kluwer.

    Google Scholar 

  5. Norman, D. A., Design Principles for Human-Computer Interaction, in Proceedings of CHI’83. 1983, ACM. p. 1–10.

    Google Scholar 

  6. Dix, A., J. Finlay, G. Abowd, and R. Beale, Human Computer Interaction (2nd edition). 1998: Prentice Hall Europe.

    Google Scholar 

  7. Shneiderman, B., Designing the user interface: strategies for effective human-computerinteraction. 1998: Addison Wesley.

    Google Scholar 

  8. Nielsen, J., Enhancing the explanatory power of usability heuristics, in Proceedings of the CHI’94 Conf. 1994, ACM: Boston, MA. p. 152–158.

    Google Scholar 

  9. Nielsen, J. Finding usability problems through heuristic evaluation. in Proc. of ACM CHI’92 Conference on Human Factors in Computing Systems. pp249–256. New York, 1992, ACM.

    Google Scholar 

  10. Lüttgen, G. and V. Carreño, Analyzing Mode Confusion via Model Checking. 1999, Technical Report, ICASE.

    Google Scholar 

  11. Rushby, J., Using Model Checking to Help Discover Mode Confusions and Other Automation Surprises, in (Pre-) Proceedings of the Workshop on Human Error, Safety, and System Development (HESSD). chapter 13, 1999.

    Google Scholar 

  12. Palmer, E. Murphi busts an Altitude: A Murphi Analysis of an Automation Surprise. in Proceedings of the 18th Digital Avionics Systems Conference (DASC). 1999: IEEE Press.

    Google Scholar 

  13. Butler, R. W., S. P. Miller, J. N. Potts, and V. A. Carreño. A Formal Methods Approach to the Analysis of Mode Confusion. in Proceedings of the 17th Digital Avionics Systems Conference. 1998. Bellevue, Washington.

    Google Scholar 

  14. Abowd, G., H. Wang, and A. Monk, A formal technique for automated dialogue development, in Proceedings of the First Symposium on Designing Interactive Systems, DIS’95. 1995, ACM Press. p. 212–226.

    Google Scholar 

  15. Paternò, F. D., A Method for Formal Specification and Verification of Interactive Systems. DPhil Thesis, Department of Computer Science, University of York, UK, 1996.

    Google Scholar 

  16. Faconti, G. and F. Paternò. An approach to the formal presentation of the components of an interaction. in Eurographics’ 90. 1990. Montreaux: North-Holland.

    Google Scholar 

  17. d’Ausbourg, B. Using Model Checking for the Automatic Validation of User Interfaces Systems. in P. Markopoulos and P. Johnson, eds., Design, Specification and Verification of Interactive Systems’ 98. 1998: Eurographics, Springer Verlag.

    Google Scholar 

  18. Campos, J. C., Automated Deduction and Usability Reasoning. DPhil Thesis, Department of Computer Science, University of York, UK, 2000.

    Google Scholar 

  19. Duke, D. J. and M. D. Harrison, Abstract Interaction Objects. Computer Graphics Forum, 1993. 12( 3): p. 25–36.

    Article  Google Scholar 

  20. Kyng, M., Creating Contexts for Design, in Scenario Based Design:Envisioning Work and Technology in System Development, J. M. Carroll, Editor. chapter 4, John Wiley & Sons, 1994.

    Google Scholar 

  21. Fields, B., M. D. Harrison, and P. Wright, THEA: Human Error Analysis for Requirements Definition. 1997, Technical Report YCS294, Department of Computer Science, University of York.

    Google Scholar 

  22. Clarke, E. M., J. M. Wing et al., Formal Methods: State of the Art and Future Directions. ACM Computing Surveys, 1996. 28(4): p. 626–643.

    Article  Google Scholar 

  23. Degani, A., On Modes, Error, and Patterns of Interaction, PhD Thesis, Georgia Institute of Technology, 1996.

    Google Scholar 

  24. Harel, D., H. Loachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, and M. Trakhtenbrot, STATEMATE: A Working Environment for the Development od Complex Reactive Systems. IEEE Transactions on Software Engineering, 1990. 16(4): p. 403–413.

    Article  Google Scholar 

  25. Armstrong, J. M., Industrial Integration of Graphical and Formal Specifications. Journal of Systems & Software Special Issue on Formal Methods Technology Transfer, 1998. 40: p. 211–225.

    Article  Google Scholar 

  26. von der Beeck, M., A Comparison of Statecharts Variants, in Formal Techniques in Real-Time and Fault-Tolerant Systems, H. Langmaack, W.-P. de Roever, and J. Vytopil, Editors. 1994, Springer-Verlag. p. 128–148.

    Google Scholar 

  27. Harel, D. and A. Namaad, The STATEMATE Semantics of Statecharts. ACM Transactions on Software Engineering and Methodology, 1996. 5(4): p. 293–333.

    Article  Google Scholar 

  28. Loer, K. and Harrison, M., Model-checking statechart interface descriptions. 2000, in preparation.

    Google Scholar 

  29. Mitchell, C. M., Operator Models, Model-Based Displays and Intelligent Aiding, in Human/Technology in Complex Systems. 1996, JAI Press Inc. p. 67–172.

    Google Scholar 

  30. Kirwan, B., A Guide to Practical Human Reliability Assessment. 1994: Taylor & Francis.

    Google Scholar 

  31. Campos, J. C. and M. D. Harrison. The role of verification in interactive system design. in P. Markopoulos and P. Johnson, eds., Design, Specification and Verification of Interactive Systems’ 98. 1998: Eurographics, Springer Verlag. p. 155–170.

    Google Scholar 

  32. Clarke, E. M., 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, 1986. 8(2): p. 244–263.

    Article  MATH  Google Scholar 

  33. Dwyer, M. B., G. S. Avrunin, and J. C. Corbett. Property Specification Patterns for Finite-State Verification. in M. Ardis, ed., 2nd Workshop on Formal Methods in Software Practice. 1998. p. 7–15.

    Google Scholar 

  34. Dix, A., R. Mancini, and S. Levaldi, The cube — extending systems for undo, in Proceedings on the 4th Eurographics Workshop on Design, Specification and Verification of Interactive Systems (DSVIS), M. D. Harrison and J. C. Torres, Editors. 1997, Springer-Verlag. p. 119–134.

    Google Scholar 

  35. Butterworth, R., A. Blandford, and D. Duke. The role of formal proof in modelling interactive behaviour. in P. Markopoulos and P. Johnson, eds., Design, Specification and Verification of Interactive Systems’ 98. 1998: Eurographics, Springer Verlag p. 87–101.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. BAE SYSTEMS Dependable Computing Systems Centre Department of Computer Science, University of York, YO10 5DD, York, UK

    Karsten Loer & Michael Harrison

Authors
  1. Karsten Loer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Harrison
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LIHS University Toulouse 1, Place Anatole France, 31042, Toulouse Cedex, France

    Philippe Palanque

  2. Istituto CNUCE, Consiglio Nazionale delle Ricerche, Via V. Alfieri 1, 56010, Ghezzano-Pisa, Italia

    Fabio Paternò

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Loer, K., Harrison, M. (2001). Formal Interactive Systems Analysis and Usability Inspection Methods: Two Incompatible Worlds?. In: Palanque, P., Paternò, F. (eds) Interactive Systems Design, Specification, and Verification. DSV-IS 2000. Lecture Notes in Computer Science, vol 1946. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44675-3_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-44675-3_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41663-0

  • Online ISBN: 978-3-540-44675-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation