Journal
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER
Volume 16, Issue 2, Pages 191-213Publisher
SPRINGER HEIDELBERG
DOI: 10.1007/s10009-013-0289-7
Keywords
Medical devices; Implantable pacemaker; Software verification; Cyber-physical systems; Model abstraction and refinement; CEGAR
Categories
Funding
- Direct For Computer & Info Scie & Enginr
- Division Of Computer and Network Systems [0923518] Funding Source: National Science Foundation
- Division Of Computer and Network Systems
- Direct For Computer & Info Scie & Enginr [1253842] Funding Source: National Science Foundation
Ask authors/readers for more resources
The design and implementation of software for medical devices is challenging due to the closed-loop interaction with the patient, which is a stochastic physical environment. The safety-critical nature and the lack of existing industry standards for verification make this an ideal domain for exploring applications of formal modeling and closed-loop analysis. The biggest challenge is that the environment model(s) have to be both complex enough to express the physiological requirements and general enough to cover all possible inputs to the device. In this effort, we use a dual chamber implantable pacemaker as a case study to demonstrate verification of software specifications of medical devices as timed-automata models in UPPAAL. The pacemaker model is based on the specifications and algorithm descriptions from Boston Scientific. The heart is modeled using timed automata based on the physiology of heart. The model is gradually abstracted with timed simulation to preserve properties. A manual Counter-Example-Guided Abstraction and Refinement (CEGAR) framework has been adapted to refine the heart model when spurious counter-examples are found. To demonstrate the closed-loop nature of the problem and heart model refinement, we investigated two clinical cases of Pacemaker Mediated Tachycardia and verified their corresponding correction algorithms in the pacemaker. Along with our tools for code generation from UPPAAL models, this effort enables model-driven design and certification of software for medical devices.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available