Gulfs of expectation: eliciting and verifying differences in trust expectations using personas

Personas are detailed description of imaginary people that embody shared assumptions about users of a product, data regarding users of a product, or both [4]. Unlike task models which focus on modelling activities that humans undertake, personas are concerned with their needs and expectations.

Personas were first introduced by Cooper [5] as a means for dealing with programmer biases arising from the word user. These biases lead to programmers introducing assumptions causing users to bend and stretch to meet these needs; Cooper called this phenomenon ‘designing for the elastic user’; his solution was to design for a single user representing the target segment of the system or product being designed. This approach brings two benefits. First, designers only have to focus on those requirements necessary to keep the target persona happy. Second, the idiosyncratic detail associated with personas makes them communicative to a variety of stakeholders. Since their initial proposal over a decade ago, personas have now become a mainstay in User Experience practice, with articles, book-chapters, and even a book [4] devoted to the subject of developing and applying them to support interaction design.

Personas have also been useful for engaging stakeholders in quality concerns like security [2], and the analysis that contributes to their creation complements security analysis by identifying opportunities for both use and misuse [6]. A visual illustration of the role personas can play in design for security can be seen in [7].

Personas help describe the impact of human factors when imagining how a system might be used; knowing these behaviours can be useful when prioritising features or looking for innovative ideas. However, many insights that might lead to innovation may not have been obvious when originally creating personas. Such insights may be locked in the empirical data upon which the artifacts are based, and may not emerge by simply presenting them to stakeholders, or writing them into a scenario.

Qualitative data analysis techniques have been shown to be effective at making sense of the data upon which personas are based. A leading approach for qualitative data analysis is Grounded Theory; this is a qualitative data analysis technique for generating theory from observed real-world phenomena [8]. These theories, and the sense-making activities associated with carrying them out, form the raw material that subsequent design activities can build upon.

Grounded Theory involves the application of three coding activities. To help make initial sense of the data, open coding is carried out to initially categorise themes arising in the data. The analytic tool of sensitising questions is used to help the researcher to see process, variation, and so on, and to make connections between concepts. Axial coding involves crosscutting, or relating, concepts to each other; this activity goes hand-in-hand with, rather than separately following, open coding [8]. Causes, conditions, contexts, and consequences are identified, mapped using semantic relationships, and structured into categories; this leads to new insights into the source material, and guides subsequent coding activities. During selective coding, emergent categories are organised around a central, core category according to specific criteria, such as ensuring the central category is abstract, it appears frequently in the data, it is logical and consistent with the data, and the concept grows with depth and explanatory power as other categories are related to it.

Grounded Theory is not traditionally construed as a design technique per se, but it has been used for theory-building in security and privacy research. For example, Adams [9] used Grounded Theory to induce a method of user perceptions of privacy from empirical data, and Fléchais [10] used Grounded Theory to induce and refine a model of the factors affecting the design of secure systems, based on empirical data gathered from several different case studies.

One of the barriers to exploring the efficacy of this technique is a lack of understanding between qualitative data analysis research concepts and usability design concepts. Without this understanding, it is difficult to envisage how tool support might help both design and research activities. The Persona Case framework (illustrated in Fig. 1) was designed to surmount this barrier by illustrating how qualitative models can be used to systematically derive personas [11]. This involves treating a design problem as a research problem, and devising research questions to characterise it. Qualitative research is then conducted to collect empirical data from the user population of concern; this might include running interviews, or some form of ethnographic study. The qualitative data collected is then coded and analysed using Grounded Theory to develop a conceptual model that tackles the research problem. Using models based Toulmin’s Model of Argumentation [12], each relationship from this conceptual model is structured to motivate and justify a persona’s characteristic.

Recent work has illustrated how the Persona Case framework can be used to elicit trust characteristics from pre-existing personas [13]. These are useful for understanding the expectations about a system that personas of users expect to hold, or personas of developers expect users to satisfy. These characteristics describe the attributes of personas that lead them to behave in a trustworthy manner (intrinsic trust), and attributes of the context that motivate persona trustworthy behaviour (contextual trust). The work builds on Riegelsberger’s framework for trust in technology-mediated interactions [14] to support a grounded theory analysis of trust factors influencing a particular user population. The research questions that drive the coding process are motivated by this framework, and include questions about intrinsic and contextual trust properties. The Persona Case framework is then used to derive intrinsic or contextual trust characteristics from each relationship in the grounded theory model.

While personas and their trust characteristics can identify the trust expectations an archetypical system user or system developer might have, it may not be apparent what the impact of expectation clashes might be in terms of system behaviour. Consequently, it may not be apparent that undesirable outcomes, ranging from unexpected system behaviour through to inconsistent use of security mechanisms, result from these clashes.

Formal methods can help identify such clashes. As the design of trustworthy systems requires input from stakeholders from different disciplines, formal methods allow contributions from these different disciplines to be represented in forms that can be understood properly and contextually by all stakeholders in the design process; it does this by providing rules about how to describe and reason about people and systems. Moreover, if models of users and the interacting system can be described precisely, claims about how easy activities are for users can be assessed, or how trustworthy a system is given their expectations. Assessing these claims is particularly important when complex interactions between system elements are difficult to make sense of, and lead to emergent behaviour that may be obvious when carrying out normal testing activities.

Dix has identified several kinds of formal methods for HCI, the most dominant classes being user methods that encompass models for analysing interaction, and system methods that model the system the user interacts with. The contribution that failures in human-automation interaction have made to aviation accidents [15], has led to innovation in a variety of different user methods for observing and analysing how users carry out tasks to achieve their goals, together with methods for modelling the outcomes of this research [16]. Although the task analysis carried out by designers to create such models can be time consuming, task analysis and modelling are still frequently used by human factors researchers, particularly those working in regulated domains like aviation and maritime. However, despite work on adapting task modelling techniques to support the engineering of interactive systems, e.g. [17‐20], they can be problematic when considering their design for two reasons.

First, task analysis and task modelling were devised to evaluate human performance associated with some design in context. As such, one needs to design and implement the system before analysing and modelling how a human user interacts with it. Such systems are usually highly complex, and the role of the human is limited to those activities necessary to support them. In contrast, humans play a more instrumental role in many software systems we encounter on a day-to-day basis, such as desktop productivity tools or mobile apps; their context of use also affords greater creativity and unpredictability. While we might envisage how humans use such systems, the cost of analysing and formally modelling their use as tasks would be exorbitant.

Second, while task models of envisaged systems appear useful for modelling tasks at a high level of abstraction, they are ineffective if tasks are accomplished in different ways without significant differences in effective performance; Diaper [21] illustrates this by providing examples from Air Traffic Control where, at a high level, tasks frequently appear brief and routine, whereas at lower levels are much more elaborate.

Because of the way that behavioural nuances are manifested, modelling user interactions in system terms provide a means for identifying erroneous or suspicious behaviour on an a priori basis [22, 23]. In their review of formal verification techniques for Human-Automation Interaction, Bolton et al. [15] describe two dominant strategies for eliciting differences in modes of behaviour using system based formal methods.

The first strategy involves the use of theorem proving, where theories are built and proven to verify a system’s correctness. This strategy was used by Masci et al. [24], who used PVS to support a field study into the social aspects of cognition by different participants. PVS (Prototype Verification System) is a framework for constructing specifications in higher-order logic that can be subject to theorem proving [25]. Masci et al. analysed different information resources and developing theories that explained physical and social work activities. While such a strategy appears to complement the activities associated with user experience research, automating this strategy can be difficult due to the expressive nature of the logics used.

The second strategy entails the use of model checking, where formal models are verified to see if they satisfy desired properties encapsulated within a specification. Bolton [20] demonstrated such an approach using Enhanced Operator Function Model with Communications (EOFMC) to model human-human protocols. The instantiated EOFMC task model was translated into SAL, and input into the SAL-SMC model checker to find countere xamples associated with potential miscommunication.

One problem associated with both of the above strategies, which arguably stymies the broader take-up of formal methods, is the creation of verifiable specifications of people and systems. In the examples described by Masci et al. and Bolton, specifications were created by analysing pre-existing system documentation and case data. However, in a real design setting, the available qualitative data may not be in such a digestible format.

While it is usually employed as a specification language for verifying concurrent protocols, CSP (Communicating Sequential Processes) has also been used for modelling patterns of interaction at higher levels of abstraction. CSP is a language for describing observable behaviour [26]. Components representing designs or properties are represented using processes, and processes and behaviours are described in terms of events. Although the process algebra used to model behaviours in CSP can be expressive, most models can be specified using only the Stop, prefix, external, and internal choice operators.

The below specification (taken from [27]) illustrates the use of CSP to model the Dining Philosopher’s problem [28].

Behaviours can also be described using traces, which are sequences of events that may be performed. In large models, we are interested in sequences of events that lead to failures. Using the FDR (Failure-Divergence Refinement) model checker [29], it is possible to carry out a refinement check of one specification against the properties of another. Refinement check failures lead to traces that provide evidence of divergences, where undefined behaviour might arise following a particular point.

A more thorough description of CSP and FDR is beyond the scope of this paper, but a more detailed introduction to both is provided by [30].

CSP is precise enough for its specifications to be formally checked, yet also expressive enough to deal with some nuances of human interactions. For example, Buth [31] used CSP, together with the FDR model checker to compare mental and system models associated with an aircraft’s autopilot system, and evaluate whether the mental models were valid refinements of the system’s specification. CSP has also be used to verify instance-based behavioural models such as use cases [32] and scenarios [33], and reasoning about interactions between multiple human actors; this was demonstrated by Jirotka and Luff, who used CSP to model work practices associated with shares trading [34].

If it were possible to derive and express characteristics suggesting the mental state of personas using CSP, it would be possible to use refinement checking to anticipate their likely behaviour, investigate whether this behaviour satisfies a system’s safety and liveness properties, or is free from divergent behaviour. This would help to highlight patterns of behaviour that betray the trust placed by the developer (through the system design) on the user. While there is no obvious means for deriving such characteristics, Jirotka and Luff [34] indicate how this may be possible. Specifically, to elicit the CSP events and processes associated with a financial trading floor, Jirotka and Luff carried out qualitative data analysis of video transcripts; this involved summarising segments of text using categories, and drawing relationships between these categories to not only make sense of these categories, but identify hitherto invisible themes within the transcripts themselves. The categories elicited formed the basis of candidate CSP events and processes. As they began to make more sense of this data, they were able to perceive how such interactions might be formalised. Moreover, undertaking this formal analysis complemented the qualitative data analysis by providing an even better understanding of the original transcripts.

As indicated earlier, when undertaking a qualitative data analysis, segments of text (quotations) are characterised with one or more codes. Codes are words that capture a summative, salient, essence-capturing and/or evocative attribute for a portion of language-based or visual data [40]. The codes of particular interest to us concern events. These correspond to CSP events: codes characterising interaction for processes, be these processes within a system specification, or processes implied from persona behaviour.

Codes are stored in a code book database, which is maintainable by team members. Based on the guidelines proposed by [41] for maintaining codes, each entry contains a full description, an inclusion criteria for when text should and should not be categorised with the code, and an example of some text categorised by the code.

To capture the elements of gulfs of expectation, we need to associate a number of concepts with those used to specify CSP descriptions. The conceptual relationships are illustrated in the UML class diagram shown in Fig. 3.

Implied specifications need to be created of untrustworthy behaviour that personas might exhibit. These specifications contain descriptions of one or more implied processes. Implied processes are CSP process descriptions that formally specify some interaction between a persona and its environment, but this interaction is only implied by the persona. Although this behaviour is summarised narratively, it is formally specified using a CSP process description. The process description incorporates channels that are based on event codes.

The model described in Fig. 3 was implemented in CAIRIS by augmenting its database structure to include additional tables and relationships corresponding with the diagram’s classes and associations respectively.

The implied processes can be combined into a single formal CSP implied specification for an activity corresponding to a system of interest. The combination of these processes into a single model is performed by a Java application, which interfaces to FDR.

Using FDR, we verify this generated model against the system specification to identify whether mistrusting behaviour in the implied process violates the system specification. If it does, allowable event traces that violate the system are output. These traces demonstrate failures that provide evidence of gulfs of expectation.

We elicited trust characteristics for the pre-existing Helen and Jimmy personas by carrying out qualitative data analysis of pre-existing data; this data was collected during workshops attended by prospective users and developers. The attendees were recruited based on shared characteristics with the Helen and Jimmy personas, and the workshop considered how the participants made access control decisions. Further details about this study can be found in [45].

The workshop reports were subject to a grounded theory analysis, and Riegelsberger’s framework was used to develop a series of sensitising questions to help variate and make connections between the different codes. To illustrate these, Fig. 4 shows the questions used to code Helen workshop reports.

From the grounded theory analysis, 57 and 37 quotations were elicited based on the Helen and Jimmy focus group reports respectively; these quotations were based on 26 codes. Figure 5 shows conceptual models generated by CAIRIS based on this analysis, and from which code networks will be based; the numbers associated with each node correspond with the number of quotations categorised with each code.

Relationship within the conceptual models form the basis of individual trust characteristic. For example, Fig. 6 illustrates how the trust characteristic Knowing the user increases tendency to trust them is a synopsis of the code relationship between the role possibilities and emergent trust codes.

Narrative descriptions summarising these characteristics from both personas are provided below.

Once tentative trust characteristics are available, gulfs of expectation can be identified when the conventional use of a specified system is challenged. These instances constitute system mistrust as the positive estimation of trust by a trustee is either intentionally or unintentionally betrayed [46]. These instances are found by verbalising potential cases of mistrust, formalising them as CSP descriptions and, based on insights arising from this formalisation exercise, re-coding the qualitative data based on any events introduced to the shared code book.

Eliciting the trust characteristics suggested candidate implied processes for both Helen and Jimmy, as described below.

For this example, we consider the elicitation of implied processes based on the previously described trust characteristics for Helen and Jimmy. These elicited characteristics informed thinking about ways of formalising this behaviour, leading to implied processes for HELEN and JIMMY. In these processes, we model the way that Helen goes through the process of picking an application and running it with a given set of permissions, and Jimmy assumes a user would go through the same process.

To simplify the example, the permissions have been reduced to three possible values: tooLittle, justRight, and tooMuch; these represent the permissions granted relative to those needed for the application to run successfully. Likewise, the result of running the program can have one of four possible values which represent the program crashing (crash), the program running with limited functionality limited, the program running with full functionality (full), and the program communicating private information about the user (breach).

In addition to the channels used by the SYSTEM process three additional channels are used. The requested channel represents the permissions requested by an application and the run channel represents the permissions that the user has chosen to run the application with. When the application has been run the result is shown on the res channel.

The HELEN and JIMMY processes were combined and imported into FDR using the CAIRIS-FDR interface, and an implied specification generated.

In this example, there is a single user process and a single application process. In a more general analysis there could be a number of each type of process. The processes USERS and APPS represent the interleaving of these two types of processes.

The US process is the composition of the USERS and SYSTEM process where events on the pick and verify channels are synchronised. Similarly, UA is the composition of the US and APPS process where events on the pick, requested, run and res channels are synchronised.

In the system specification, two of the possible results represent error cases, these are crash and breach. To test for these error cases, we perform two separate trace refinement checks against processes that can perform any event apart from either crashes or breaches.

The output of the application is a number of traces that verify the presence of gulfs of expectation; these detail the sequence of events that led to the error condition.

There are two traces that result in the application crashing.

In the first of these Helen tries to install and run the Kids in Focus application on her laptop. Helen believed that the system would allow her to do this, but, due to an error in Jimmy’s coding, the application fails to request all the permissions needed to successfully run the application. As Helen is likely to accept the default permissions when using her laptop, she fails to spot the missing permissions and the application crashes.

Another example of an application crashing takes place when Helen installs Kids in Focus on Eric’s tablet. This time the error is not caused by Jimmy’s coding, which requests the correct permissions for the application to run, but by changes in Helen’s expectations between specifying permissions for the application and installing it. As Helen is very concerned about the privacy of Eric, she has denied some of the permissions needed for the application to run correctly; this has caused the application to crash.

The final trace results in a leaking of confidential information. This is similar to the first trace in that the application requests the wrong permissions due to a coding error. This time the application requests too many permissions, including ones that result in Helen’s private data being made public. As the system’s state is based on Jimmy’s expectations that users should have all the freedom of action they need, this results in a breach of Helen’s privacy.