Time and context modelling in interactive systems
model checking, timing, context, ubiquitous systems, human computer interaction
For many interactive systems the cost of their undependability in terms of human safety, material destruction, commercial or economic impact and security is high. For many systems, dependability relies in part on the ability of a human user to interact to prevent failure from occurring. When designing dependable interactive systems therefore it is important to identify and, where possible, to eliminate difficulties in the design that might lead a user carrying out actions that might compromise its dependability. Although a number of techniques have been developed by the Human Computer Interaction (HCI) community to assess interactive systems at early stages in design, these techniques do not map well into the system or software engineering processes. They are not well integrated with the practices and understandings of system and software engineers. Many of these techniques involve prototype or sketch designs and feedback from potential users, but others involve team inspection of a design such as the cognitive walk-through method . In such methods designers, domain experts and potential users together or individually consider the design in the context of representative activities and explore and evaluate the design. It is typical of these techniques that standard questions or heuristics are used by the evaluators to trigger observations about the usability of the system. These techniques are useful, though their value is difficult to measure. Experiments, intended to explore their value, lead to conclusions that are difficult to assess in the context of general usage of the approaches . These methods require considerable domain and human factors expertise in order that they can be applied effectively.
In order to close the gap between HCI practice and software engineering processes a tool (IFADIS)  has been developed to support a model checking process for the analysis of dependable interactive systems. This tool supports the modelling of interactive systems using statecharts, supports the specification of properties based on a hierarchy of usability engineering patterns akin to Dwyer's patterns  for describing temporal logic properties and provides a simple visualisation of counter-examples or witnesses to properties.
In addition, further extensions to current HCI practice have been explored using model checking techniques. It is clear that environmental issues are crucial to understanding the user's interaction with a device. In this connection the focus of attention has been timing and context.
 Dwyer, M., Avrunin, G. and Corbett, J. (1999) Petterns in property specifications for finite state verification. In 21st International Conference on Software Engineering, Los Angeles, California.
 Gray, W. and Salzman, M. (1998) Damaged merchandise? a review of experiments that compare usability evaluation methods. Human Computer Interaction 13(3): 203-261.
 Loer, K. and Harrison, M. (2002). Towards usable and relevant model checking techniques for the analysis of dependable interactive systems. In Emmerich, W. and Wile, D., editors, Proceedings of Automated Systems Engineering: ASE'02. IEEE Computer Society Press. pp. 223-226.
 Wharton, C., Rieman, J., Lewis, C. and Polson, P. (1994) The cognitive walkthrough method: a practitioner's guide. In Nielsen, J. and Mack, R., editors Usability Inspection Methods, Chapter 2 John Wiley & Sons, Inc.
Loer, K. and Harrison, M. (2002). Towards usable and relevant model checking techniques for the analysis of dependable interactive systems. In Emmerich, W. and Wile, D., editors, Proceedings of Automated Systems Engineering: ASE'02. IEEE Computer Society Press. pp. 223-226.
Loer, K., Hildebrandt, M. & Harrison, M. (2004) Analysing dynamic function scheduling decisions.In Johnson and Palanque (editors) Human Error, Safety and Systems Development. Kluwer Academic. pp. 45-60
Loer, K. & Harrison, M.D. (in press) Analysing user confusion in context aware mobile applications. In proceedings Interact 2005. Springer Lecture Notes in Computer Science.
Michael Harrison (Newcastle)
|Page Maintainer: email@example.com||Credits||Project Members only||Last Modified: 10 August, 2005|