Development of an Open Test-bed for Application of Formal Methods to Plug and Play Medical Devices

点击翻译按钮获取中文摘要

Effective processes, techniques, and tools for Verification and Validation (V&V) of medical devices will play a significant role in enabling FDA to carry out its mandate of approving only safe and effective medical devices. However, much work is needed to develop V&V techniques and certification processes that can cope with and encourage the same revolutionary changes in medical devices that are occurring informational, financial, and scientific service domains. In contrast to the monolithic nature of past systems, modern computing and information systems tend to be highly componentized and emphasize customization through flexible integration of components via ?plug-and-play? (PnP) and service-oriented architectures. In the medical device domain, systems are still largely monolithic due to the substantial verification challenges, absence of standards for interfaces and architectures, and lack of clear processes and techniques for approving componentized safety-critical medical devices. Without substantial progress in these areas, innovations in medical devices and health care will be severely inhibited and the risk of introducing unsafe devices into the market will increase as manufacturers continue to push newer technologies into medical devices.This project has developed a suite of new capabilities, integrated in a tool framework called Bogor/Kiasan for pervasive specification, analysis, and testing of component-based embedded systems that are expected to be very relevant for V&V of PnP medical device systems. These capabilities include: interface specification and verification frameworks for Java that allow complex pre/post-conditions and invariants to be specified and automatically checked using model-checking and lightweight theorem-proving technologies; automated unit test case generation from specifications that enable the source code checking technologies to be more directly integrated with existing testing-centric quality assurance mechanisms; scalable static analysis techniques for calculating program dependences and information flow that can be used to reasoning about system coupling, to automatically derive traceability information, and to detect and visualize security flaws that are manifested as improper information flows. The focus of this NSF-FDA research project is the application of these tools to a PnP framework prototype that is being designed by FDA engineers. The goal is to extend existing V&V processes and techniques to better support development of safe and effective medical device systems that utilize current and emerging component, networking, and plug-and-play technologies, and also to verify that the associated implementation conforms to specifications, to generate test suites to achieve coverage requirements associated with device approval, and to improve the evidence produced to document results of certification activities.