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

有效的医疗器械验证和确认(V&amp；V；V)流程、技术和工具将在使FDA能够履行其仅批准安全有效的医疗器械的任务方面发挥重要作用。然而，需要做大量的工作来开发V&amp；V技术和认证流程，以应对和鼓励医疗设备正在发生的信息、金融和科学服务领域的革命性变化。与过去系统的单片化性质不同，现代计算和信息系统倾向于高度组件化，并通过即插即用？灵活集成组件来强调定制。(PnP)和面向服务的体系结构。在医疗设备领域，由于大量的验证挑战，缺乏接口和体系结构的标准，以及缺乏批准组件化的安全关键医疗设备的明确流程和技术，系统在很大程度上仍然是单一的。如果这些领域没有实质性的进展，医疗器械和医疗保健领域的创新将受到严重抑制，随着制造商不断将更新技术引入医疗器械市场，不安全设备进入市场的风险将会增加。该项目开发了一套新功能，集成在名为茂物/基桑的工具框架中，用于普遍规范、分析和测试基于组件的嵌入式系统，预计这些系统将与即插即用医疗器械系统的V&Amp；V非常相关。这些功能包括：Java的接口规范和验证框架，允许使用模型检查和轻量级定理证明技术指定和自动检查复杂的前置/后置条件和不变量；从规范自动生成单元测试用例，使源代码检查技术能够更直接地与现有以测试为中心的质量保证机制集成；可扩展的静态分析技术，用于计算程序依赖和信息流，可用于推理系统耦合、自动派生可跟踪性信息，以及检测和可视化表现为不正确信息流的安全缺陷。NSF-FDA研究项目的重点是将这些工具应用于FDA工程师正在设计的PNP框架原型。目标是扩展现有的V&A；V；V

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.