Balancing the formal and the informal in user-centred design

Interacting with Computers, Vol. 33 No. 1, 2021 © The Author(s) 2021. Published by Oxford University Press on behalf of The British Computer Society. This is an Open Access article distributed under the terms of the Creative Commons Attribution License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted reuse, distribution, and reproduction in any medium, provided the original work is properly cited. Advance Access publication on 21 April 2021 doi: 10.1093/iwcomp/iwab012 Balancing the Formal and the Informal in User-centred Design Michael D. Harrison1,*, Paolo Masci2and José Creissac Campos3,4 1School of Computing, Newcastle University, Urban Sciences Building, Newcastle upon Tyne, NE4 5TG, UK 2National Institute of Aerospace, 100 Exploration Way, Hampton, VA 23666, USA 3Department of Informatics, University of Minho, Campus de Gualtar, 4710-057 Braga, Portugal 4HASLab - High-Assurance Software Laboratory / INESC TEC, Campus de Gualtar, 4710-057 Braga, Portugal ∗Corresponding author: mic[email protected] This paper explores the role of formal methods as part of the user-centred design of interactive systems. An iterative process is described, developing prototypes incrementally, proving user-centred requirements while at the same time evaluating the prototypes that are executable forms of the developed models using ‘traditional’ techniques for user evaluation. A formal analysis complements user evaluations. This approach enriches user-centred design that typically focuses understanding on context and producing sketch designs. These sketches are often non-functional (e.g. paper) prototypes. They provide a means of exploring candidate design possibilities using techniques such as cooperative evaluation. This paper describes a further step in the process using formal analysis techniques. The use of formal methods provides a systematic approach to checking plausibility and consistency during early design stages, while at the same time enabling the generation of executable prototypes. The technique is illustrated through an example based on a pill dispenser. RESEARCH HIGHLIGHTS • The paper describes a user centred design process that integrates the use of formal models, theorem proving and prototypes based on the formal description and empirical analysis. • The process is illustrated with a realistic case study based on a pill dispenser device suitable for use in common areas in care homes or hospitals. Keywords: user-centred design; formal methods Handling Editor: Regina Bernhaupt Received 5 December 2019; Revised 20 May 2020; Accepted 10 March 2021 1. INTRODUCTION Traditional user-centred design approaches such as contextual design [Beyer & Holtzblatt, 1998] and scenario-based design [Carroll, 1995] focus on user tasks early and throughout the design process. They measure usability empirically and test and refine the design iteratively, based on results obtained through user evaluation sessions. The evaluations build on the use of scenarios and sketch designs. Scenarios capture typical or exceptional situations and tasks. Sketch designs represent possible design solutions that would improve the situation. They are often non-functional, for example it could be a simple PowerPoint presentation or a paper storyboard. Think-aloud techniques such as cooperative evaluation [Monk et al., 1993] are typically used to collect feedback necessary to assess the design and judge whether a further iteration would be appropriate. These usability methods are well understood and provide important insights about the context inwhich a device is used, as well as the needs of different users. In safety critical contexts, however, where guarantees about the interaction between users and systems are needed, Downloaded from https://academic.oup.com/iwc/article/33/1/55/6232199 by guest on 18 March 2024 56 M. D. Harrison et al. prototyping is not enough to provide the required level of assurance. Even if the prototype is detailed enough to capture all relevant aspects of the system, simple manual inspection does not provide the required level of analysis thoroughness. This paper advocates a complementary process in which each step of the user-centred design process uses the, by now, traditional approach of presenting the current version of the interface to users but, at the same time, also involves a formal analysis of the model that is developed alongside the design. Specific aspects of the approach will be illustrated using a concrete example based on an automated pill box for dispensing medication to patients at specific times. The initial sketch design of the pill box is introduced in Section 3, after the design process and the tools used to support the design process in this paper are introduced (in Section 2). The sketch design includes an explanation of the sketch prototype and how an executable formal model can be derived from the sketch. A requirement relating to the functionalities that should be available to different intended users (doctor, carer and pharmacist) is also discussed. An enhanced design is then presented that fills various gaps observed of the initial design (Section 4). The formal model associated with the enhanced design is mechanically checked against plausibility properties (Section 5)using lightweight formal methods based on simulation and testing. The enhanced design is validated with end users by integrating the same formal model in a realistic interactive prototype that can be effectively presented to end users and domain experts (Section 6). Formal verification of requirements of the model is then described (Section 7). Use-related requirements include the consistency of the actions offered by the enhanced design (Section 7.1), the reversibility of scrolling behaviour supported by designed scrolling actions (Section 7.2)and mutual exclusion of different user pathways (Section 7.3). The final sections present a discussion of comparable approaches (Section 8) and concluding remarks (Section 9). The formal aspects of two iterations of the user-centred design process are demonstrated for the illustrated design. This demonstrates a framework that may be used effectively for the design of use aspects of safety critical interactive systems. Contributions of the paper are the following: (i) a user-centred design process that integrates the use of formal models and empirical analysis and (ii) an application of the approach to a realistic case study based on a pill dispenser device. This paper is an extended version of Harrison et al. [2018]. The main extensions are as follows: an enriched description of the approach for integrating the formal analysis in standard user-centred design methods, an extended presentation of the requirements of the pill box device and a detailed illustration of the formal analysis carried out to verify use-related requirements of the pill box device. A similar approach was presented in Harrison et al. [2019b], where verification was used post hoc, to guarantee relevant risks had been considered in the design. While the approach is similar, the concern in this paper is different and complementary, as the approach is used to support the design process itself. 2. THE APPROACH Usability engineering usually assumes that part of design development involves a (possibly) iterative process in which designs are subject to some form of evaluation. In some cases, these design stages can involve non-functional prototypes, see for example Beyer & Holtzblatt [1998]. This paper argues that user-centred design can involve a formal stage. The design is modelled and the model is executed but at the same time properties are developed from user-centred design requirements developed with the participation of users. This may include usability heuristics, for example Nielsen & Molich [1990], and use-centred regulatory requirements, for example Masci et al. [2013]. The envisaged design process is as follows: Step 1: use-centred requirements. An initial set of usecentred requirements is developed through, for example, contextual enquiry. These requirements are typically formulated using natural language. At each iteration of the design process the requirements are validated or supplemented by further requirements relevant to the current state of the model. Step 2: executable formal model. A formal model is developed that captures the functionalities indicated in the requirements. The formal model is checked mechanically using lightweight formal methods based on simulation and testing. The aim of this step is to gain confidence that the specification satisfies basic properties, e.g. coverage of conditions. Step 3: validation of requirements. A mockup prototype is created that can be presented to end users and domain experts. The visual appearance of the mockup captures that of the final system. The behaviour of the mockup is driven by the executable formal model developed in Step 2. The mockup is evaluated with end users and domain experts. The main aim of this step is to validate requirements, i.e. make sure that developers are creating the right system. Requirements, model and mockup are modified as gaps and errors are found. This step iterates as necessary. Step 4: verification of requirements. Requirements are proved of the model using exhaustive formal methods approaches, e.g. model checking or theorem proving. The formal model is modified when verification attempts point out corner cases where requirements are not satisfied. Requirements may also be modified as gaps and errors are found through the formal analysis. End users are brought back into the loop when iterating the design process (see also description of Step 5) Interacting with Computers, Vol. 33 No. 1, 2021 Downloaded from https://academic.oup.com/iwc/article/33/1/55/6232199 by guest on 18 March 2024 Balancing the Formal and the Informal 57 Step 5: iterating the system design. Requirements and mockup are iterated starting again at Step 1. Step 2 brings end users and domain experts back into the development loop. Requirements and mockup are re-validated in Step 3, to make sure the changes introduced by developers are accepted by end users and domain experts. Changes introduced in Step 3 lead to a new formal verification phase (Step 4). The iteration continues until a satisfactory design has been produced. The approach requires, besides support for developing mockups, a formal verification tool (theorem prover or model checker) that is able to support both the verification and the animation of the models. The technologies adopted in this work are introduced in the next sub-section. 2.1. Primer on PVS and PVSio-web PVS [Owre et al., 1992] is an interactive theorem proving system based on sequent calculus. PVS specifications are called theories. Properties to be proved of the specification are called theorems. Theories and theorems are specified in a higher-order logic language. The basic elements of the PVS syntax are as follows (additional elements will be introduced and explained later in Section 4, when introducing the pill box example): •Function types: they are type expressions of the form [domain ->range],whererange can be another function type. The commands defined in this paper are typically of the form [state ->state]; hence, their type defines a function that transforms the current state of the device into a new updated state following the execution of an action (for example, pwd_screen(st: state): state, see Listing 1.7). Anonymous functions are expressed using the LAMBDA keyword. They can be conveniently used to initialize and update data structures. For example, LAMBDA (x: fields_type): FALSE,wherefield_type is an enumeration, is a function of type [fields_type ->boolean] that can be used to create a hashmap table where all elements are initialized to the boolean constant FALSE. •Subtypes: these types use a predicate to restrict the domain of another type. They are defined using the syntax S: TYPE = {x:T|P(x) },whereTis a type, Pis the subtyping predicate and Sis a subtype of T.The same subtype can be expressed using a more compact form (P), where the predicate name is within round parentheses. Subtypes are used in the paper to describe commands that are only available under particular conditions. For example, in the definition of the command password_screen (see Listing 1.1), the function is only permitted if a predicate per_password_screen, which is called the permission function, is true. Hence, the signature of password_screen has the following form: password_screen(st: (per_password_ screen)): state. The predicate per_password_ screen is only true if the state of the device is in certain modes. •Enumerated types are declared by listing the enumerated constants between a pair of curly brackets. An example is path_mode_type: TYPE = {scripts_path, meds_path, no_path }, where path_mode_type is the name of the enumerated type and scripts_path,meds_path and no_path are the enumerated constants. •Record types are declared by listing the name of the record attributes between a pair of square brackets and the hash symbol. An example record type declaration is as follows: where patient_type is the name of the record type; p_name,p_fields,script_index and scripts are record attributes. p_index and s_index are types defining the set of patient and script names, respectively. fields_set defines the set of fields describing the patient and list_script_type the list of prescriptions for the patient. •Record literals are specified as a list of assignments between a pair of round brackets and the hash symbol. An example literal is as follows: where nil_patient is the name of the literal. This literal specifies initial values for the patient fields. The expression nil_patient‘p_name can be used to access a record field. An equivalent functional notation p_name(nil_patient) can also be used for the same purpose. As mentioned earlier in this section, the PVS theorem prover uses sequent calculus. Theorems to be proved of a specification are presented in the form {-1}A1 {-2}A2 {-3}.. | ———- {1}S1 {2}S2 {3}.. Interacting with Computers, Vol. 33 No. 1, 2021 Downloaded from https://academic.oup.com/iwc/article/33/1/55/6232199 by guest on 18 March 2024 58 M. D. Harrison et al. where A1,..., An are formulae called antecedents and S1,..., Sn are formulae called consequents. Intuitively, antecedents can be thought of as the hypotheses of the theorem, and the consequents comprise the theorem to be proved. Inference rules are used to perform the proof. A proof is considered complete when the application of the inference rules leads to a consequent that is true, or an antecedent that is false, or when an antecedent occurs also as a consequent. A first example in the paper of a proof of this kind is presented and discussed in Section 3.3. PVSio-web [Masci et al., 2015b] is a web-based environment that enables the creation of interactive prototypes based on executable PVS specifications. The toolkit supports the creation of both storyboard-based prototypes using mockup pictures of different screens of the system under development [Watson et al., 2018]andhigh-fidelity prototypes that can closely resemble the visual appearance and behaviour of a final product. The interactive prototypes, so constructed, can be evaluated with end users. PVSio-web prototypes use a split architecture to create a separation of concerns between the specification of the behaviour of the prototype and its visual appearance. •The back-end of a PVSio-web prototype defines the behaviour of the prototype. The PVSio evaluation environment [Muñoz, 2003] is used to compute the evolution of the prototype, including how the prototype reacts to user actions and other system events. PVSio executes specifications written in the logic language of the PVS verification system by automatically translating the model into Lisp code. PVS specifications can either be created manually or automatically generated from Emuchart diagrams. Emuchart is a graphical state transition language that is a simplified version of Statecharts [Harel, 1987]. •The front-end is executed in a Web browser, rendering the visual appearance of the prototype. A picture of the real system is used as a basis for its visual appearance. JavaScript code is used to create interactive areas over the picture to enable user interactions with the prototype and are translated into evaluation commands for the back-end. A set of widgets provided by PVSio-web facilitates the definition of common interactive elements such as buttons and touchscreen elements. The frontend is refreshed every time the state of the underlying PVS specification changes. State attributes of the PVS specification that are intended to be visible in the user interface are rendered as displays in the prototype, thereby reproducing the attribute’s look and feel. 3. THE DESIGN PROBLEM The design problem that is used in the paper had been explored originally at the Polytechnic Institute of Cávado and Ave in (a) Password screen (b) Patient list screen (c) Patient details screen FIGURE 1. Example sketch images produced for the initial prototype. Portugal. A prototype had already been developed by that organization. A system was required that could be provided in care-home common rooms or hospital wards. Its purpose would be to enable the alerting and dispensing of medications at appropriate times and with appropriate prescriptions. It was proposed that patients be alerted when a dose was due according to their particular prescriptions. Only the designated patient, or their doctor or nurse carer, was to be permitted to access the required dose. The solution that had been originally sketched, see Fig. 1, assumes a stand-alone device that provides the required facility to patients. The sketch, used as a starting point for the analysis, was developed from the prototype that already existed. Facilities in the proposed design illustrated the following: (i) a database of medications and doses, available to be used as prescriptions, that could be viewed and in some cases updated by authorized personnel and (ii) the updating of patient details and associated prescriptions. This latter facility Interacting with Computers, Vol. 33 No. 1, 2021 Downloaded from https://academic.oup.com/iwc/article/33/1/55/6232199 by guest on 18 March 2024 Balancing the Formal and the Informal 59 required both an appropriate authorized person and the patient. The patient’s thumb print was to be used for user authentication. The device, as envisaged, alerts the patient when medicine is due and the patient responds and obtains their dose using a thumb print to ensure they are receiving the medication intended for them or through gated access by the designated carer (though this aspect of the administration process is not the focus of the paper). The device maintains a database of patients who have been subscribed to the system as well as a list of their prescriptions. The pill dispenser supports ‘columns’ of pills from which the patient can obtain their required dose. 3.1. Pathways The sketch design indicates three user pathways: (i) making available to the patient the appropriate medication at the appropriate time, (ii) setting up and editing the patient details along with a list of medication prescriptions and (iii) updating the medications database. The rest of this paper focuses only on prototypes and specifications based on pathways (ii) and (iii) because the main design challenges covered in these two pathways also relate to the first pathway (see next sub-section for a discussion of the design challenges). A design challenge, that is not discussed here, relates to issues associated with timing. Our previous work on infusion pumps [Harrison et al., 2017] demonstrates how to address the timing dimension. 3.2. Design challenges and preliminary requirements The pathways provide insights into the initial set of requirements. The following main design challenges can be identified: •Patient functions. The system should include functions that allow a patient to obtain a medication through thumbprint identification. •Carer functions. The system should allow designated carers to create patient logins, enter patient details and enter prescription details. •Pharmacy functions. Functions should also be provided to update medications and prescription details. Preliminary requirements are identified based on these design challenges. The initial focus is on the security and usability of the design. The pathways must satisfy requirements that relate to mutually exclusive access. The person that is authorized to update the medications database should not have access to patient details. The person that is authorized to update and view patient details should not be able to update the medical database. Clearly, the design should not allow a circumstance where the user is able to access or update data that should not be available to them. The design should also satisfy use-centred requirements. In particular, actions available to the user should have consistent behaviour. These requirements will be made more precise as the specification is developed in subsequent sections of the paper. 3.3. The initial formal model A video of the early prototype of the pill box device was provided to the authors. This formed the basis for a storyboard that was suitable for initial evaluation with stakeholders (see Fig. 1). Sketches representing each display state were created based on the material provided by the video. Appropriate images were used to illustrate entry, or modification, of patient details as well as displays that indicate the requirement for password entry by the nurse or carer responsible for setting up patient details. For example, images relating to patient details illustrate the following aspects: •when patient information can be entered; •the authentication sequence based on the patient’s thumb print; •how to access the list of patients in the database; •how to change the details stored for each patient; •how a prescription can be added or removed. Similarly, storyboard images, related to the medications database, indicate that the database is protected by password, and access is only enabled for doctors or pharmacists who are able to enter details of medicines. This pathway includes screen displays that allow entry or editing of medicines. The medicine pathway includes display screens that allow medicines to be listed or displayed and modified. The storyboard describes the paths that are possible with non-functional representations of these displays. It gives no information about the other actions within each state. The storyboard images were used to create a first interactive prototype in PVSio-web. Figure 2indicates a phase of the creation of the prototype. Green areas on the left-hand side of the sketch design represent interactive buttons that can be used to navigate to a different screen. The full list of screens used to develop the sketch design is shown at the bottom-left corner of the figure. PVSio-web creates a state machine diagram from the interactive storyboard. The state machine is represented using an Emuchart. The diagram is then translated into an executable PVS specification. Each node in the Emuchart represents a display screen, and each labelled edge represents a transition between screens. A fragment of the Emuchart can be seen in Fig. 3. Listing 1.1 shows the PVS specification that was generated automatically from the Emuchart diagram. Nodes are translated into an enumerated type Mode. Labelled edges are translated into PVS functions. The state of the diagram is represented using a record type state that includes an attribute current_mode of type Mode, indicating the current screen. The initial state of the specification is thus specified Interacting with Computers, Vol. 33 No. 1, 2021 Downloaded from https://academic.oup.com/iwc/article/33/1/55/6232199 by guest on 18 March 2024 60 M. D. Harrison et al. (Lines 8 and 9) as a record literal with current_mode set to initial_screen. The transition function password_screen (Lines 18–29) is linked to the Emuchart edges that enter node password_ screen. The function uses a subtyping predicate, per_ password_screen, to restrict the domain of the function. The predicate reflects the structure of the Emuchart, as edges entering node password_screen originate only from three nodes, database_password_screen, pill_dispensed_screen and initial_screen (see Fig. 3). Two auxiliary functions, leave and enter_into, are used to update attribute current_mode. This storyboard provides sufficient information to serve two purposes. The first purpose is to allow a user to navigate the state transition model associated with the interactive storyboard. It shows sketch images at each state of the model (see Fig. 2for example). In practice, this can be used as a preliminary stage of user evaluation with relevant stakeholders. The second purpose is to provide a basis for demonstrating that the initial requirements, developed through the initial elicitation process, are satisfied. An important initial requirement is that the patient database and the medical database can only be updated by relevant authorized personnel who have entered their passwords (see Section 3.2). Those authorized to access the medical database are not authorized to access the patient database. In the case of this initial requirement, more formal analysis enables a more exhaustive exploration of all the possible paths. To specify this requirement as a property, it was necessary to adjust the initial specification generated automatically from the Emuchart. Additional attributes were added manually to the PVS specification necessary to keep track of which pathway is taken and which password is used to access the system. The state of the device is augmented with two attributes: path_mode_set, indicating which credentials were used to access the system, and path_mode, which associates each screen to a pathway. If these two attributes differ, then the user is attempting an unauthorized entry. These changes in the structure of the state require some adjustments in functions init and enter_into generated automatically from the Emuchart, see Listing 1.2. The transition (enter_into)is updated by including two assignments to the added attributes to state (see Lines 23–30). An example requirement that can now be checked is as follows: it should not be possible to reach the screen new_med (which allows updating of the medical database) unless the user has gone through the db_pwd screen. The screen new_med is associated with meds_path, and therefore the attribute FIGURE 2. Creation of the sketch design in PVSio-web. Interacting with Computers, Vol. 33 No. 1, 2021 Downloaded from https://academic.oup.com/iwc/article/33/1/55/6232199 by guest on 18 March 2024 Balancing the Formal and the Informal 61 FIGURE 3. The initial sketch: Emucharts diagram. LISTING 1.1. Fragment of the PVS specification generated from the Emuchart. path_mode_set should be meds_path if the user has, as required, gone through the medical database password (db_pwd) screen. The formalization of this requirement can be found in the theorem given in Listing 1.3. The theorem LISTING 1.2. Re-defining enter_into. uses a structural induction. It checks, for all accessible states, that path_mode and path_mode_set are as they should be, that is defined by path_function (see Line 3) and remain the same through state transitions (see Line 6). Note that Interacting with Computers, Vol. 33 No. 1, 2021 Downloaded from https://academic.oup.com/iwc/article/33/1/55/6232199 by guest on 18 March 2024 62 M. D. Harrison et al. path_function is defined to associate the expected path mode with each state of the model. This function is described in detail in relation to the second iteration of the model (see Listing 1.25). LISTING 1.3. Pathway theorem relating to the sketch design. A state is accessible if it can be reached from a previous state by a transition function. The transition function is described by the predicate state_transitions, part of which is illustrated in Listing 1.4. LISTING 1.4. The state transitions predicate. The theorem fails with many counter-examples. One of the counter-examples indicates that it is possible to move from db_menu andthentodb_patient_list (which can only be viewed by a carer). The counter example generated by PVS, when attempting proof, can be seen in Listing 1.5.The proof fails. This can be seen by combining elements of the antecedent [-3] in Lines 4–8. path_mode_set(post) is meds_path, but the current path mode is scripts_path. The consequent in Line 13 therefore cannot be proved. LISTING 1.5. Counter-example to Listing 1.3 theorem. Further details in the design and its specification are required to prove a suitable path requirement as well as other use-centred requirements. These details will be discussed in Section 4. 4. THE SECOND ITERATION The second iteration aims to fill gaps in the initial prototype (e.g. data entry functions and other details that were shown only in the images of the storyboard and not captured in the Emuchart diagram). The first iteration of the model simply indicates which transitions can take place between which screens. It does not provide detail about the content of the values entered, simply that the information is entered. The model created in the second iteration describes, in more detail, all these aspects. It provides a more functional representation that can be used in analysing requirements and evaluating the usability of a prototype. Changes, as a result of evaluation of the previous iteration of the design, through the sketch prototype with end users, and through analysis of the pathway requirements, led to the new specification. Clearly, this may not be a refinement of the design in the strict formal sense [Morgan, 1994]. Changes in response to evaluation may in fact include changes in functionality. The changes involved restructuring the model (see the repository1for a full specification of the restructured model). The new specification describes the circumstances under which an action can be taken (for example, through the entry of relevant data fields) and also the effect of the action. The result of executing an action depends on the display mode. The device state therefore describes the structure of the screen, including the actions that are visible and available, as well as which fields must be entered before an action can be completed. Actions cause transitions between modes and can also include updates to the state, for example updates to the patient database. Transitions may also be caused by selecting fields and entering values. These latter transitions do not change mode. They add to the set of fields that have been entered and also add the values entered to temporary records of patients, their prescriptions or medicines (depending on mode). The remainder of this section describes illustrative fragments of the new specification in more detail. 4.1. Modes, keys, fields and databases The type associated with display modes and path modes are based on those identified in the first iteration. Fields used to handle data entry (Lines 16–18 of Listing 1.6) and a field indicating the availability of actions (Line 19) have been added to the device state. The definition of these fields required the creation of two new data types: available_actions_type and fields_set (Lines 10–11). They are arrays of booleans that store information about the availability of actions and fields in a given device state. The new version of the model includes functions that represent transitions between display states in the same way as 1http://hcispecs.di.uminho.pt/m/8 Interacting with Computers, Vol. 33 No. 1, 2021 Downloaded from https://academic.oup.com/iwc/article/33/1/55/6232199 by guest on 18 March 2024 Balancing the Formal and the Informal 63 the first iteration. For example, password_screen (the initial specification is in Listing 1.1) is now represented as a function pwd_screen (see Listing 1.7) which changes mode to the display that requests a password to enter the scripts path. The function changes attributes mode,path_mode and path_mode_set appropriately. The function changes the availability of actions (Lines 6–9) as well as the visibility of fields (Lines 10–11) and indicates that no actions are selected and no fields selected or entered. A function clear_screen (Line 2) provides the basic blank state of the screen (with no actions or fields, and fields are not selected or entered) which is enriched by changes to the state attributes defined in the WITH clause (Lines 3–12). LISTING 1.6. Types used in the second iteration model. From the password screen, the user is first required to select the password field (which is visible, see Lines 10–12 in Listing 1.7) and then enter the password before selecting an appropriate action. Two new functions are required to specify this functionality: enter, which defines how to enter the password, and select, which defines how to select fields and actions in the screen. LISTING 1.7. The second iteration password screen. The function enter is illustrated in Listing 1.8.Inthe simple case of password entry, the function checks that the password field is selected (Line 2) and assigns the field as entered (Lines 16–18) and clears the selection of the field (Line 19). LISTING 1.8. Entering a field. In the cases identified by the permission functions (Lines 5, 9 and 13), further checks are carried out when specific fields are being entered. For example, entering details associated with daily or weekly prescriptions will vary according to the period. There is insufficient space to describe this part of the specification in detail. The full specification in the repository provides more information. The select function is polymorphic and can be applied both to fields (Listing 1.9) and actions (Listing 1.10). When applied to a field, if the field is visible (Line 2 in Listing 1.9), then the function flags the given field as selected. This is not made explicit in the model but there is an underlying assumption that there is a process of selection that maps to the select function (for example moving the cursor to the action icon or displayed field and using a mouse and clicking to select). Otherwise, the state remains unchanged. LISTING 1.9. The select functions. When applied to an action, the select function checks that the action is available and then invokes an auxiliary function act that updates the device state (Line 2 in Listing 1.10). If the action is not available, the state remains unchanged. LISTING 1.10. The select functions. Interacting with Computers, Vol. 33 No. 1, 2021 Downloaded from https://academic.oup.com/iwc/article/33/1/55/6232199 by guest on 18 March 2024 70 M. D. Harrison et al. LISTING 1.28. Select field function. This means that the user can see the medicine details but cannot update the device. Both theorems, representing the two pathway requirements, are true of the specification. 8. RELATED WORK While there is relatively little literature concerned with development techniques that combine informal representations of design with formal models, there are many activities that combine different formal descriptions of visual, functional and task elements. In Furniss et al. [2014]andMasci et al. [2015a], formal methods have been integrated with contextual enquiry with the aim of supporting the work of a field investigator (as opposed to supporting the development of a device). Written notes provided by the field investigator described workflows carried out by clinicians in a hospital. This included how information resources are communicated and transformed throughout the socio-technical system. The notes were manually translated to a PVS model by a formal methods expert, and formal analysis was used to identify gaps and weaknesses that could warrant further investigation. In Masci et al. [2012], formal methods were used to support incident investigation methods. Key aspects of an incident report were modelled in PVS with the aim of analysing claims and hypotheses described in the report. In Masci et al. [2017], formal methods were used to extend a standard hazard analysis process and promote rigorous specification of safety requirements. Bowen & Reeves [2017] explore the relation between display and functional models. Their work also focuses on specifications of sketch designs and aims to enable analysis of these designs. It is not clear, however, that executable versions of their models have been developed. Haesen et al. [2011] integrate models and informal design knowledge. Their focus is also the role of formal task models and abstract user interfaces in user-centred design. They use personas, scenarios and related task models in their models. Graphical models of storyboards are produced along with constraints on these models. Bolton et al. [2014], Mori et al. [2002]andFields [2001] combine task and functional models. Martinie et al. [2011] combine visual, functional and task elements. 9. CONCLUSION The process of user-centred design described in the paper is iterative. The initial non-functional design is based on the initial interviews with, or observations of, participants in the work environment. In this case, it would be envisaged that patients, carers, pharmacists and doctors would be involved in this initial process. The initial non-functional design would be evaluated both by the participants and then by considering the preliminary requirements (for example, in this case, that the pathways are mutually exclusive). Subsequent iterations of the specification will generate a functional prototype that can be subjected to further user evaluation. The requirements that have been developed through the previous stages of the process will be proved of these iterations and as features are added or issues are discovered in the use of the design further requirements will be added. The final result will be a design that has been tested with users and provably satisfies usability requirements. It will be a design that is based on a specification that will additionally support safety and security analysis. Two iterations of the design are described in this paper. The model of the first iteration, the sketch design, was produced automatically from an initial sketch. A single property, the pathway property, was proved of that model. The second iteration involved a specification consisting of 83 functions, analysed using 26 PVS theorems, which were proved within on average 3 seconds. The PVS system was installed on an Apple Macbook Pro with a 2.9 GHz Intel Dual Core i5. The conversion functions required to animate the specification involved 189 lines. Similar much larger specifications have been used to model a variety of full-scale interactive systems, for example Harrison et al. [2019a,b]. In the case of Harrison et al. [2019b], a model of the controller for a neonatal dialysis machine was developed. Safety properties were checked in meetings involving the developers and a formal analyst. In many cases where a property failed, the model or the property could be adjusted, and appropriate rationale developed, within the meeting. A future dimension of this work, currently under development, is to simplify and automate some of these processes. Tools for presenting and instantiating property templates are being developed. Heuristics are being developed to automate the proof of PVS theorems. The process of using PVSio-web is being simplified to construct prototypes from models. The aim is to make these techniques accessible to a wider group of developers. An important challenge in developing the approach described in this paper was not to reduce the value of user-centred design. A criticism often levelled at formal techniques is that they can have the effect of limiting the scope of the analysis, ignoring important broader issues. It is hoped that analysis, as an adjunct to the techniques and approaches of user-centred design, responds to these criticisms. A further concern is that the effort and knowledge involved in producing the models Interacting with Computers, Vol. 33 No. 1, 2021 Downloaded from https://academic.oup.com/iwc/article/33/1/55/6232199 by guest on 18 March 2024 Balancing the Formal and the Informal 71 and performing the analysis are not cost effective. It is true that these are techniques that are not typically found in the toolkit of a development team, particularly the small teams that often design and implement medical devices such as the one used here for illustration purposes. However, the safety of medical devices, in particular, is crucial and a thorough analysis of usability issues is a key contribution ensuring safety. Acknowledgments Nuno Rodrigues, João Vilaça and Nuno Dias from IPCA (Polytechnic Institute of Cavado and Ave) developed the first prototype of the pill dispenser. Funding This work is financed by National Funds through the Portuguese funding agency, FCT – Fundação para a Ciência e a Tecnologia, within project UIDB/50014/2020. REFERENCES Beyer, H. and Holtzblatt, K. (1998) Contextual Design: Defining Customer-Centred Systems. Morgan Kaufmann. Bolton, M., Jiménez, N., van Paassen, M. and Trujillo, M. (2014) Automatically generating specification properties from task models for the verification of human-automation interaction. IEEE Trans. Hum. Mach. Syst., 44, 561–575. Bolton, M. L., Bass, E. and Siminiceanu, R. (2013) Using formal verification to evaluate human-automation interaction, a review. IEEE Trans. Syst. Man Cybern. Part A Syst. Humans, 99, 1–16. Bowen, J. and Reeves, S. (2017) Combining Models for Interactive System Modelling. In Weyers, B., Bowen, J., Dix, A. and Palanque, P. (eds), The Handbook of Formal Methods in HumanComputer Interaction, pp. 161–182. Springer International Publishing, Cham. Carroll, J. (ed.) (1995) Scenario Based Design: Envisioning Work and Technology in System Development. Wiley. Fields, R. E. (2001) Analysis of erroneous actions in the design of critical systems. PhD Thesis, Department of Computer Science, University of York, Heslington, York, YO10 5DD. Furniss, D., Masci, P., Curzon, P., Mayer, A. and Blandford, A. (2014) 7 themes for guiding situated ergonomic assessments of medical devices: a case study of an inpatient glucometer. Appl. Ergon.,5, 1668–1677. Haesen, M., Van den Bergh, J., Meskens, J., Luyten, K., Degrandsart, S., Demeyer, S. and Coninx, K. (2011) Using Storyboards to Integrate Models and Informal Design Knowledge. In Hussmann, H., Meixner, G. and Zuehlke, D. (eds), Model-Driven Development of Advanced User Interfaces, pp. 87–106. Springer Berlin Heidelberg, Berlin, Heidelberg. Harel, D. (1987) Statecharts: a visual formalism for complex systems. Sci. Comput. Program., 8, 231–274. Harrison, M., Campos, J. and Masci, P. (2015) Reusing models and properties in the analysis of similar interactive devices. Innov. Syst. Softw. Eng., 11, 95–111. Harrison, M., Masci, P. and Campos, J. (2018) Formal Modelling as a Component of User Interface Design. In Mazzara, M., Ober, I. and Salaün, G. (eds), Software Technologies: Applications and Foundations STAF 2018 Collocated Workshops (Revised Selected Papers). Lecture Notes in Computer Science, vol. 11176, pp. 274–294. Springer. Harrison, M., Masci, P. and Campos, J. (2019a) Verification templates for the analysis of user interface software design. IEEE Trans. Softw. Eng., 45, 802–822. Harrison, M. D., Freitas, L., Drinnan, M., Campos, J. C., Masci, P., di Maria, C. and Whitaker, M. (2019b) Formal techniques in the safety analysis of software components of a new dialysis machine. Sci. Comput. Program., 175, 17–34. Harrison, M. D., Masci, P., Campos, J. C. and Curzon, P. (2017) Verification of user interface software: the example of use-related safety requirements and programmable medical devices. ACM Trans. Hum. Mach. Syst., 47, 834–846. Martinie, C., Palanque, P., Barboni, E., Winckler, M., Ragosta, M., Pasquini, A. and Lanzi, P. (2011) Formal tasks and systems models as a tool for specifying and assessing automation designs. In Proc. 1st int. conf. application and theory of automation in command and control Systems, ATACCS ‘11, pp. 50–59. IRIT Press, Toulouse, France. Masci, P., Ayoub, A., Curzon, P., Harrison, M., Lee, I., Sokolsky, O. and Thimbleby, H. (2013) Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. In Proc. ACM symposium engineering interactive systems (EICS 2013), pp. 81–90. ACM Press. Masci, P., Curzon, P., Furniss, D. and Blandford, A. (2015a) Using pvs to support the analysis of distributed cognition systems. Innov. Syst. Softw. Eng., 11, 113–130. Masci, P., Huang, H., Curzon, P. and Harrison, M. D. (2012) Using PVS to Investigate Incidents Through the Lens of Distributed Cognition. In Goodloe, A. E. and Person, S. (eds), NASA Formal Methods. Lecture Notes in Computer Science, vol. 7226, pp. 273–278. Springer, Berlin Heidelberg. Masci, P., Oladimeji, P., Zhang, Y., Jones, P., Curzon, P. and Thimbleby, H. (2015b) PVSio-web 2.0: Joining PVS to HCI. In Kroening, D. and P˘ as˘ areanu, C. S. (eds), Computer aided verification: 27th int. conf. CAV 2015, San Francisco, CA, USA, July 18–24, 2015, Proceedings, Part I, pp. 470–478. Springer International Publishing, Cham. Masci, P., Zhang, Y., Jones, P. and Campos, J. C. (2017) A hazard analysis method for systematic identification of safety requirements for user interface software in medical devices. In 15th int. conf. software engineering and formal methods (SEFM 2017), pp. 284–299. Springer. Monk, A., Wright, P., Haber, J. and Davenport, L. (1993) Improving Your Human-Computer Interface: A Practical Technique. Prentice-Hall. Morgan, C. C. (1994) Programming from Specifications (2nd edn). Prentice-Hall International. Mori, G., Paternò, F. and Santoro, C. (2002) CTTE: support for developing and analyzing task models for interactive system design. IEEE Trans. Softw. Eng., 28, 797–813. Interacting with Computers, Vol. 33 No. 1, 2021 Downloaded from https://academic.oup.com/iwc/article/33/1/55/6232199 by guest on 18 March 2024 72 M. D. Harrison et al. Muñoz, C. (2003) Rapid Prototyping in PVS. Technical Report NIA Report No. 2003–03, NASA/CR-2003-212418, National Institute of Aerospace. Nielsen, J. and Molich, R. (1990) Heuristic evaluation of user interfaces. In Chew, J. and Whiteside, J. (eds), ACM CHI proc. CHI ‘90: empowering people, pp. 249–256. Owre, S., Rushby, J. and Shankar, N. (1992) PVS: A prototype verification system. In Kapur, D. (ed.), Eleventh int. conf. automated deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 607, pp. 748–752. Springer. Sommerville, I. (2010) Software Engineering. Addison-Wesley. Watson, N., Reeves, S. and Masci, P. (2018) Integrating user design and formal models within PVSio-Web. In Workshop on formal intergrated development environment (F-IDE-18). Electronic Proc. theoretical computer science (EPTCS). Interacting with Computers, Vol. 33 No. 1, 2021 Downloaded from https://academic.oup.com/iwc/article/33/1/55/6232199 by guest on 18 March 2024