Increasing activity in human-computer interaction (HCI) research over
the last twenty years indicates that the need to include human factors
issues into the design of systems has been recognised. However, the
findings of this research, particularly with respect to usability,
often do not seem to have found their way into the development
processes of interactive devices and systems. One possible
explanation is that the analysis methods offered by HCI researchers
often do not fit well in the engineering context. Most of these
methods focus on selected interface issues and are incompatible with
methods that focus on other design issues. Furthermore, some methods
are applicable at particular design stages only, whereas ideally they
should be usable throughout the whole design cycle. Additionally, in
the dependable systems domain, our primary area of concern, the use of
formal analysis techniques is often required by authorities. It is
partly to comply with those requirements that a number of formal
analysis methods have been developed in the field of HCI. These formal
approaches also make it possible to perform an unambiguous analysis
and to provide a basis for automated analysis of interactive system
properties, for example usability properties. However, generally
these methods use notations and focus on problems that are different
from those used by system designers. Therefore, the application of
these methods, if used at all in practice, is left to a human factors
specialist. This often leads to usability analysis being one of the
last steps in the design process, where changes in the design are most
expensive. If formal usability analysis methods were more compatible
with standard system design techniques and notations, there might be a
chance of these methods being better integrated in the earlier stages
of the design process.
The proposed thesis addresses these issues by introducing an
approach for the model-based automated analysis of dependable
interactive systems. The main objectives of this approach are (1) to
be accessible by non-formal methods experts, like usability engineers,
and (2) to interface with the methods and techniques that are already
in place in dependable systems engineering, without excessive extra
costs. The approach, called practical formal analysis, provides an
analysis framework that utilises standard techniques for the
specification and validation of dependable systems, and it is supposed
to accompany the design process throughout all stages. To communicate
the results of the analysis to stakeholders with different background,
a suitable rendering of these results will be provided. In this
context scenarios of work are being used as a means of communication.