The Handbook of Formal Methods in Human-Computer Interaction

This chapter provides an overview of several formal approaches for the design, specification, and verification of interactive systems. For each approach presented, we describe how they support both modelling and verification activities. We also exemplify their use on a simple example in order to provide the reader with a better understanding of their basic concepts. It is important to note that this chapter is not self-contained and that the interested reader should get more details looking at the references provided. The chapter is organized to provide a historical perspective of the main contributions in the area of formal methods in the field of human–computer interaction. The approaches are presented in a semi-structured way identifying their contributions alongside a set of criteria. The chapter is concluded by a summary section organizing the various approaches in two summary tables reusing the criteria previously derived.

In this chapter, we present an overview of some of the general themes and topics that can be seen in research into formal methods in human–computer interaction. We discuss how the contents of the rest of the book relate to these topics. In particular, we show how themes have evolved into particular branches of research and where the book contents fit with this. We also discuss the areas of research that are relevant, but are not represented within the book chapters.

This chapter attempts to identify future research directions for formal methods in HCI. It does this using two main approaches. First, we will look at trends within HCI more broadly and the challenges these pose for formal methods. These trends in HCI are often themselves driven by external technical and societal change, for example the growth of maker/hacker culture and the increasing dependence of basic citizenship on digital technology, effectively establishing external requirements for the field. Second we will look inwards at the FoMHCI literature, the user interaction phenomena it is trying to address and the processes of interaction design it is intended to support. Through this second analysis we will identify internally generated trends. This does not lead to a single overarching research agenda, but does identify a number of critical areas and issues, and hence establishes opportunities for further research to expand the state of the art.

This chapter introduces a set of case studies that are used in the rest of the book. They encompass well-known problem domains in human–computer interaction research and provide a practical focus for the approaches presented in this book. The set of case studies includes case studies concerned with the controller interface to a (semiautomated) nuclear power plant; a partly autonomous arrival management interactive system in the domain of air traffic control; a user interface for new interactive cockpits; and an interactive system used in rural and urban areas to maintain wind turbines. The final case study brings an interesting perspective for formal techniques, namely interactive public displays.

This chapter presents the visual Formal Interaction Logic Language (FILL) for the description of executable user interface models. This modeling approach is based on an architecture called 3LA, which separates a user interface from its outward appearance as a set of interaction elements called physical representation, and its functional part called interaction logic, which connects the physical representation with the system to be controlled. The latter refers in general terms to a business model of an interactive system, where the interaction logic is further meant to describe dialog-specific aspects, e.g., the availability of widgets depending on the system state or other widgets. FILL is algorithmically transformed to reference nets, a special type of Petri nets, which makes it executable and equips FILL with formal semantics through the formal semantics of reference nets. FILL models are modularization which enables the description of multidevice user interface models as well as the reuse and exchange of parts of the model. For the creation and execution of FILL-based user interface models, the UIEditor tool is presented. It offers editors for modeling the physical representation and the modularized FILL-based interaction logic. It further implements the transformation algorithm for generating reference nets out of a given FILL model and finally the execution environment for the user interface model. The applicability of this modeling approach will be shown by means of a case study for the control of a simplified nuclear power plant. The chapter will conclude with a broader view to future challenges this approach is facing.

Our approach for modelling interactive systems has been to develop models for the interface and interaction which are lightweight but with an underlying formal semantics. Combined with traditional formal methods to describe functional behaviour, this provides the ability to create a single formal model of interactive systems and consider all parts (functionality, user interface and interaction) with the same rigorous level of formality. The ability to convert the different models we use from one notation to another has given us a set of models which describe an interactive system (or parts of that system) at different levels of abstraction in ways most suitable for the domain but which can be combined into a single model for model checking, theorem proving, etc. There are, however, many benefits to using the individual models for different purposes throughout the development process. In this chapter, we provide examples of this using the nuclear power plant control system as an example.

When modelling user interactions, we normally assume that the user is acting with intention: some very explicit such as opening a valve in a nuclear power station, others more tacit, hardly needing any thought, for example tipping a tablet to turn a page. However, there are also a range of system behaviours that make use of unintentional user actions, where the user acts, but the system decides that the action has meaning, and how to make use of that meaning. Again, these may operate on a variety of levels from ‘incidental interactions’, which operate entirely without the user realising, perhaps subtle changes in search results based on past activity, to more ‘expected interactions’ such as automatic doors that open as you approach. For intentional interaction, there is long-standing advice—making sure that the user can work out what controls do, where information is, interpret the available information, receive feedback on actions—and also long-standing modelling techniques. Low-intention interactions, where the system has more autonomy, require different design strategies and modelling techniques. This chapter presents early steps in this direction. Crucial to this is the notion of two tasks: the sensed task, which the system monitors to gain information and the supported task, which the system augments or aids. First, this chapter demonstrates and develops techniques in the retrospective modelling of a familiar low-intention interaction system, car courtesy lights. These techniques are then applied proactively in the design of a community public display, which is now deployed and in everyday use.

In industrial control rooms, in our living rooms, and in our pockets, the devices that surround us combine physical controls with digital functionality. The use of a device, including its safety, usability and user experience, is a product of the conjoint behaviour of the physical and digital aspects of the device. However, this is often complex; there are multiple feedback pathways, from the look, sound and feel of the physical controls themselves, to digital displays or the effect of computation on physical actuators such as a washing machine or nuclear power station. Physigrams allow us to focus on the first of these, the very direct interaction potential of the controls themselves, initially divorced from any further electronic or digital effects—that is studying the device ‘unplugged’. This modelling uses a variant of state transition networks, but customised to deal with physical rather than logical actions. This physical-level model can then be connected to underlying logical action models as are commonly found in formal user interface modelling. This chapter describes the multiple feedback loops between users and systems, highlighting the physical and digital channels and the different effects on the user. It then demonstrates physigrams using a small number of increasingly complex examples. The techniques developed are then applied to the control panel of a wind turbine. Finally, it discusses a number of the open problems in using this kind of framework. This will include practical issues such as level of detail and times when it feels natural to let some of the digital state ‘bleed back’ into a physigram. It will also include theoretical issues, notably the problem of having a sufficiently rich semantic model to incorporate analogue input/output such as variable finger pressure. The latter connects back to earlier streams of work on status–event analysis.

This chapter presents an approach for the description and implementation of adaptable user interfaces based on reconfigurable formal user interface models. These models are (partially) defined as reference nets, a special type of Petri nets. The reconfiguration approach is based on category theory, specifically on the double pushout approach, a formalism for the rewriting of graphs. In contrast to the related single pushout approach, the double pushout approach allows the definition of reconfiguration rules that assure deterministic results gained from the rewriting process. The double pushout approach is extended to rewrite colored (inscribed) Petri nets in two steps: first, it has already been extended to basic Petri nets and second, the rewriting of inscriptions has been added to the approach in previous work of the author. By means of a case study, this approach is presented for the interactive reconfiguration of a given user interface model that uses a visual editor. This visual editor is equipped with an XML-based rewriting component implemented in the UIEditor tool, which has been introduced as a creation and execution tool for FILL-based user interface models in Chap. 5. This chapter is concluded with a discussion of limitations and a set of future work aspects, which mainly address the rule generation and its application to broader use cases.

This chapter is concerned with the problem of learning how to interact safely with complex automated systems. With large systems, human–machine interaction errors like automation surprises are more likely to happen. Full-control mental models are formal system abstractions embedding the required information to completely control a system and avoid interaction surprises. They represent the internal system understanding that should be achieved by perfect operators. However, this concept provides no information about how operators should reach that level of competence. This work investigates the problem of splitting the teaching of full-control mental models into smaller independent learning units. These units each allow to control a subset of the system and can be learned incrementally to control more and more features of the system. This chapter explains how to formalize the learning process based on an operator that merges mental models. On that basis, we show how to generate a set of learning units with the required properties.

Interactive software, systems and devices are typically designed for a specific (set of) purpose(s) and the design process used ensures that they will perform satisfactorily when used as specified. In many cases, users will use these systems in unintended and unexpected ways where it seems appropriate, which can lead to problems as the differing usage situations have unintended effects on use. We have previously introduced a method of combining formal models of interactive systems with models of usage scenarios to allow reasoning about the effects that this unintended use may have. We now extend this approach to consider how such models might be used when considering deliberately extending the usage scenarios of existing interactive systems to support other activities, for example in emergency situations. This chapter explores a methodology to identify the effect of properties of emergency scenarios on the interactivity of interactive systems and devices. This then enables us to consider when, and how, we might utilise such devices in such emergencies.

The enhanced operator function model (EOFM) is a task analytic modeling formalism that allows human behavior to be included in larger formal system models to support the formal verification of human interactive systems. EOFM is an expressive formalism that captures the behavior of individual humans or, with the EOFM with communications (EOFMC) extension, teams of humans as a collection of tasks, each composed representing a hierarchy of activities and actions. Further, EOFM has a formal semantics and associated translator that allow its represented behavior to be automatically translated into a model checking formalism for use in larger system verification. EOFM supports a number of features that enable analysts to use model checking to investigate human-automation and human-human interaction. Translator variants support the development of different task models with methods for accounting for erroneous human behaviors and miscommunications, the creation of specification properties, and the automated design of human-machine interfaces. This chapter provides an overview of EOFM, its language, its formal semantics and translation, and analysis features. It addresses the different ways that EOFM has been used to evaluate human behavior in human-interactive systems. We demonstrate some of the capabilities of EOFM by using it to evaluate the air traffic control case study. Finally, we discuss future directions of EOFM and its supported analyses.

This chapter explores a layered approach to the analysis of the Nuclear Power Plant Control System described in Chap. 4. A model is specified to allow the analysis of use-centred properties based on generic templates. User interface properties include the visibility of state attributes, the clarity of the mode structure and the ease with which an action can be recovered from. Property templates are used as heuristics to ease the construction of requirements for the control system interface.

Several modern safety-critical environments involve multiple humans interacting not only with automation, but also between themselves in complex ways. For example, in handling the National Airspace, we have moved from the traditional single controller sitting in front of a display to multiple controllers interacting with their individual display, possibly each other’s displays, and other more advanced automated systems. To evaluate safety in such contexts, it is imperative to include the role of one or multiple human operators in our analysis, as well as focus on properties of human automation interactions. This chapter discusses two novel frameworks developed at NASA for the design and analysis of human–machine interaction problems. The first framework supports modeling and analysis of automated systems from the point of view of their human operators and supports the specification and verification of HMI-specific properties such as mode confusion, controllability, or whether operator tasks are compatible with a particular system. The second framework captures the complexity of modern HMI systems by taking a multi-agent approach to modeling and analyzing multiple human agents interacting with each other as well as with automation.

Model-driven engineering (MDE) is an important enabler in the development of complex, reactive, often real-time, and software-intensive systems, as it shifts the level of specification from computing concepts (the “how”) to conceptual models or abstractions in the problem domain (the “what”). Domain-specific modelling (DSM) in particular allows to specify these models in a domain-specific modelling language (DSML), using concepts and notations of a specific domain. It allows the use of a custom visual syntax which is closer to the problem domain and therefore more intuitive. Models created in DSMLs are used, among others, for simulation, (formal) analysis, documentation, and code synthesis for different platforms. The goal is to enable domain experts, such as a power plant engineer, to develop, to understand, and to verify models more easily, without having to use concepts outside of their own domain. The first step in the DSM approach when modelling in a new domain is, after a domain analysis, creating an appropriate DSML. In this chapter, we give an introduction to DSML engineering and show how it can be used to develop a human–computer interaction interface. A DSML is fully defined by its syntax and semantics. The syntax consists of (i) the abstract syntax, defining the DSML constructs and their allowed combinations, captured in a metamodel, and (ii) the concrete syntax, specifying the visual representation of the different constructs. The semantics defines the meaning of models created in the domain. In this chapter, we show how two types of semantics (operational and translational) can be modelled using model transformations. Operational semantics gives meaning to the modelling language by continuously updating the model’s state, effectively building a simulator. Translational semantics defines mappings of models in one language onto models in a language with known semantics. This enables the automatic construction of behavioural models, as well as models for verification. The former can be used for automated code synthesis (leading to a running application), whereas the latter leads to model checking. We choose to specify properties for model checking using the ProMoBox approach, which allows the modelling of properties in a syntax similar to the original DSML. A major advantage of this approach is that the modeller specifies both requirements (in the form of properties) and design models in a familiar notation. The properties modelled in this domain-specific syntax are verified by mapping them to lower-level languages, such as Promela, and results are mapped back to the domain-specific level. To illustrate the approach, we create a DSML for modelling the human–computer interaction interface of a nuclear power plant.

During early phases of the development of an interactive system, future system properties are identified (through interaction with end-users, e.g., in the brainstorming and prototyping phases of the development process, or by requirements provided by other stakeholders) imposing requirements on the final system. Some of these properties rely on informal aspects of the system (e.g. satisfaction of users) and can be checked by questionnaires, while others require the use of verification techniques over formal models (e.g. reinitializability) or validation techniques over the application (e.g. requirements fit). Such properties may be specific to the application under development or generic to a class of applications, but in all cases verification and validation tools are usually required for checking them. The usability of these tools has a significant impact on the validation and verification (V&V) phases which usually remain perceived as very resource consuming. This chapter proposes a user–centred view on the use of formal methods, especially on the use of formal modelling tools during the development process of an interactive system. We propose to apply Norman’s action theory to the engineer tasks of formal modelling in order to analyse how modelling tools impact the following engineer activities: model editing, model verification and model validation. The CIRCUS Integrated Development Environment serves as an illustrative example to exemplify how engineer tasks may be impacted by modelling tools features.

Model-based approaches aim to support designers and developers through the use of logical representations able to highlight important aspects. In this chapter, we present a set of tools for task and user interface modelling useful for supporting the design and development of interactive applications. Such tools can be used separately or in an integrated manner within different types of development processes of various types of interactive applications. This tool suite is publicly available and, as such, can be exploited in real-world case studies and university teaching.

This chapter shows how flexible systems of user interfaces with an underlying formal model can be created by learning from the success story of apps on mobile devices and leveraging the concept of business process modelling. It is shown how these multi-app user interfaces are modelled and how they can be transformed into Petri nets in order to apply existing formal analysis methods. The created user interfaces are called App-Ensembles and resemble interactive systems comprised of self-contained apps that are connected in a purposeful manner via navigation links and data channels. A formal language for modelling these App-Ensembles is introduced (AOF-L). The graphical modelling elements are taken exclusively from BPMN 2.0 (Business Process Model and Notation). The underlying notation is formalized using an OWL 2 ontology. It is shown how App-Ensembles can be easily integrated into existing classical business process models. Two use cases illustrate the utility of App-Ensembles and the practicality of the modelling approach. This chapter demonstrates that it is useful to combine a semi-formal graphical notation with a strictly formal mathematical model. Strengths of the approach include the ability to run reasoning algorithms on the model, to query the model using languages such as SPARQL, and to perform a formal verification regarding contradictions and BPMN compliance.

Formal methods provide support for validation and verification of interactive systems by means of complete and unambiguous description of the envisioned system. Used in the early stages of the development process, they allow detecting and correcting development faults at design and development time. However, events that are beyond the envelope of the formal description may occur and trigger unexpected behaviours in the system at execution time (inconsistent from the formally specified system) resulting in failures. Sources of such interactive system failures can be permanent or transient hardware failures, due to, e.g. natural faults triggered by alpha particles from radioactive contaminants in the chips or neutrons from cosmic radiation. This chapter first presents a systematic identification of the faults that can be introduced in the system during both at development and operations time and how formal methods can be used in such context. To exemplify such usage of formal methods, we present their use to describe software architecture and self-checking components to address these faults in the context of interactive systems. As those faults are more likely to occur in the high atmosphere, the proposed solutions are illustrated using an interactive application within the field of interactive cockpits. This application allows us to demonstrate the use of the concepts and their application for WIMP interactive systems (such as the ones of the nuclear case study of the book).