The Specification and Analysis of Use Properties of a Nuclear Control System

Abstract

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.

The original version of the book was revised: For detailed information please see Erratum. The erratum to the book is available at 10.1007/978-3-319-51838_21

An erratum to this chapter can be found at http://dx.doi.org/10.1007/978-3-319-51838-1_21

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Formal modelling can offer substantial benefits when developing an interactive system. It enables systematic clarification of assumptions made about a design and supports verification that specified requirements have been met. This paper considers the nuclear power plant control system described in Chap. 4. The use cases introduced in the book offer slightly different perspectives that might suggest different approaches to analysis. Broadly, analysis approaches may be classified as task-orientated or task-based on the characteristics of the interface. In the first category, there are informal approaches, for example Cognitive Walkthrough (Polson et al. 1992), and formal approaches such as those of Bolton et al. (2012). These approaches are concerned with the representation of the intended task and then to analyse the system that is intended to perform the task. In the second category, analysis may be based on the characteristics of the interface (for example, Heuristic Evaluation Nielsen and Molich (1990) and formal approaches such as those of Campos and Harrison (2009). These approaches focus on, for example, the visibility or perceivability of key attributes of the device and analyse the properties of the supported actions (e.g. their predictability or undoability). The approach taken in this paper supports both styles of analysis. In the case of the task approach, the focus is on the constraints that determine the activities that the user performs, rather than focusing on prescribed normative behaviours. Constraints include the visibility of information (e.g. function key displays) that help the user to decide what action to be taken next.

A modelling approach based on the layers of specification is designed to unify these two approaches to analysis, with the aim of maintaining the integrity of the specification. Analysis of the interactive system is facilitated by the use of property templates.

This chapter is organised as follows: Sect. 14.2 describes the features of the example that are relevant to illustrating the analysis. Section 14.3 discusses the structure of the model that describes the interactive behaviour of the system. Section 14.4 describes the tools, including the set of property templates that are used to drive the analysis. Section 14.5 details the model of the example and describes the process of instantiating the property templates to be theorems over the model. Finally, we describe related work (Sect. 14.6) and conclusions (Sect. 14.7).

2 The Use Case

In the present example, two analytic perspectives are taken.

• How well does the interface support operating procedures¹ developed to help the controller start up or close down the system?

• Is the operator able to monitor and make appropriate adjustments to the process? Is there sufficient information for operators to understand what is happening and are suitable actions visible and available?

These two perspectives require different styles of analysis. The first is concerned with how effectively the display, and the actions it supports, can be invoked as required by an operator who is following the start-up and close-down operating procedures. The second is concerned with the display, the graphics, the status display, the sliders, the enabled actions and how these change the display and reflect the state of the underlying process. Whatever the level of analysis of the user interface, it is important to understand the interface to the underlying system. The interface of the system should aid understanding by making parts of the underlying process visible to the user; producing visible feedback to enable the operators to assess what has been done. Interactive systems of any complexity have a common characteristic that some elements of the state of the system are perceivable (e.g. visible or audible) and that user actions transform the state (Duke and Harrison 1993). Furthermore, not all actions are permitted all of the time, and the behaviour of actions can depend on distinguished state attributes called modes, see Gow et al. (2006) for further discussion. The modes in this case determine, for example, whether the control rods are being controlled automatically or manually. Modes also determine specific interactions related to the behaviour of the mouse: its position and whether the mouse button is pressed or not. For example, when the mouse button is pressed and the cursor position coincides with a slider on the screen, and the slider is not in automatic mode, then dragging the cursor moves the position of the slider thus changing the relevant behaviour of the component of the process that it represents.

Users have difficulty in understanding the progress of a system when the elements of the state of the system that are relevant to that understanding are not visible in a form that makes sense to them. At the same time, confusion can arise when actions relevant to the current activity are, apparently or actually, disabled by the system, or when the actions have an unexpected or inconsistent effect with respect to the users’ knowledge and experiences of the system. Actions and states are therefore elemental in understanding interactive behaviour. Modes are also important. It is unusual that an interactive system is so simple that actions always have the same effect.

To achieve the goals and activities required of the users, most interactive systems are designed more or less effectively to ensure that the information required (we call them information resources (Campos et al. 2014)) is made explicitly available, and in a form that can be easily understood by the users. A role of a model of the interactive system is therefore to make these information resources explicit, so that assumptions about the constraints they impose may be analysed.

3 Structure of the Models

It is important to distinguish between the interactive systems and the components of interactive systems. Interactive systems are socio-technical systems involving people, devices and artefacts (desks, pieces of paper, pens, tablets and so on). The primary focus of the modelling approach illustrated here is on the interactive devices that are the components of the interactive system. The presented property templates capture aspects of the system that can facilitate device–user interaction.

3.1 The Interface Specification

The specification of an interactive system includes a definition of the set of actions, including user actions, that are possible within them. These actions affect and are affected by the state of the system. The behaviour of actions is often determined by the mode of the device. The proposed model of the interactive system also makes explicit the information resources that are assumed to aid the use of the system. Assumptions about the activities for which the system is designed are also made explicit. An action is a transformation supported directly by the interface. An activity is a means to achieve some work goal, for example achieving a steady state of the system with maximum voltage.

The interface specification describes what the display shows and captures the effects of user-level actions. The display will show some features of the state of the reactor, and these features may be encoded as part of the interface. It will also show the user actions that are translated into actions within the reactor. The specification includes display widgets, showing simple status information. These include widgets labelled $RKS$, $RKT$, $KNT$, $TBN$, $WP1$, $WP2$, $CP$, $AU$. These displays are associated with a range of colours indicating status. The display also shows actions associated with the valves: $SV1$, $SV2$, $WV1$, $WV2$ and sliders that change the position of the control rods and the status of the valves.

Analysis of an interactive device is then concerned with proving that relevant feedback is given on completing an action, that relevant information is available before an action is carried out, that it is possible to recover from an action in specified circumstances, and that it is always possible simply to step to some home mode whatever the state of the device and that actions can be completed consistently.

3.2 Structuring Specifications

The model of the interactive system is structured into four layers. The first layer simply specifies the constants and types used throughout the specification. It includes types related to the devices involved and the entities that are in the broader system. For example, in the case of the reactor these types would include notions such as $pressure$, $volume$ and $temperature$. There would also be types associated with pumps and valves. Constants would include maximum and minimum values required to trigger error events in certain situations.

The second layer describes assumptions about the underlying process, managed or controlled by the devices that are required to enable the analysis of the characteristics of the interactive device. This layer is often reused across families of device models when exploring the effects of differing user interfaces. For example, in Harrison et al. (2015b), different brands of IV infusion devices share the same pump layer. The process layer, in the case of the nuclear process, is the simplest model of the nuclear reactor that will allow a proper consideration of interactive behaviour of the control system. A specification of the underlying reactor, describing the details of the relation between reactor core and turbine, would include attributes defining water level and pressure for each. The specification at this level would also define the characteristics of the pumps and valves. The pumps would be associated with rates per minute, and the valves would be on or off. A number of actions will be specified at this level. An action $tick$ is used to represent the interval of one minute and update the attributes to describe the evolving process. There will be further actions switching pumps on and off, opening and closing valves and changing the value of flow in the pump, for example.

The third layer describes the interface to the interactive device or system. This model uses the process description described in the second layer. It makes those aspects of the state that are visible explicit through the interface. It describes the user actions, including how the sliders or buttons or other display widgets work. The third layer of the specification of the nuclear power plant control user interface specifies how the user sets, controls and views the operation of the reactor. It is specific to this particular interface, whereas the reactor specification (given in the second layer) may be more generic and therefore used with several user interfaces. It provides an opportunity to explore the variety of user interfaces that may be appropriate for supporting human–machine interactions necessary to control the reactor.

The fourth, and final, layer makes explicit the information resources that are required for different actions in different circumstances. It captures constraints on action based on the goals and activities that the user achieves (Campos et al. 2014). This layer contains an interactive system view. The activities and actions are “resourced” by user interfaces for devices that are used in the interactive system or, indeed, any other source of relevant information that is present within the interactive system. It adds attributes that are not captured by the devices and includes (meta-)actions that describe activities that may involve the actions of the interactive devices. An example of this fourth layer used in a different context can be found in Masci et al. (2012).

The models to be considered have some or all of the following characteristics depending on layer.

• A set of actions , where S is a set of states. Actions are partial functions. They are made total by including a value “undefined” ($\bot$). A permission function per takes an action and determines whether it is defined for a value in its domain $per : A \rightarrow (S \rightarrow T)$ such that $per(a)(s) = true$ if $a(s) \ne \bot$.

• A state is a set of attributes. Functions of the form $filter : S \rightarrow C$, where C is an attribute will often be used to extract an attribute of the state. The attribute is itself a domain, for example temperature or pressure. Similarly, some elements of the state are part of the interface and are perceivable. $p\_ filter$ will often be used to describe the filter that extracts the corresponding visual attribute to the value extracted by $filter$. Alternatively, a predicate $vis\_filter : C \rightarrow T$ may be used to assert that the value of the filtered attribute is visible.

• The function mode is a particular form of $filter$, namely $mode : S \rightarrow MS$. It extracts the modes of the model, where MS is an attribute that ranges over a set of modes. In the example, one set of modes relates to the types of variable being entered through number entry.

4 Tool Support

Two approaches to specification and proof are feasible for the kinds of model described here: model checking and theorem proving. The theorem-proving approach is appropriate here because a potentially important feature of the analysis, not discussed further in this short chapter, concerns the mechanisms for number entry. Since the domain of numbers is relatively large, proof using model checking can result in analyses of very large models that can be intractable. Interested readers are redirected to Harrison et al. (2015a) for an application where the layered approach described in this paper is used in an example involving number entry.

4.1 Representing and Proving the Model

The analysis is performed using the Prototype Verification System (PVS) (Shankar et al. 1999), an automated theorem prover developed at SRI. The system combines a specification language based on higher-order logic with an interactive prover. PVS has been used extensively in several application domains. The higher-order logic supports the usual basic types such as boolean, integer and real. New types can be introduced either in a declarative form (these types are called uninterpreted) or through type constructors. Examples of type constructors used in the present specification are function and record types. Function types are denoted [D -> R], where D is the domain type and R is the range type. Predicates are Boolean-valued functions. Record types are defined by listing the field names and their types between square brackets and hash symbols. Predicate subtyping is a language mechanism used for restricting the domain of a type by using a predicate. An example of a subtype is {x:A | P(x)}, which introduces a new type as the subset of those elements of type A that satisfy the predicate P. The notation (P) is an abbreviation of the subtype expression above. Predicate subtyping is useful for specifying partial functions. This notion is used to restrict actions to those that are permitted explicitly by the permission predicates mentioned when describing the models in general terms. Specifications in PVS are expressed as a collection of theories, which consist of declarations of names for types and constants, and expressions associated with those names. Theories can be parametrised with types and constants, and can use declarations of other theories by importing them. The prelude is a standard library automatically imported by PVS. It contains a large number of useful definitions and proved facts for types, including common base types such as Booleans (boolean) and numbers (e.g. nat, integer and real), functions, sets and lists.

The specification of the models takes a standard form as described in Sect. 14.3.2. A model consists of a set of actions and a set of permissions that capture when the actions can occur.

For each action, there is a predicate:

that indicates whether the action is permitted.

4.2 Property Templates

Property templates are generic mathematical formulae designed to help developers to construct theorems appropriate to the analysis of user interface features. The aim is to make these programmable devices more predictable and easy to use. The particular set of templates considered here is derived from Campos and Harrison (2008). A formulation of these properties based on actions, states and modes is presented, along with a brief summary of the use-related concerns captured by the template. There are two types of property: properties that relate states where a specific action has taken place, and properties that relate a state to any state that can be reached by any action from that state. The relation $transit : S \times S$ relates states that can be reached by any action. For a particular model, $transit$ will be instantiated to connect states by the actions provided by the system.

Completeness. This template checks that the interactive system allows the user to reach significant states in one (or a few steps). For example, being able to reach “home” from any device screen in one step is a completeness property. The completeness template asserts that a user action will transform any state that satisfies a predicate $guard : S \rightarrow T$ into another state that satisfies a predicate $goal : S \rightarrow T$. The guard is introduced to make it possible to exclude states that may not be relevant.

Feedback. When certain important actions are taken, a user needs to be aware of whether the resulting device status is appropriate or problematic (AAMI 2010). Feedback breaks down into state feedback, requiring that a change in the state (usually specific attributes of the state rather than the whole state) is visible to the user, and action feedback, requiring that an action always has an effect that is visible to the user.

In the case of state feedback, the guard may be used, for example, to restrict the analysis to ensure that the device or system is considered to be in the same mode as a result of the state transition. Variants of the feedback properties will also be used that assume separate visible attributes are not specified in the model. Instead, a relevant predicate $vis\_filter : S \rightarrow T$ is linked to $filter : S \rightarrow A$. $vis\_filter (s)$ is true for $s \in S$ if $filter (s)$ is visible. Both these variants will be used in Sect. 14.5. The choice is based on how the model is constructed.  

Consistency. Users quickly develop a mental model that embodies their expectations of how to interact with a user interface. Because of this, the overall structure of a user interface should be consistent in its layout, screen structure, navigation, terminology and control elements (AAMI 2010). The consistency template is formulated as a property of a group of actions $A_c \subseteq \wp (S \rightarrow S)$, or it may be the same action under different modes, requiring that all actions in the group have similar effects on specific state attributes selected using a filter. The relation $consistent$ connects a filtered state, before an action occurs, with a filtered state after the action. The description of the filters and the $consistent$ relation capture the consistency across states and across actions.

Consistency is a property of, for example, the cursor move actions when the mouse button is pressed. It may be used to prove that while the button is down, the move actions will continue to be interpreted in the relevant mode.  

Reversibility. Users may perform incorrect actions, and the device needs to provide them with functions that allow them to recover by reversing the effect of the incorrect action. The reversibility template is formulated using a $guard : S \rightarrow T$ and a $filter : S \rightarrow FS$, which extracts a set of focus attributes of the state:

Some properties simply maintain invariants for any state. Examples of such properties are visibility and universality. There are alternative formulations of these two properties. The first asserts that a predicate applied to one filtered value is true if and only if an appropriate predicate is true of the other filtered value. The second asserts that a filtering of the first value is equal to the determined filter of the second value. These two formulations are appropriate in different circumstances as will be briefly explored in Sect. 14.5. The style of interface described in this case study lends itself particularly to the second option.  

Visibility. This property describes an invariant relation between a state variable that is not necessarily visible to the user and a user interface value that is visible to the user. Examples of these properties are as follows: the current operational mode is always unambiguously displayed; a slider that shows the position of the control rods always shows the actual position of the control rods in the underlying process; the colour of the status attribute describes general characteristics of the value of the attribute. $filter (s)$ and $p\_ filter (s)$ are the filters for the attribute and its perceivable counterpart.

Universality. Universality generalises the visibility property requiring that given two filters of the state: $filter1$ and $filter2$, there are predicates on the filters that are equivalently true.

5 Modelling the Nuclear Power Plant Control User Interface

The fragments of specification described in this section were taken from the description to be found in Chap. 4 and a simulator (see the simulator description and code²) that includes a version of an interface to the nuclear controller. A more thorough description of the user interface was required than was available in the use case material to do a thorough analysis using the property templates. The analysis of IV infusion pumps described in Harrison et al. (2015a) illustrates the more thorough approach. If such a detailed description had been available, then it could be further explored using PVSio-web (Masci et al. 2015) to ensure that assumptions made seem realistic and to demonstrate where properties of the system fail to be true. This would provide confidence that the behaviour of the interface as specified conforms with the expected user experience. The issue of validation of the model of the system is explored in more detail in Harrison et al. (2014). The introduction to the use case contains the following paragraph.

The operation of a nuclear power plant includes the full manual or partially manual starting and shutdown of the reactor, adjusting the produced amount of electrical energy, changing the degree of automation by activating or deactivating the automated steering of certain elements of the plant, and the handling of exceptional circumstances. In case of the latter, the reactor operator primarily observes the process because the safety system of today’s reactors suspends the operator step by step from the control of the reactor to return the system back to a safe state.

The interface involves schematics of the process, the availability of actions as buttons and graphical indications of key parameters, for example temperature and levels. The specification of the model can be layered using the levels described in Sect. 14.3 as follows.

5.1 Types and Constants

This contains generic definitions that will be used throughout other layers of the theory. It defines types such as:

The pump attribute is defined to have a speed of flow and to be either on or off. There are several pumps with the same characteristics as defined by the following function type:

This type definition allows the definition of multiple pumps indexed by an integer (vp_number). This type relates to the process layer. The following types are used in the interface layer.

The type cursor_type specifies the type of the cursor on the controller display. It is tied to the physical position of the mouse. The details of how this is done will not be described here. It will be assumed that there is a function mouse that extracts the current cursor position of the mouse. The slider which is also found in the interface layer is specified as follows:

The slider type specifies the current x-position of the cursor when the slider has been selected (xpos). It specifies the left and right limits of the slider (lx and rx) and the y-position of the slider (ypos). As a simplification for the illustration, the slider is assumed to have no depth. In the real system, sliders also have a depth and therefore the y-coordinates will also have boundaries.

5.2 The Process Layer

The process layer describes sufficient details of the underlying process of the nuclear reactor to provide an adequate underpinning for the interface. The interface captures, for example, those situations where the process automates and therefore removes the ability of the operator to change settings manually. The model describes the ongoing process in terms of a single action $tick$ that updates the attributes of the pump state as time progresses.

This fragment of specification illustrates the form of the process layer. The action that is described is tick. Its function is to update the process state (defined by type npp) attributes. Some of these attributes can be changed by actions that can be invoked by the operator (e.g. the two valves wv(1) and wv(2)), while others are internal to the process (e.g. poi_reactor and bw).

Further actions determine transformations of the process that can be invoked directly through the user interface. For example control_rods is an action that updates the process state to its new position. This position is determined by where the cursor is, as represented in the control rods slider, when the rod’s position is not under automatic control.

5.3 The Interface Layer

The interface layer describes those attributes of the state of the process that are visible to the user and the actions that can be performed by the operator. The interface presents the state of the process to provide the operator with situation awareness. There are also displayed attributes that indicate sliders and buttons that can be used by the operator to control aspects of the process.

An illustration of the layer considers the mouse actions: $move$, $click$ and $release$. The actions $move$ and $release$ have effects that depend on the modes that the interface is in. The action $click$ changes the mode. The change in mode depends on the position of the cursor. Two sets of modes are specified. One set relates to the sliders on the display (slider_mode), while the other relates to the actions that are offered by the display (action). When the mouse has not been clicked or is over a space in the display that does not correspond to a slider or an action, then slider_mode = nulslimo and action = null_action. When the mouse is clicked, then a boolean attribute clicked is true. The permission that allows click to be an available action is as follows:

$click$ is an action that:

• 1. assigns a value to slider mode if the cursor is at the appropriate y-coordinate (ypos) and in the relevant range of x-coordinates for the slider (in reality, there may also be a range of y-coordinates) otherwise it sets the slider mode to the relevant null value.

• 2. assigns a value to action, the action mode, if the x- and y-coordinates are within the relevant range of an action button and the action is enabled. If the cursor is outside the defined button ranges, then the action is set to null.

Fragments of the action specification are given below. They show the effect when the mouse is within the slider for the pump $wp1$ and the effect when the mouse is in the area of the action button that sets control rods to automatic mode.

Different actions and therefore modes are specified depending on whether the pumps or the control rods are in automatic mode. Moving the cursor has different significance, depending on whether the mouse is clicked or not. When the mouse is clicked outside the sensitive areas or when the mouse button is not depressed, then the cursor coordinates only are changed. If the mouse is clicked within the space, then the appropriate mode is taken. If the mode is related to a slider, then the cursor on the slider is moved.

$release$ has the effect of invoking actions in the process layer if the slider mode is non-null and also the action is non-null. Hence, for example, if slidermode = wp1s, that is the flow rate of $wp1$ is being changed, then a function is invoked that changes the flow rate of the pump. This function is defined as part of the interface layer, but it invokes the relevant function in the process layer.

Aspects of the status of the process are captured in indicators (e.g. RKS, RKT). The colours of the indicators are linked to the states of the underlying reactor (modelled in the second layer), for example if the value of a process attribute is outside specified bounds then the indicator shows the colour red. The model also specifies that the user can perform open/close actions on valves by highlighting the available option in the display.

5.4 Proving Properties of the Interface Layer

Two examples will be used to illustrate how the template properties are instantiated in the interface layer. The first example is concerned with the visibility of different aspects of the underlying process, while the second is concerned with the consistency when releasing the mouse button. The concern in the first example is with the CP pump as it transports water through the cooling pipes in the condenser. A display, specified by the attribute that is part of the interaction mode, $status\_cp$ simply indicates whether the pump flow is normal (green) or out of bounds (red). The property to prove is that the display shows these colours correctly. This can be proved by instantiating the visibility property template (Eq. 6 in Sect. 14.4.2).

This theorem contains an induction based on the accessible states. The initial state is specified by the predicate init_state. The visibility property to be proved is:

The filter predicates are specified as follows:

Similar properties can be proved of a range of display features relating to, for example, the status of the process attributes; whether the pumps and control rods are in automatic mode; the values of pump flows and the position of control rods; whether it is possible to switch pumps on or off.

To illustrate the consistency property (Eq. 4 in Sect. 14.4.2), the $release$ action is considered in relation to the sliders. The theorem instantiates the template properties indicated in the formulation of the property. The guard and consistency predicates are specified over all the slider modes. We therefore slightly modify the formulation. The aim is to prove the property:

There are four modes to be considered in $MS$, namely wp1s, wp2s, cps and crs. The guard checks that the mouse cursor is in the relevant region of the display depending on mode that release is permitted and that the particular function is not currently automated.

The predicate x_in_area checks that the cursor is in a relevant position in relation to the slider.

The consistency relation is distributed across these modes as follows:

The relation $consistent$ is equally distributed over the modes; the filter_pre indicates what the new state of the process should be, that is for each mode a function in the underling process should be invoked that updates the relevant state attribute.

and filter_post(st) = release(st). Consistency relates the change in state filter_post(st) to the state before the action in which the mode determined action takes place in the process layer. It determines that $release$ always invokes the mode-relevant process action (changing pump flow or control rod position). The instantiated consistency theorem is an induction on the actions of the interaction model.

Attempting to prove this theorem identifies an issue with the simulator display. The four sliders occupy the same x-space. The sliders are implemented so that the slider will continue to be dragged across even when the y-coordinate is not in the slider area relating to the mode. It would be imagined that this characteristic would not be a feature of the real control room display.

5.5 The Activity Layer

The purpose of the activity layer is to specify assumptions about how the attributes specified in the interface layer, as well as other specified attributes that may be external, are used to carry out the intended activities of the system. It is clearly necessary to know what the activities are that will be performed by the controllers. Typically, this information would be gathered by observing existing processes, by interviewing controllers, or by developing scenarios with domain experts that relate to anticipated constraints in terms of new design concepts. The approach is described in more detail in Campos et al. (2014).

Given the limited information provided by the use case, it is difficult to develop and assess plausible assumptions. However, we do have operating procedures associated with starting up and closing down the reactor. This will be the information that provides the basis for sketches of the activity layer given here.

The aim of start-up is to bring output power to 700 MW (100% of possible output power) and to hold the water level in the reactor tank stable at 2100 mm. The operating procedure is as follows:

• 1. Open SV2

• 2. Set CP to 1600 u/min

• 3. Open WV1

• 4. Set WP1 to 200 u/min

• 5. Stabilise water level in the reactor tank at 2100 mm by pulling out the control rods

• 6. Open SV1

• 7. ...

The process of developing the activity model involves, for each step in the operating procedure, considering the information resources that are conjectured to enable the user to take the appropriate action in the interface. The action is resourced if information relevant to the use of the action is clear in the interface. The activity model also considers how the user is notified what the next action is to be performed. In the case of this fragment, it will be assumed that the written operating procedure will be used to decide the sequence. However, in other circumstances it should be considered whether the user will be allowed by the control system to change the order of the operating procedure and what the effect of such a change would be. The action OpenSV2 is expressed in the model as

The open valve action is generic to the valves supported by the interface and is made specific by the attribute action. It may be assumed that this action would be triggered if

• the openSV2 button area is enabled, that is it is highlighted: highlightosv2 = true. This should only be true if sv2_open = false, a property checked of the interface model.

• the cursor is within the osv2 area:

The resource layer specifies all the constraints based on assumptions about what triggers the actions supported by the interface as well as activities that are to be performed. When these assumptions have been specified, they can be used as additional constraints when proving theorems based on the templates. The resource layer makes it possible to prove whether the properties are true in circumstances that afford some measures of plausibility in relation to what users do.

Additional actions may be specified that characterise the activities performed by users. For example, consider the user activity $recover$, in contrast to the autonomous action that causes recovery. This activity would involve several actions before the goal of the activity is achieved. Information resources would help the operator to begin the activity. This means that the activity also has information resource constraints. For example, it would specify that “increasing pressure”, using the relevant action in the interface layer, would occur only if other actions had already been completed and the displayed tank, valve and pump parameters specified in the second layer were displayed (in the interface layer), indicating particular values.

Further activities include, for example, “monitor recovery”. This would be expressed as an action that describes the constraints on the operator when monitoring an autonomous recovery. The specification of the action would include the information resources that would be required in the monitoring process at different stages of the recovery and would specify the conditions in which any user actions would take place.

The value of expressing constraints in this way is that theorems that are instantiations of property patterns of Sect. 14.4.2 can be proved subject to the resource constraints. Properties can be considered that only relate to plausible interactions. This would be relevant if it was considered inappropriate to analyse properties across sequences of actions that would not plausibly occur. The implications of such an analysis are that an understanding of whether an action is plausible becomes more relevant, and this requires an understanding of the human factors of a situation. This topic is considered in more detail in Harrison et al. (2016). It can also be proved that, for the steps of the operating procedures, the constraints are satisfied.

6 Related Work

Models, of the type outlined, have been developed for other interactive systems using both model checking approach and theorem-proving approach (Masci et al. 2012; Harrison et al. 2014, 2015b; Campos et al. 2016). The advantage of model checking is that it is possible to explore, more readily, reachability properties as well as potential non-determinisms. The disadvantage is that the size of model is seriously limited. It is possible to explore the essential details of the control of the nuclear power plant using a model checking approach, but as soon as a realistic process model is used this becomes impossible. Making the model abstract enough, to make analysis feasible, would restrict what could be asked of the model. It would be more difficult to prove relevant properties.

Theorem proving allows analysis of larger models but properties may be more difficult to formulate and prove. In particular, while model checking allows simple formulations of reachability properties, these are difficult to specify using a theorem-proving approach. There is a trade-off to be made between the effort needed to develop a model amenable to verification and the effort needed to carry out the proofs. Typically, a theorem proving-based approach will gain advantage in the former, because of more expressive languages, and model checking in the latter, because of more automated analysis. In all the cases, how to identify and express the properties of interest is also an issue.

Design patterns and property templates have been extensively studied in engineering practices. Most of the effort, however, has been devoted to creating patterns and templates for the control part of a system, rather than for the human–machine interface. Vlissides et al. (1995) established a comprehensive set of standard design patterns for software components of a system. An example pattern is the abstract factory, which facilitates the creation of families of software objects (e.g. windows of a user interface). Another example is the adapter pattern, which converts the interface of software components to enable the integration of otherwise incompatible software components. These patterns are a de facto standard in the software engineering community, and they are widely adopted in engineering practices to solve common problems related to the realisation of software components. Konrad and Cheng (2002) discuss design patterns for the elements of embedded systems. An example pattern is the actuator–sensor pattern, providing a standard interface for sensors and actuators connected to the control unit of an embedded system. Similarly, Sorouri et al. (2012) present a design pattern for representing the control logic of an embedded system. Lavagno et al. (1999) introduced Models of computation (MoC) as design patterns for representing interactions between distributed system components. Recently, Steiner and Rushby (2011) have demonstrated how these MoC can be used in model-based development of systems, to represent in a uniform way different time synchronisation services executed within the system. These and similar activities are concerned with the design patterns for the control part of a system, as opposed to the human–machine interface—e.g. problems like how to correctly design the behaviour of data entry software in human–machine interfaces are out of scope.

Various researchers have introduced design patterns for the analysis of complex systems. For example, in Li et al. (2014), verification patterns are introduced that can be used for the analysis of safety interlock mechanisms in interoperable medical devices. Although they use the patterns to analyse use-related properties such as “When the laser scalpel emits laser, the patient’s trachea oxygen level must not exceed a threshold $\varTheta _{O_2}$”, the aim of their patterns is to facilitate the introduction of a model checker in the actual implementation of the safety interlock, rather than defining property templates for the analysis of use-related aspects of the safety interlock. Other similar work, e.g. Tan et al. (2015), King et al. (2009), Larson et al. (2012), also introduce design patterns for the verification of safety interlocks, but the focus of the patterns is again on translating verified design models into a concrete implementation—in Tan et al. (2015), for example—the design patterns are developed for the automatic translation of hybrid automata models of a safety interlock into a concrete implementation.

Proving requirements similar to the properties produced from the templates of this paper has been the focus of previous work. For example, a mature set of tools has been developed using SCR (Heitmeyer et al. 1998). Their approach uses a tabular notation to describe requirements which makes the technique relatively acceptable to developers. Combining simulation with model checking has also been a focus, in other work, for example Gelman et al. (2013). Recent work concerned with simulations of PVS specifications provides valuable support to this complementarity (Masci et al. 2013). Had the specification been developed as part of a design process, then a tool such as Event B (Abrial 2010) might have been used. In such an approach, an initial model is first developed that specifies the device characteristics and incorporates the safety requirements. This model is gradually refined using details about how specific functionalities are implemented.

In our previous work, we have introduced modelling patterns for decomposing interactive (human–machine) system models into a set of layers to facilitate models reuse (Harrison et al. 2015b). Bowen and Reeves (2015), who are concerned with design patterns for user interfaces, complements our work on modelling patterns. They have introduced four modelling patterns: the callback pattern, representing the behaviour of confirmation dialogues used to confirm user operations; the binary choice pattern, representing the behaviour of input dialogues used to acquire data from the user; the iterator pattern, representing the behaviour of parametric user interface widgets that share the same behaviour but have a different value parameter, such as the numeric entry keys 0–9; and the update pattern, for representing the behaviour of a numeric display.

7 Discussion and Conclusions

Two approaches to specification and proof are possible with the considered examples: model checking and theorem proving. Model checking is the more intuitive of the two approaches. Languages such as Modal Action Logic with interactors (MAL) (Campos 2008) express state transition behaviour in a way that is more acceptable to non-experts. The problem with model checking is that state explosion can compromise the tractability of the model so that properties to be proved are not feasible. Model checking, hence, is more convenient for analysing high-level behaviour, for example when checking the modal behaviour of the user interface. Theorem proving, while being more complex to apply, provides more expressive power. This makes it more suitable when verifying properties requires a high level of detail, such as those related to a number entry system, because the domain of numbers is relatively large.

To employ the strength of the two approaches, simple rules can be used to translate from the MAL model to the PVS model that is used for theorem proving. Actions are modelled as state transformations, and permissions that are used in MAL to specify when an action is permitted are described as predicates. The details of the specification carefully reflects its MAL equivalent. This enables us to move between the notations and verification tools, choosing the more appropriate tool for the verification goals at hand.

One aspect that has not been discussed in this chapter is the analysis and interpretation of verification results. Interpretation may be facilitated through the animation of the formal models to create prototypes of the modelled interfaces. These prototypes make it easier to discuss the results of verification with stakeholders. Such prototypes can be used either to replay traces produced by a model checker or interactively to both discuss the findings of the verification or help identify relevant features of the system that should be addressed by formal analysis. This approach is described in Masci et al. (2014).