| High Confidence Medical Device Software and Systems |
|
The development and production of medical device software and systems is a critical issue as medical device software is increasingly sophisticated and medical devices are networked. Of particular importance is how to ensure such medical device systems are safe.
Paper: ProjectsGIPThe goal of the Generic Infusion Pump (GIP) project is to develop a set of models and reference specifications of generic infusion pumps to verify the correct functioning of software for different types of infusion pumps submitted for FDA approval. The project defines a reference specification of a generic infusion pump which device manufacturers could use to develop more specialized pumps.Our process of building these formal models starts with requirements elicitation and hazard analysis. These requirements and hazards are used in building the formal models as extended finite state machines and to create properties which are checked against the EFSM models using model checkers. So far we have gathered informal requirements and done a hazard analysis for a generic large volume pump model as well as the additional requirements and hazards to extend this large volume model to cover patient controlled analgesia (PCA) infusion pumps. We plan to use these models and properties to generate tests which can be used for conformance testing infusion pump implementations. Our future work will focus on extending these pump models with additional safety requirements and exploring the use of test generation for conformance testing real pump implementations. Using a recognized reference specification would allow device manufacturers to concentrate on the specialized functionality of their particular pump devices and simplify the verification process. Papers:
MD PnPThe Medical Device "Plug-and-Play" Interoperability (or MD PnP) program is a inter-disciplinary, multi-institutional program committed to advancing medical device interoperability to improve patient safety and healthcare efficiency. Networked medical device systems will support the widespread clinical use of medical data and enable medical device integration, to produce complete and accurate electronic health records, create error-resistant systems, and reduce healthcare costs."from mdpnp.org We have been involved in the project for several years building sample implementations of various interoperability systems. We have also been involved in the development of the Interconnecting the Clinical Environment (ICE) proposed standard. The demo systems we helped develop have been exhibited at the American Society of Anesthesiologists (ASA) annual conference in 2006 and 2007, HIMSS 2007 and 2008, and the CIMIT Innovation Congress in 2006 and 2007. The MD PnP team received the 2007 CIMIT Edward M Kennedy award and our demo was awarded first place at the ASA Scientific Exhibition in 2007. Papers:
The project homepage is located at http://www.mdpnp.org/
Pacemaker ChallengeOne of the major research avenues in this project targets pacemakers, a life-critical implantable device. Starting from the informal requirements for a pacemaker, provided by the vendor Boston Scientific, we are undertaking a model-driven development effort that will result in a working prototype of the pacemaker, supplemented by an assurance case that provides evidence that the developed prototype is safe. To date, we have developed a model of the digital controller of the pacemaker that supports all operational modes specified in the requirements, providing complete traceability from the requirements to the model elements. That is, for each model element such as a state transition, we identified a paragraph in the requirements document that justifies the model element. This mapping from requirements to the model forms an important part of the assurance case. We then proved, using the state-of-the-art verification tool UPPAAL, that the controller model satisfies some of the high-level properties listed in the requirements document, as well as other critical properties that were identified through the dialogue with Brian Larson, a developer at Boston Scientific.On-going efforts target generation of executable code for a particular embedded microprocessor and extending the assurance case to cover the generated code.
AHLTA-MobileOne of the major sources of failures in medical device systems is human error. Nurses, who often lack extensive technical background, misunderstand the device interface and misinterpret instructions given by the device. Safety assurance for medical devices is impossible without making them more robust to human error. An important direction of research in this project is establishing whether operation of the device is consistent with the mental model that a typical user of the device has. The technical approach is to consider mental models represented as finite state machines with transitions labeled by user interface elements of the device. Once such a model is constructed, the verification problem is to determine, whether the device operation is consistent with the model. Research concentrates on two approaches to determine consistency. One uses model-based testing, where tests are generated from the model and applied to the device. A more ambitious direction is to automatically extract an abstraction of the device operation from the source code of the embedded device software. Then, consistency can be established using well-known notions of state machine equivalence and refinement.A feasibility study concentrates on a handheld point-of-injury data collection device, developed by TATRC, the U.S. Army medical research center. The project team, in collaboration with device developers, is constructing the mental model of the device user and is developing the means of model extraction based on the static analysis of the source code.
BloodbankPolicy documents contain rules that must be adhered to when implementing policy. The Food and Drug Administration (FDA) has created rules or regulations for blood bank organizations which are contained in the Code of Federal Regulations (CFR). These documents are written in natural language which makes them prone to under-specifications, conflicts, ambiguities, etc. This makes the extraction of an algorithmic procedure difficult and error prone.Our case study identified inconsistencies in the document and implementation using domain knowledge and an extracted formal model which has a high degree of traceability to the document. This model was checked for internal inconsistency and totality using existing boolean satisfiability checkers. The case study also explained a testing procedure to check for conformance of an implementation to the policy. Conformance failure can be traced back to the policy document using the formal model. We used the tests generated from the model to check a blood bank software implementation against the regulations. We discovered several problems in the implementation, mostly corresponding to areas of ambiguity in the regulations.
These projects are being supported in part by NSF CNS-0834524 and TATRC/FDA grant MIPR-6MRXMM-6093, and were supported in part by NSF-CNS-0610297 (FDA SIR), NSF CNS-0509327, and ARO URI DAAD19-01-1-0473. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the sponsoring agencies. |
