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.
RELATED WORK
In this paper, the model-based approach is implemented using the Prototype Verification System (PVS). PVS is a state-of-the-art verification tool that provides an expressive specification language based on higher-order logic, a language mechanism for theory interpretation, a verification engine based on automated theorem proving, and a code generator for automatic translation of PVS specifications into executable code.
PVS is only one approach of course, and other tools could have been used to develop the prototype. Our choice was guided by pragmatics linked to best current development practices the need to specify safety requirements independently, expressiveness of the specification language (here, PVS), and auto- mated code generation from verified specifications.
THE GENERIC PCA (GPCA) PUMP
Fig. 1. Schematic of the FDA’s Generic PCA infusion pump prototype.
The FDA has developed a Matlab Simulink/Stateflow model of the Generic PCA (GPCA) pump that captures the core functionalities of PCA pumps in general. The GPCA model has a layered architecture (see Figure 1(a)). The GPCA user interface, as provided with the original model, has the layout shown in Figure 1(b). The user interface includes the following elements: a programming unit and pump console, which renders information about the pump state and allows users to set infusion parameters; and a keypad, which allows users to send commands to the pump.
DEVELOPMENT OF THE GPCA USER INTERFACE
Fig. 2. The adopted model-based development approach.
A GPCA user interface (hereafter, GPCA-UI) prototype is now developed using a model-based approach. Within model-based development approaches, models are used as primary artefacts during the whole development cycle: they present a design specification that can be checked against given requirements, and then code generation techniques are used to transform the model into a concrete implementation for a specific platform. The adopted model-based development approach consists of the following phases (as shown in Figure 2).
Fig. 3. The GPCA-UI prototype.
The GPCA-UI prototype can be downloaded. The prototype architecture is split into a front-end and a back-end, as shown in Figure 3(a). The front-end is deployed on a tablet, which makes it possible to do realistic interaction with the buttons on the user interface. The back-end is deployed on a server with the PVSio prototyping environment.
Listing 1.4. Proof obligation.
Given this theory interpretation, PVS automatically generates the proof obli- gation in Listing 1.4, which then needs to be discharged. The proof obligation requires we show that, for all reachable states, it is always true that the display and the VTBI range have values between v min and v max (0–99999 in this case).
CONCLUSIONS
Making medical devices safer involves a constructive dialogue among stakeholders (manufacturers, regulators, clinicians), and a verification approach based on these generic models can help to make this dialogue precise, as well as having the advantages of being computerized and runnable.
We have presented a model-based development approach for building a realistic user interface for the GPCA pump prototype. Although the user interface is a research prototype and not a real medical device, the functionalities and level of detail used in the specification are very similar to those of commercial PCA pumps. Because of this, it is evident that the specification can be used as a realistic workbench, and the model-based developed approach used can in principle be used as part of the development of real medical device user interfaces.
The model-based approach incorporates several concepts promoted by medical device regulators and which should be directly applicable to the development of real medical devices. For instance, the FDA Office of Science and Engineering Lab (OSEL) engineers have promoted the formalisation of safety requirements as generic models that can be used for verification of real devices.
The model-based approach introduced here has some limitations that need to be considered and should be the subject of further work: the formalisation of safety requirements as predicates does not allow a formal verification of the consistency of the safety requirements (e.g., contradictory safety requirements can be formalised); the verification technique based on theory interpretation allows the creation of mappings that are syntactically correct but semantically wrong (e.g., visible display elements of the reference model can be mapped into state variables of the concrete model that are not rendered on the display); code generation is limited to Lisp code (new code generators that translate PVS models into C and Java are still under development). Further work is needed to demonstrate the approach for the entire user interface (we have illustrated the approach just for the data entry system). We have started to explore solutions to these limitations.
Source: University of Pennsylvania
Authors: Paolo Masci | Anaheed Ayoub | Paul Curzon | Insup Lee | Oleg Sokolsky | Harold Thimbleby
>> 200+ Matlab Projects based on Control System for Final Year Students