Reasoning of Safety-Critical Medical Devices using Formal Methods.
Raoul Praful Jetley · NCSU Libraries Repository (North Carolina State University Libraries) · 2003
The design and functional complexity of medical devices have increased during the past 50 years, evolving from the use of a metronome circuit for the initial cardiac pacemaker to functions that include electrocardiogram analysis, laser surgery, and intravenous delivery systems that adjust dosages based on patient feedback. As device functionality becomes more intricate, concerns arise regarding efficacy, safety and reliability. It thus becomes imperative to adopt a standard or methodology to ensure that the possibility of any defect or malfunction in these devices is minimized. It is with these facts in view that regulatory bodies are interested in investigating mechanisms to certify such medical devices. These organizations advocate the use of formal method techniques to evaluate safety-critical medical systems. The use of formal methods is keenly debated though, with most manufacturers claiming that they are arduous and time-consuming. In this thesis, we evaluate the feasibility of formal method techniques for medical devices. More specifically, we discuss our experiences in modeling and verification of the specifications for a typical medical system called the Computer Aided Resuscitation Algorithm (CARA) using two formal methods based tools, UPPAAL and Spin.