Towards Certification by Verification

走向验证认证

• 批准号: 0209237
• 负责人: Zohar Manna
• 金额: $ 9.3万
• 依托单位: Stanford University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-10-01 至 2005-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0209237&HistoricalAwards=false
• 关键词: Towards; Certification; Verification

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.

医疗设备软件的认证是食品药品监督管理局的主要关注点：对于所涉及的公司而言，这是昂贵且耗时的，并且人们越来越怀疑当前的认证要求随着系统复杂性的增加而变得越来越不足。目前，医疗设备软件的认证面向过程。人们强烈希望采用更面向产品的方法，但是目前尚不清楚应需要哪些方法/证据。这项研究的目的是表明可以对现有的正式方法进行调整和增强，以便可以在认证过程中有效使用它们。 实现此目的的研究由以下三个组成部分组成：自动生成用户模型：对于许多医疗设备可操作性是一个重要的问题，但并未明确设计。自动生成用户模型（即用户需要了解的系统以便能够操作它）允许在设计的早期阶段评估可操作性，并保证用户模型和机器模型之间的正确对应关系。 该项目正在正式化用户模型要求和开发从机器模型自动构建这些模型的方法。运行时间验证：运行时验证可以在系统太复杂而无法实现完整验证时进行补充设计时间验证。运行时分析技术也可以根据运行时特征来进行性能建模和改进系统。 该项目在认证过程中调查了运行时分析的有用性，包括在规范阶段（压力测试从规范生成的模型）和实际操作（以建立审计跟踪并捕获意外行为）。 该研究针对开发适当的规范语言和逻辑进行运行时验证，以及用于程序仪器的有效数据结构。Case研究：应FDA的要求，Walter Reed陆军研究所（WRAIR）为中型医疗设备提供了要求。目的是将该系统用作研究面向产品认证的可行性的基础。 该设备的建模已经启动，并且已经进行了一些初步分析。目的是使用正式方法来制作一套Fulll证明文件，并与FDA合作评估这些文件是否被认为是足够的证据进行认证。