Towards Certification by Verification

医疗设备软件的认证是食品和药物管理局关注的主要问题：对于涉及的公司来说，这是昂贵和耗时的，并且越来越多的人怀疑，随着系统复杂性的增加，当前的认证要求正变得越来越不充分。目前，医疗器械软件认证是流程化的。人们强烈希望转向一种更以产品为导向的方法，但目前还不清楚应该需要什么方法/证据。这项研究的目的是表明，现有的正式方法可以调整和增强，以便它们可以在认证过程中有效地使用。实现这一目标的研究包括以下三个组成部分：用户模型的自动生成：对于许多医疗设备来说，可操作性是一个重要的问题，但它并没有明确的设计。用户模型的自动生成（即用户需要了解系统的哪些信息才能操作系统）允许在设计的早期阶段对可操作性进行评估，并保证用户模型与机器模型之间的正确对应。该项目正在形式化用户模型需求，并开发从机器模型自动构建这些模型的方法。运行时验证：当系统过于复杂而无法实际地完全验证时，运行时验证可以补充设计时验证。运行时分析技术还可以用于基于运行时特征的系统性能建模和改进。该项目调查了运行时分析在认证过程中的有用性，无论是在规范阶段（对从规范生成的模型进行压力测试），还是在实际操作中（建立审计跟踪并捕获意外行为）。该研究的目的是开发用于运行时验证的适当规范语言和逻辑，以及用于程序检测的有效数据结构。案例研究：应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.