Download Structural Usability Techniques for Dependable HCI

5.5 Meta-theorems: patterns and families
127
using the theorem discovery infrastructure on which the algorithm is built.
We also note that this is another case where partiality is particularly interesting: if a user believes that
some action sequence always takes them to a safe state, but actually in a few states that’s not true, that
represents a potential surprise and possibly even a hazard.
5.5.6
Families of theorems
There will frequently be cases where some aspect of a system’s interactive behaviour is expressed as a
set of theorems rather than just one. Action groups and undo, as described above, are two examples of
this phenomenon; in order to recognise their presence automatically, some post-processing is required
beyond the basic theorem discovery algorithm described in section 5.4. In the cases of action groups
and undo, we have identified particular patterns of theorems to look for; in general, however, families
can arise with unpredictable structure, as emergent properties of the particular system being analysed.
We see an example in section 6.5.2, with theorems on the ‘device’ model of the Casio HS-8V simulation
considered in section 4.5. There are two families of nine theorems each, where each family corresponds
to some (different) aspect of the system’s behaviour. To produce that analysis it was necessary to visually
examine the eighteen theorems that theorem discovery found on that model, and look for patterns — by
applying human intelligence it was then quite straightforward then to group the theorems together and
interpret them as described later. It is unclear at this time to what degree it ought to be possible to
automate or support this process; the question of how to do this in general is beyond the scope of this
thesis, and is proposed as future work; see also section 6.2.3.