CHI+MED logo banner

Model-Based Design of User Interface Software

Key points
We have:

  • Worked with the US Food and Drug Administration (FDA) to create tools that support the model-based design of user interfaces.
  • Shown that using them can lead to design problems being found early in the design process when they are cheap to fix.

Model-based design is a process for developing a system from design specifications written in a mathematically precise language. For user interface software, it involves:

  • Verifying the design specifications against given usability, safety and security requirements.
  • Generating a software implementation of the interface from those design specifications using code generation techniques.

When using rigorous techniques for verification and code generation, the generated software code automatically satisfies the same requirements verified for the design specifications.

GPCA pump prototype

Figure 1: Screenshot of the GPCA pump prototype executed within PVSio-web

In collaboration with the FDA, we have developed tools and techniques to support rigorous model-based design of user interface software of infusion pumps and other interactive medical devices. Using our approaches, we contributed to the development of the Generic Patient Controlled Analgesia Pump (GPCA). We also demonstrated how potential design issues can be identified early in the design process, and so fixed before expensive design commitments are made.

Key people
P Masci, P Curzon (QMUL); A Cauchi, A Gimblett, P Oladimeji, H Thimbleby (Swansea University); I Lee, O Sokolsky, A Ayoub (University of Pennsylvania)

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. Proceedings of 32nd International Conference on Computer Safety, Reliability and Security (SAFECOMP 2013)

Oladimeji, P., Masci, P., Curzon, P., & Thimbleby, H. (2013). PVSio-web: A tool for rapid prototyping device user interfaces in PVS. Proceedings of the 5th International Workshop on Formal Methods for Interactive Systems (FMIS 2013). Electronic Communications of the EASST, vol 69 (To appear.)

Thimbleby, H., & Gimblett, A. (2011). Dependable keyed data entry for interactive systems. Proceedings of the Fourth International Workshop on Formal Methods for Interactive Systems (FMIS 2011). Electronic Communications of the EASST, vol. 45

Thimbleby, H., Gimblett, A., & Cauchi, A. (2011). Buffer Automata: a UI architecture prioritising HCI concerns for interactive devices. Proceedings of the 3rd Symposium on Engineering Interactive Computing Systems (EICS'11), 73–78. New York: ACM.

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.


Masci, P., Zhang, Y., Jones, P., Thimbleby, H., & Curzon, P. (2014). A generic user interface architecture for analyzing use hazards in infusion pump software. Proceedings of the 5th Workshop on Medical Cyber-Physical Systems (MCPS 2014), 1–14. OASIcs: Open Access Series in Informatics, vol. 36. pdf (1.2 MB) doi bibtex abstract