CHI+MED logo banner

Refinement in developing and verifying user interface requirements for infusion pumps

Key points

  • Criteria for the acceptable safety of medical devices, safety requirements, are typically described precisely, but in natural languages like English. An important issue is how the regulator can be assured that the given requirements are satisfied.

  • We have developed a refinement based approach that involves gradually transforming  a requirement into a form that can be coded. It relates to the pre-market review process promoted by the FDA to provide safety assurances.

  • Our approach helps to both design and clarify high level safety requirements that relate to user interfaces of medical devices.

  • It also supports the development of usage models for a range of interaction methods and their verification against safety requirements.

The designs of medical devices can potentially exhibit a range of problems about the way we have to interact with them. Many of these problems have an impact on patient safety and contribute to health-care costs. Criteria for the acceptable safety of devices are commonly described by the regulator as safety requirements that the device should follow. These requirements are typically described precisely but in natural languages like English. The regulator’s aim is to be sure that risks associated with the use of a device are as low as reasonably practicable. Part of this assurance is gained through a credible demonstration that the device meets the safety requirements. An important issue is how the regulator can be sure of this.

Currently, medical device regulators rely on the pre-market review process. This is a process by which they have to check a design is safe in a short period of time. The manufacturer has to provide paperwork that demonstrates either that the new device is as safe and effective as an already legally marketed device, or that it has been developed following recognised international standards. To reduce the amount of paperwork and collect more succinct and rigorous evidence, the use of formal methods - mathematical techniques - to support the checking, has been suggested. The FDA, the regulator for medical devices in the US, is now promoting this approach. It is based on developing safety based usage models. They describe the common characteristics and behaviour of software for broad classes of devices mathematically. The aim is to show that these models satisfy core sets of safety requirements that are designed to mitigate typical hazards. The regulator would provide them as a reference for manufacturers, showing how the requirements can be met.

Correct by construction
We have developed an approach for deriving usage models from requirements that are correct-by-construction. It uses refinement, which is a way of mathematically transforming one model into another while preserving its important properties. The approach focusses specifically on the interactive aspects of medical devices. Usage models for interface requirements are complex because systems can use different interaction technologies that have very different characteristics. For example, one design may use a keypad with digits for entering numbers, whereas another might use up and down arrows for the same purpose.

We address two key points of the FDA’s approach. The first is how to design and clarify high level safety requirements so that they are sufficiently precise to be related to the behaviour of a medical device. The second is to provide a way to cover all the different interaction technologies used by medical systems. A mathematical formalism is initially used to express the high level requirements such as those proposed by the FDA. Refinement, supported by an automatic tool, is then used to make those high level requirements more precise. It is also then used to show how the requirement can be met by different interaction technologies. It is cascaded into a hierarchy of usage models that capture the variety of possible designs.

Linking to the pre-market review process
Our approach relates to the current FDA pre-market review process. It relies on establishing substantial equivalence between the new product and a reference device that has been demonstrated to be safe. In our approach, the relevant safety requirements are shown to be satisfied by a top level usage model. Then the safety and usability of the user interface for the specific pump is demonstrated by showing that the interface belongs to the hierarchy of usage models.

Proof of Concept
As a proof of concept, we have successfully used this approach to develop a subset of safety requirements provided by the FDA and analyse two commercial infusion pumps against them. The considered safety requirements relate to two critical aspects of the user interface design in infusion pumps: the usability of their data entry systems (e.g. “The flow rate for the pump shall be programmable”), and the safeguards against inadvertent changes of or tampering with infusion settings (e.g. “Clearing of the pump settings shall require confirmation”).

Key people
Rimvydas Rukšėnas, Paolo Masci, Paul Curzon, Michael Harrison

Rukšėnas, R., Masci, P., Harrison, M. D., & Curzon, P. (2013). Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach. Proceedings of the 5th International Workshop on Formal Methods for Interactive Systems (FMIS 2013). Electronic Communications of the EASST, vol. 69.

Rukšėnas, R., Masci, P., & Curzon, P. (2015). Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach. Chapter in L. Petre & E. Sekerinski (Eds), From Action Systems to Distributed Systems: The Refinement Approach, Chapman and Hall/CRC (in press).