Towards Certification by Verification

医疗器械软件的认证是美国食品药品监督管理局的一个主要关注点：对相关公司来说，这是一项昂贵且耗时的工作，而且人们越来越怀疑，随着系统复杂性的增加，目前的认证要求越来越不充分。目前，医疗器械软件的认证是以过程为导向的。人们强烈希望转向更注重产品的方法，但目前还不清楚应该要求什么方法/证据。本研究的目标是表明，现有的正式方法可以适应和增强，使他们可以有效地用于认证过程中。 实现这一目标的研究包括以下三个部分：用户模型的自动生成：对于许多医疗设备来说，可操作性是一个重要的问题，但它并没有明确设计。自动生成用户模型（即，用户需要了解系统的哪些信息才能操作系统）可以在设计的早期阶段评估可操作性，并确保用户模型和机器模型之间的正确对应。 该项目是形式化的用户模型的要求和开发的方法来构建这些模型自动从机器模型。运行时验证：运行时验证可以补充设计时验证时，系统是太复杂，实际上完全验证。运行时分析技术也可以用于性能建模和基于运行时特性的系统改进。 该项目研究了运行时分析在认证过程中的有用性，包括在规范阶段（对从规范生成的模型进行压力测试）和在实际操作中（建立审计跟踪和捕获意外行为）。 该研究是针对开发足够的规范语言和逻辑运行时验证，和有效的数据结构的programinstrument.Case研究：在FDA的要求，沃尔特里德陆军研究所（WRAIR）提供了一个中型医疗设备的要求文件。旨在以该体系为基础，研究面向产品的认证的可行性。 该设备的建模已经开始，并进行了一些初步分析。目标是使用正式的方法来制作一套完整的证明文件，并与FDA合作评估这些文件是否被认为是认证的充分证据。

Certification of medical device software is a major concern for the Food and Drug Administration: it is costly and time-consuming for the companies involved, and there is a growing suspicion that the current certification requirements are becoming more and more inadequate with increasing system complexity. At present certification of medical device software is process-oriented. There is a strong desire to move to a more product-oriented approach, but it is as yet unclear what methods/evidence should be required. The goal of this research is to show that existing formal methods can be adapted and augmented such that they can be used effectively in the certification process. The research to achieve this consists of the following three components:Automatic Generation of User Models:For many medical devices operability is an important concern, but it is not explicitly designed for. Automatic generation of user models (that is, what does the user need to know about the system to be able to operate it) allows evaluation of operability in early stages of the design and guarantees a correct correspondence between user model and machine model. The project is formalizing user model requirements and developing methods to construct these models automatically from the machine model.Run-time Verification: Run-time verification can complement design-time verification when the system is too complex to be realistically verified in full. Run-time analysis techniques can also be used for performance modeling and improvement of the system based on run-time characteristics. The project investigates the usefulness of run-time analysis in the certification process, both in the specification phase(to stress test the model generated from the specification), and in actual operation (to establish audit trails and catch unexpected behaviors). The research is directed at the development of adequate specification languages and logics for run-time verification, and efficient data structures for program instrumentation.Case study: At the request of the FDA, the Walter Reed Army Institute of Research (WRAIR) has made available a requirements document for a medium-sized medical device. It is the intent to use this system as a basis to study the feasibility of product-oriented certification. The modelingof this device has already started and some preliminary analyses have been performed. The goal is to use formal methods to produce a fulll set of proof documents and evaluate, in cooperation with the FDA, whether these documents would be considered adequate evidence for certification.