Skip to main content
Article
Model-Based Development of the Generic PCA Infusion Pump User Interface Prototype in PVS
Lecture Notes in Computer Science: Computer Safety, Reliability, and Security
  • Paolo Masci, Queen Mary University of London, UK
  • Anaheed Ayoub, University of Pennsylvania
  • Paul Curzon, Queen Mary University of London, UK
  • Insup Lee, University of Pennsylvania
  • Oleg Sokolsky, University of Pennsylvania
  • Harold Thimbleby, Swansea University, UK
Date of this Version
9-1-2013
Document Type
Conference Paper
Comments

32nd International Conference on Computer Safety, Reliability and Security (SAFECOMP 2013), Toulouse, France, September 24-27, 2013.

Abstract
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.
DOI
10.1007/978-3-642-40793-2_21
Copyright/Permission Statement
The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-40793-2_21
Keywords
  • Formal methods,
  • Model-based development,
  • Medical devices,
  • User interface prototyping
Citation Information
Paolo Masci, Anaheed Ayoub, Paul Curzon, Insup Lee, et al.. "Model-Based Development of the Generic PCA Infusion Pump User Interface Prototype in PVS" Lecture Notes in Computer Science: Computer Safety, Reliability, and Security Vol. 8153 (2013) p. 228 - 240
Available at: http://works.bepress.com/sokolsky/83/