A A A
CHI+MED logo banner
Loading

PVSio-web: a tool for prototyping interactive medical systems
from mathematical models

Key points

  • Our prototyping tool, PVSio-web, helps check the safety of designs of devices.

  • It supports design teams, regulators, and hospital training and procurement staff.

  • It supports a model-based design process: that is, it is based on precise mathematical descriptions of the device’s behaviour.

  • Working with the US regulator, the Food and Drug Administration (FDA), our tool has helped identify problems in a series of commercial medical devices.

  • Hospitals have used it as part of training programmes highlighting safety-related design issues.

Figure 1: Screenshot of the PVSio-web prototyping environment.

The PVSio-web Tool
Tools that help manufacturers and regulators rigorously check both prototypes and final designs of devices are vital if using those devices could lead to safety issues. PVS is one industry standard tool used for checking systems that need such high levels of assurance. It is used within a model-based design process: a mathematical description of the way a device behaves (a model) is checked against similar descriptions of what it should do.

We extended PVS with a sophisticated graphical front-end, called PVSio-web (see Figure 1). It makes it easy to create and check realistic prototypes of a device, focussing on the interface that doctors, nurses or patients must interact with. The prototypes have the appearance and behaviour of the real system being analysed. Their behaviour is generated from mathematical descriptions (i.e., models).

We took a pragmatic approach to the rapid generation of prototypes. A picture of the real system, or if early in the development, a design mock up, is used to give the prototype’s appearance. The developer creates programmable areas over interactive parts, like the buttons and displays. The prototype’s behaviour in these programmable areas is given by the mathematical model. Its behaviour is demonstrated or explored by clicking on buttons in the picture, with the results of the interactions seen immediately on the display areas of the picture.

PVSio-web combines different views of the device designed for people with different roles and background. This allows a development team and their stakeholders to work together using a single mathematical model. One view, designed for domain specialists and end users, allows them to explore the behaviour of the prototype. Developers normally create and edit designs using a graphical notation such as Statecharts. The tool therefore provides an editor for a notation based on Statecharts, with the mathematical models created automatically from these design drawings. Another view allows formal methods experts to edit the description of the device’s behaviour and do simple checks on it (type-checking). They can also draw on more powerful verification tools for checking the design behaves in the way required.

While our focus has been on medical devices we have put a lot of effort into creating a tool that is generally useful and usable by a wide range of stakeholders in different ways and this appears to have been successful:

 


"The PVSIO web page is a generally user friendly interface that enhances the value and use of (a very complicated theorem-proving) tool in academia and outside - in the medical device industry sector and other industry sectors, NASA and other government agencies, some manufacturing companies – it has broad impact." - US government stakeholder


 

PVSio-web is particularly suitable for presenting mathematical properties and the results of checking them to engineers and domain specialists in a way that is easy to understand. It is also good for checking assumptions made in the formal models before analysis. It can finally be used in a design process centred around people, allowing early evaluation of prototypes with the people who will have to use the device.

Application and Impact
We have successfully used PVSio-web in several different ways.

  • We have demonstrated previously undetected software defects in commercial medical devices that have safety implications.

  • We have validated mathematical versions of a set of safety/usability requirements for infusion pumps.

  • We created training material to help manufacturers, regulators, clinicians, and procurement staff identify design issues, before expensive design commitments are taken and/or before the final product is placed on the market. It has also been used as part of a hospital training programme for clinicians about device problems.

International research groups are exploring applications of our tool to the analysis of real case studies. For example

  • The US FDA is using it to check medical device user interfaces.

  • Honeywell is using it to check flight decks,

  • Universities are using it to teach interactive and safety-critical systems.

PVSio-web was downloaded over 1,600 times in 2014 alone and is available with the main PVS distribution from SRI International.

Key people
Paolo Masci, Paul Curzon (QMUL), Patrick Oladimeji Harold Thimbleby (Swansea)

Publications
M.D. Harrison, P. Masci, J.C. Campos, and P. Curzon. Demonstrating that medical devices satisfy user related safety requirements. In 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (FHIES2014), 2014.

P. Masci. Design issues in medical user interfaces.

P. Masci, A. Ayoub, P. Curzon, I. Lee, O. Sokolsky, and H. Thimbleby. Model based development of the generic PCA infusion pump user interface prototype in PVS. In Computer Safety, Reliability, and Security (SafeComp2013), volume 8153 of Lecture Notes in Computer Science, pages 228-240. Springer Berlin Heidelberg, 2013.

P. Masci, P. Oladimeji, P. Curzon, and H. Thimbleby. Tool demo: Using PVSio-web to demonstrate software issues in medical user interfaces. In 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (FHIES2014), 2014.

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

P. Masci, Y. Zhang, P. Jones, P. Curzon, and H. Thimbleby. Formal verification of medical device user interfaces using PVS. In 17th International Conference on Fundamental Approaches to Software Engineering (ETAPS/FASE2014), Berlin, Heidelberg, 2014. Springer-Verlag.

P. Masci, Y. Zhang, P. Jones, P. Oladimeji, E. D'Urso, C. Bernardeschi, P. Curzon, and H. Thimbleby. Combining PVSio with Stateflow. In Proceedings of the 6th NASA Formal Methods Symposium (NFM2014), Berlin, Heidelberg, April-May 2014. Springer-Verlag.

P. Oladimeji, P. Masci, P. Curzon, and H. Thimbleby. Pvsio-web: a tool for rapid prototyping device user interfaces in PVS. In 5th International Workshop on Formal Methods for Interactive Systems (FMIS2013), 2013.