| Search the Collection|Browse Subjects|Services|Library Information|Community |News & Events | |
|
|
|
|
|
|
|
|
||||
|
|||||||
Type of Document Master's Thesis Author Jetley, Raoul Praful, Author's Email Address rpjetley@unity.ncsu.edu URN etd-07052002-164931 Title Reasoning of Safety-Critical Medical Devices using Formal Methods. Degree Master of Science Graduate Program Computer Science Advisory Committee
Advisor Name Title DR. S. PURUSHOTHAMAN IYER Committee Chair DR. ANNIE I. ANTÓN Committee Member DR. JOHN W. BAUGH Committee Member Keywords
- automata
- verification
- specification
- analysis
- modeling
- formal methods
- WRAIR
- FDA
Date of Defense 2002-06-26 Availability unrestricted Abstract 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 medical bookkeeping, 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 the regulatory bodies are interested in investigating mechanisms by which to certify such medical devices. These organizations believe that the rigorous employment of formal mathematical models can achieve significant software quality over current practice, and advocate the use of formal methods 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, titled ?Reasoning of Safety-Critical Medical Devices using Formal Methods?, 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.
We find that the use of UPPAAL and Spin for the analysis of the CARA system yields several
anomalies and inconsistencies, hitherto undetected. The results from the two tools are found to be in accordance, and the effort involved comparable to conventional techniques. Based on our results, we conclude that formal methods provide a feasible and effective means for reasoning of safety-critical medical devices.
Files
Filename Size Approximate Download Time (Hours:Minutes:Seconds)
28.8 Modem 56K Modem ISDN (64 Kb) ISDN (128 Kb) Higher-speed Access etd.pdf 1.20 Mb 00:05:31 00:02:50 00:02:29 00:01:14 00:00:06