A A A
CHI+MED logo banner
Loading

Verification of User Interface Software

Key points
We have:

  • Developed techniques for checking mathematically that the user interfaces of infusion pumps are safe and easy to use.
  • Used our methods to find safety problems in existing commercial infusion pumps.
  • The results are being used by regulators and hospitals to raise awareness about the problems found.

The FDA have developed a draft set of user-related safety requirements that infusion pumps should satisfy. Their current recommendation is that requirements should be demonstrated as true through evidence that the device being checked has been appropriately tested.

As a complementary and additional approach to this verification process the project has been developing techniques for checking mathematically that the user interfaces of infusion pumps are safe and easy to use. The value of these techniques is being demonstrated by using the methods to find safety problems in existing commercial infusion pumps. The results are being used by regulators and hospitals to raise awareness about the problems found.

prototypes.jpg

Figure 1: Example safety problems identified in commercial products using our analysis techniques.

Background
Verification is an important part of the software development process: checking that the design of a system meets the requirements for it. Formal Verification is a mathematical way of doing this - proving the implemented system complies with its requirements documents. Two mathematical descriptions (known as ‘formal specifications’) are needed, one describing the behaviour of the actual system and the other describing the requirements. These techniques have been used to verify software generally, however user interfaces and requirements about ease of use, safety and prevention of human error present new challenges. For infusion pumps this is a critical area as human error can lead to patient harm.

For user interface software, verification involves checking that a formal specification of the interface’s behaviour satisfies a formal specification of usability and other requirements linked to the behaviour of those operating devices (nurses, doctors, patients, etc). The aim is to identify potential issues in the software in advance, in ways that are more reliable than just using testing methods (executing the software on the real device). This is important as subtle issues are hard to discover if only testing of the software is done. Such issues include traditional software bugs but also design problems that would increase the likelihood of people making mistakes when using devices.

Achievements
In collaboration with the FDA, techniques have been developed to generate formal specifications from source code implementations. This is important as it allows those formal specifications to be used in further verification activity to ensure the safety and usability of infusion pumps, for example as part of regulatory checks or as part of a procurement process.

Mathematical descriptions of both usability and safety requirements for infusion pumps have been developed. These are properties that need to be verified to demonstrate that essential safety and performance levels are met by the software design.

The developed techniques have been validated by analysing software incorporated in commercial medical devices from different manufacturers. Specifications were extracted from the source code and these checked mathematically against the requirements.

These techniques have made it possible to identify previously undetected design issues in commercial infusion pumps. These issues have safety implications, as they could lead to accidental misconfiguration of infusion parameters (such as the volume of drug to be administered) and so, ultimately, cause patient harm. The results of the analysis, particularly in relation to data entry, are being used by regulators, device manufacturers, and hospitals to raise awareness about general user interface software issues.

Key people
P Masci, R Ruksenas, H Huang, P. Curzon (QMUL); A Cauchi, A Gimblett, P Oladimeji, H Thimbleby (Swansea University); MD Harrison (Newcastle University); J Campos (Universidade de Minho)

Publications
2014
Campos, J. C., Doherty, G., Harrison, M. D. (2014). Analysing interactive devices based on information resource constraints. International Journal of Human-Computer Studies, 72, 284–297.

Ruksenas, R., Curzon, P., Blandford, A. E., & Back, J. (2014). Combining human error verification and timing analysis: A case study on an infusion pump. Formal Aspects of Computing, 26, 1033–1076.

Harrison, M. D., Masci, P., Campos, J. C., & Curzon, P. (2014). Demonstrating that medical devices satisfy user related safety requirements. Proceedings of the 4th International Symposium on Foundations of Health Information Engineering and Systems with 6th International Workshop on Software Engineering in Healthcare (FHIES/SEHC 2014)

Masci, P., Zhang, Y., Jones, P., Curzon, P., & Thimbleby, H. (2014). Formal verification of medical device user interfaces using PVS. Proceedings of the 17th International Conference in Fundamental Approaches to Software Engineering (FASE 2014)

Masci, P., Oladimeji, P., Curzon, P., & Thimbleby, H. (2014). Using PVSio-web to demonstrate software design issues in medical user interfaces. Proceedings of the 4th International Symposium on Foundations of Health Information Engineering and Systems with 6th International Workshop on Software Enginineering in Health Care (FHIES/SEHC 2014)

Cauchi, A. (2014). Using analytical and empirical techniques for improving medical device number entry systems design. PhD thesis, Swansea University.

Oladimeji, P. (2014). Designing number entry user interfaces: a focus on interactive medical devices. PhD thesis, Swansea University.

2013
Harrison, M. D., Campos, J. C., & Masci, P. (2013). Reusing models and properties in the analysis of similar interactive devices. Innovations in System and Software Engineering.

Masci, P., Ruksenas, R., Oladimeji, P., Cauchi, A., Gimblett, A., Li, Y., Curzon, P., & Thimbleby, H. (2013). The benefits of formalising design guidelines: A case study on the predictability of drug infusion pumps. Innovations in Systems and Software Engineering

Masci, P., Ayoub, A., Curzon, P., Harrison, M. D., Lee, I., & Thimbleby, H. (2013). Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. Proceedings of the Fifth Symposium on Engineering Interactive Computing Systems (EICS 2013), 81–90. New York: ACM. (Among top 3 papers in conference.)

Ruksenas, R., Curzon, P., & Harrison, M. D. (2013). Integrating formal predictions of interactive system behaviour with user evaluation. Proceedings of the 10th International Conference on Integrated Formal Methods (IFM 2013), 238–252. Lecture Notes in Computer Science, vol. 7940. Springer.

Harrison, M. D., Masci, P., Campos, J. C., & 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 (FMIS 2013). Electronic Communications of the EASST, vol. 69. (To appear.)

Ruksenas, 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. (To appear.)

Cauchi, A. (2013). Using differential formal analysis for dependable number entry. Proceedings of the Fifth Symposium on Engineering Interactive Computing Systems (EICS 2013), 155–158. New York: ACM. (Prize for best Doctoral Consortium presentation.)

Masci, P., Zhang, Y., Curzon, P., Harrison, M. D., Jones, P., & Thimbleby, H. (2013). Verification of software for medical device user interfaces in PVS. Technical report.

2012
Cauchi, A., Gimblett, A., Thimbleby, H. W., Curzon, P., & Masci, P. (2012). Safer “5-key” number entry user interfaces using Differential Formal Analysis. Proceedings of the 2012 BCS Conference on Human-Computer Interaction (BCS-HCI 2012), 29–38.

Cauchi, A. (2012). Differential Formal Analysis: Evaluating safer 5-key number entry user interface designs. Proceedings of the 2012 Symposium on Engineering Interactive Computing Systems (EICS'12), 317–320. New York: ACM.

Masci, P., Huang, H., Curzon, P., & Harrison, M. D. (2012). Using PVS to investigate incidents through the lens of distributed cognition. Proceedings of the 4th NASA Formal Methods Symposium (NFM-2012), 273–278. Lecture Notes in Computer Science, vol. 7226. Springer.

Masci, P., Ruksenas, R., Huang, H., Curzon, P. & Harrison, M. D. (2012). Formal verification and the prevention of systematic user error. Paper presented at the Workshop on Formal Methods in Human-Machine Interaction, Imperial College, London, May 2012.

Thimbleby, H., Cauchi, A., & Gimblett, A. (2012). Simulation to evaluate alternative approaches to blocking use errors. Poster presented at Design of Medical Devices Conference (DMD 2012), Minneapolis, April 2012.</li>

2011
Campos, J. C., & Harrison, M. D. (2011). Modelling and analysing the interactive behaviour of an infusion pump. Proceedings of the Fourth International Workshop on Formal Methods for Interactive Systems (FMIS 2011). Electronic Communications of the EASST, vol. 45.

Masci, P, Ruksenas, R., Oladimeji, P., Cauchi, A., Gimblett, A., Li, Y., Curzon, P. & Thimbleby, H. (2011). On formalising interactive number entry on infusion pumps. Proceedings of the Fourth International Workshop on Formal Methods for Interactive Systems (FMIS 2011). Electronic Communications of the EASST, vol. 45.

Ruksenas, R., & Curzon, P. (2011). Abstract models and cognitive mismatch in formal verification. Proceedings of the Fourth International Workshop on Formal Methods for Interactive Systems (FMIS 2011). Electronic Communications of the EASST, vol. 45.

Disclaimer
The information provided on this web page is for academic research purposes only. We make no claims as to the completeness or correctness of this information. We encourage academics and others to experiment with this work and report their results to this web page so that everyone involved may benefit from the work.