NDLI: Closed-loop verification of medical devices with model abstraction and refinement

Content Provider	Springer Nature Link
Author	Jiang, Zhihao Pajic, Miroslav Alur, Rajeev Mangharam, Rahul
Copyright Year	2013
Abstract	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.
Starting Page	191
Ending Page	213
Page Count	23
File Format	PDF
ISSN	14332779
Journal	International Journal on Software Tools for Technology Transfer
Volume Number	16
Issue Number	2
e-ISSN	14332787
Language	English
Publisher	Springer Berlin Heidelberg
Publisher Date	2013-09-24
Publisher Place	Berlin, Heidelberg
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Medical devices Implantable pacemaker Software verification Cyber-physical systems Model abstraction and refinement CEGAR Software Engineering Software Engineering/Programming and Operating Systems Theory of Computation
Content Type	Text
Resource Type	Article
Subject	Information Systems Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

An abstraction refinement approach combining precise and approximated techniques

Data-abstraction refinement: a game semantic approach

Relating software validation to technology trends

Local abstraction–refinement for the μ-calculus

Parameterized verification through view abstraction

Don’t care in SMT: building flexible yet efficient abstraction/refinement solvers

Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure

Cyber-physical modeling of implantable cardiac medical devices (2012)

αSPIN: A tool for abstract model checking

Closed-loop verification of medical devices with model abstraction and refinement

Similar Documents

An abstraction refinement approach combining precise and approximated techniques

Data-abstraction refinement: a game semantic approach

Relating software validation to technology trends

Local abstraction–refinement for the μ-calculus

Parameterized verification through view abstraction

Don’t care in SMT: building flexible yet efficient abstraction/refinement solvers

Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure

Cyber-physical modeling of implantable cardiac medical devices (2012)

αSPIN: A tool for abstract model checking

Closed-loop verification of medical devices with model abstraction and refinement