Towards Certification by 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.