The systematic analysis of interactive devices to explore potential problems that might arise through their use provides an important element in the design of new systems or the analysis of existing systems. The use of behavioral models, focusing on the system and supported by automated reasoning, to analyze human-computer interaction has been the subject of previous research [1, 2, 3, 4] but how best to fold the user into the analysis of system resilience remains an open problem. We are currently working on a technique that tackles this issue by narrowing the model checking analysis of interactive systems to cognitively plausible behaviours (those behaviours that are likely to be carried out by users because the device or the user’s training or some other contextual factor leads to it).
Assumptions about how the system is to be used are established in the technique by making information needs explicit. This process includes establishing whether the right information is provided to the user at the right time in support of activities. The designer must consider a range of issues: support for a range of user strategies, making the most of available screen space, avoiding information overload, and reconciling competing information requirements when the system supports a number of different activities. These information needs provide constraints on user behavior, and together with additional resources afforded by the environment as a whole in which the system is situated, act to shape the likely behaviors of the end user. Encoding these information needs, and using them to drive analysis, enables consideration of a broader class of uses and user behaviors than could be achieved by restricting analysis to the behaviors encoded in more prescriptive models of user behavior (for example, task models), while at the same time eliminating many of the false negatives (in an HCI perspective) that a totally unconstrained device model would generate.
A preliminary version of this work has been published [5, 6]. We are currently further developing the technique and applying it to safety critical devices (e.g., infusion pumps). You can contact me if you would lime more details (email@example.com).
 F. Paternò and G. Ballardin. Model-aided Remote Usability Evaluation. In M. Angela Sasse and Chris Johnson, editors, Human-Computer Interaction – INTERACT ’99, volume 1, pages 434–442. IOS Press, 1999.
 J.C. Campos and M.D. Harrison. Model checking interactor specifications. Automated Software Engineering, 8:275–310, 2001.
 J. Rushby. Using model checking to help discover mode confusions and other automation surprises. Reliability Engineering and System Safety, 75(2):167–177, February 2002.
 K. Loer. Model-based Automated Analysis for Dependable Interactive Systems. PhD thesis, Department of Computer Science, University of York, UK, 2003.
 J.C. Campos and G. Doherty. Supporting resource-based analysis of task information needs. In Interactive Systems: Design, Specification and Verification, volume 3941 of Springer Lecture Notes in Computer Science, pages 188–200. Springer-Verlag, 2006.
 G. Doherty, J.C. Campos, and M.D. Harrison. Resources for situated actions. In Interactive systems: Design, Specification and Verification, volume 5136 of Springer Lecture Notes in Computer Science, pages 194–207. Springer-Verlag, 2008.