Curzon P, Masci P, Oladimeji P, Ruksenas R, Thimbleby H, D'Urso E.  2014.  Human-Computer Interaction and the Formal Certification and Assurance of Medical Devices: The CHI+MED Project. 2nd Workshop on Verification and Assurance (Verisure2014), in association with Computer-Aided Verification (CAV), part of the Vienna Summer of Logic. Abstractverisure14.pdf

The number of recalls of medical device with embedded computers due to safety issues in recent years suggests there is a need for new approaches to support the process. There is increasing concern about the impact of systematic use errors. There has been little research focusing on model-based tool support for the assurance and certification of medical devices with respect to systematic use error, however. The CHI+MED project ( aims to address this gap. It is concerned with the design of safer medical devices with a specific focus on human-computer interaction. We are developing a range of integrated model-based engineering methods and other formal and semi-formal techniques to support the certification process, both pre- and post-market, including their use in the wider system context. In this position paper we review our approach and the contributions to date.

Bernardeschi C, Domenici A, Masci P.  2014.  Integrated Simulation of Implantable Cardiac Pacemaker Software and Heart Models. Proceedings of the 2nd International Congress on Cardiovascular Technologies. 2014_cardiotechnix.pdf
Harrison M, Masci P, Campos JC, Curzon P.  2013.  Automated theorem proving for the systematic analysis of interactive systems. Proceedings of the 5th International Workshop on Formal Methods for Interactive Systems. Abstractharrisonmcc.pdf

This paper describes the use of an automated theorem prover to analyse properties of interactive behaviour. It offers an alternative to model checking for the analysis of interactive systems. There are situations, for example when demonstrating safety, in which alternative complementary analyses provide assurance to the regulator. The rigour and detail offered by theorem proving makes it possible to explore features of the design of the interactive system, as modelled, beyond those that would be revealed using model checking. Theorem proving can also speed up proof in some circumstances. The paper illustrates how a theory generated as a basis for theorem proving (using PVS) was developed systematically from a MAL model used to model check the same properties. It also shows how the CTL properties used to check the original model can be translated into theorems.

Masci P, Ayoub A, Curzon P, Harrison M, Lee I, Sokolsky O, Thimbleby H.  2013.  Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. Proceedings ACM Symposium Engineering Interactive Systems - EICS. :81-90. Abstractmascietal.pdf

Medical device regulators such as the US Food and Drug Administration (FDA) aim to make sure that medical devices are reasonably safe before entering the market. To expedite the approval process and make it more uniform and rigorous, regulators are considering the development of reference models that encapsulate safety requirements against which software incorporated into medical devices must be verified. Safety, insofar as it relates to interactive systems and its regulation, is generally a neglected topic, particularly in the context of medical systems.

An example is presented that illustrates how the interactive behaviour of a commercial Patient Controlled Analgesia (PCA) infusion pump can be verified against a reference model. Infusion pumps are medical devices used in healthcare to deliver drugs to patients, and PCA pumps are particular infusion pump devices that are often used to provide pain relief to patients on demand. The reference model encapsulates the Generic PCA safety requirements provided by the FDA, and the verification is performed using a refinement approach.

The contribution of this work is that it demonstrates a concise and semantically unambiguous approach to representing what a regulator’s requirements for a particular interactive device might be, in this case focusing on user-interface requirements. It provides an inspectable and repeatable process for demonstrating that the requirements are satisfied. It has the potential to replace the considerable documentation produced at the moment by a succinct document that can be subjected to careful and systematic analysis.

Oladimeji P, Masci P, Curzon P, Thimbleby H.  2013.  PVSio-web: a tool for rapid prototyping device user interfaces in PVS. FMIS2013, 5th International Workshop on Formal Methods for Interactive Systems, London, UK, June 24, 2013. 69 Abstractfmis2013.pdf

We present PVSio-web which extends the simulation component of the PVS proof system with functionalities for rapid prototyping device user interfaces. The tool presents itself as a classic image-editing environment with functionalities such as area selection and hyperlink creation, thus reducing the barriers that prevent non-experts in formal methods from using PVS. Designers load a picture of the layout of the device user interface under development, specify interactive areas over the layout, and link them to a PVS specification. They can then explore the behaviour of the formal user interface specification through point-and-click interactions. The architecture of the tool is general, and can be used as the basis for extending other verification tools. A demonstration of the capabilities of PVSio-web is presented through an example based on a commercial medical device user interface. Our ultimate aim is to promote and facilitate the use of formal verification tools when developing device user interfaces.

Ruksenas R, Masci P, Harrison M, Curzon P.  2013.  Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach. FMIS2013, 5th International Workshop on Formal Methods for Interactive Systems, London, UK, June 24, 2013. 69 Abstract964-2899-1-pb.pdf

It is common practice in the description of criteria for the acceptable safety of systems for the regulator to describe safety requirements that should be satisfied by the system. These requirements are typically described precisely but in natural language and it is often unclear how the regulator can be assured that the given requirements are satisfied. This paper is concerned with a rigorous refinement process that demonstrates that a precise requirement is satisfied by the specification of a given device. It focuses on a particular class of requirements that relate to the user interface of the device. For user interface requirements, refinement is made more complex by the fact that systems can use different interaction devices that have very different characteristics. The described refinement process recognises an input/output hierarchy.

Masci P, Ayoub A, Curzon P, Lee I, Sokolsky O, Thimbleby H.  2013.  Model-Based Development of the Generic PCA Infusion Pump User Interface Prototype in PVS. Computer Safety, Reliability, and Security. 8153:228-240. Abstractgpcaui-safecomp2013.pdf

A realistic user interface is rigorously developed for the US Food and Drug Administration (FDA) Generic Patient Controlled Analgesia (GPCA) pump prototype. The GPCA pump prototype is intended as a realistic workbench for trialling development methods and techniques for improving the safety of such devices. A model-based approach based on the use of formal methods is illustrated and implemented within the Prototype Verification System (PVS) verification system. The user interface behaviour is formally specified as an executable PVS model. The specification is verified with the PVS theorem prover against relevant safety requirements provided by the FDA for the GPCA pump. The same specification is automatically translated into executable code through the PVS code generator, and hence a high fidelity prototype is then developed that incorporates the generated executable code.

Harrison M, Campos JC, Masci P, Thomas N.  2012.  Modelling and systematic analysis of interactive systems. Proceedings of the Workshop on Formal Methods in Human-Machine Interaction (Formal H). :25-28. Abstractformalh.2012.proceedings.pdf

Two aspects of our research concern the application of formal methods in human-computer interaction. The first aspect is the modelling and analysis of interactive devices with a particular emphasis on the user device dyad. The second is the modelling and analysis of ubiquitous systems where there are many users, one might say crowds of users.The common thread of both is to articulate and prove properties of interactive systems, to explore interactive behaviour as it influences the user, with a particular emphasis on interaction failure. The goal is to develop systematic techniques that can be packaged in such a way that they can be used effectively by developers. This “whitepaper” will briefly describe the two approaches and their potential value as well as their limitations and development opportunities.

Masci P, Furniss D, Curzon P, Harrison M, Blandford A.  2012.  Supporting Field Investigators with PVS: A Case Study in the Healthcare Domain. Software Engineering for Resilient Systems. 7527:150-164. Abstractmascipvsdistributed.pdf

This paper reports the lessons learnt about the benefits of using a formal verification tool like PVS to support field studies. The presentation is based on a field study in the healthcare domain which was designed to investigate the resilience of human behaviour in an oncology ward of a hospital. The automated reasoning tool PVS was used systematically to compare actual practice observed during the field study with normative behaviour described for example by user manuals for the devices involved. The approach helped (i) identify latent situations that could lead to hazard, and (ii) suggest situations likely to warrant further investigation as part of the field study. The main contribution of this paper is a set of detailed examples that illustrate how we used PVS during the field study, and how the tool led to insights.

Masci P, Huang H, Curzon P, Harrison M.  2012.  Using PVS to Investigate Incidents through the Lens of Distributed Cognition. NASA Formal Methods. 7226:273-278. Abstractmascinasa.pdf

A systematic tool-based method is outlined that raises questions about the circumstances surrounding an incident: why it happened and what went wrong. The approach offers a practical and systematic way to apply a distributed cognition perspective to incident investigations, focusing on how available information resources (or the lack of them) may shape user action, rather than just on causal chains. This perspective supports a deeper understanding of the more systemic causes of incidents. The analysis is based on a higher order-logic model describing how information resources may have influenced the actions of those involved in the incident. The PVS theorem proving system is used to identify situations where available resources may afford unsafe user actions. The method is illustrated using a healthcare case study.

Cauchi A, Gimblett A, Thimbleby HW, Curzon P, Masci P.  2012.  Safer "5-key" number entry user interfaces using differential formal analysis. BCS HCI. :29-38. Abstract

Differential formal analysis is a new user interface analytic evaluation method based on stochastic user simulation. The method is particularly valuable for evaluating safety critical user interfaces, which often have subtle programming issues. The approach starts with the identification of operational design features that define the design space to be explored. Two or more analysts are required to analyse all combinations of design features by simulating keystroke sequences containing keying slip errors. Each simulation produces numerical values that rank the design combinations on the basis of their sensitivity to keying slip errors. A systematic discussion of the simulation results is performed for assessing the causes of any discrepancy, either in numerical values or rankings. The process is iterated until outcomes are agreed upon. In short, the approach combines rigorous simulation of user slip errors with diversity in modelling and analysis methods.

Although the method can be applied to other types of user interface, it is demonstrated through a case study of 5-key number entry systems, which are a common safety critical user interface style found in many medical infusion pumps and elsewhere. The results uncover critical design issues, and are an important contribution of this paper since the results provide device manufacturers guidelines to update their device firmware to make their devices safer.

Masci P, Ruksenas R, Huang H, Curzon P, Harrison M.  2012.  Formal verification and the prevention of systematic user error. FormalH, Workshop on Formal Methods in Human-Machine Interaction sponsored by the IFIP Working Group 13.5 on Human Error, Safety, and System Development.
Bernardeschi C, Cassano L, Domenici A, Masci P.  2011.  A Tool for Signal Probability Analysis of FPGA-Based Systems. COMPTOOLS2011, the 2nd Intl. Conf. on Computational Logics, Algebras, Programming, Tools, and Benchmarking.
Blandford A, Cauchi A, Curzon P, Eslambolchilar P, Furniss D, Gimblett A, Huang H, Lee P, Li Y, Masci P et al..  2011.  Comparing Actual Practice and User Manuals: A Case Study Based on Programmable Infusion Pumps. Eics4Med, the 1st International Workshop on Engineering Interactive Computing Systems for Medicine and Health Care. Abstract

We report on a case study investigating current practice in the use of a programmable infusion pump. We start by formalising an existing description of the procedure followed by nurses for setting up a commercial infusion pump obtained via observation and interview. We then compare and contrast this procedure with a formal description of the sequence of actions reported in the pump's user manual. Mismatches were validated by a training manager. The aim of this comparison is to point out how minor mismatches between the two descriptions can be used to reveal major safety issues. Our contributions are: first, we analyse a real-world system and show the importance of having a clear and consistent specification of the procedures; second, we show how a graph-based notation can be conveniently used for building non-ambiguous and intuitive specifications. We argue that this can provide support to an investigator when building a description of actual practice in that it can help focus attention on areas to observe more closely and questions to ask to understand why procedures, as followed, are the way they are.

Cauchi A, Curzon P, Eslambolchilar P, Gimblett A, Huang H, Lee P, Li Y, Masci P, Oladimeji P, Ruksenas R et al..  2011.  Towards Dependable Number Entry for Medical Devices. Eics4Med, the 1st International Workshop on Engineering Interactive Computing Systems for Medicine and Health Care. CEUR Workshop Proceedings, vol 727 Abstract

Number entry is an ubiquitous task in medical devices, but is implemented in many different ways, from decimal keypads to seemingly simple up/down buttons. Operator manuals often do not give clear and complete explanations, and all approaches have subtle variations, with details varying from device to device. This paper explores the design issues, critiques designs, and shows that methods have advantages and disadvantages, particularly in terms of undetected error rates.