September 2013:
Paper on the Safety-critical Pacemaker Development accepted for publication at ACM TECS!

August 2013:
Paper on pacemaker verification accepted at the International Journal on Software Tools for Technology Transfer!

April 2012:
Best Student Paper Award at RTAS'12 for the MDD framework paper and UPP2SF!

March 2012:
Best Paper Candidate at TACAS'12 for the paper on pacemaker verification!

January 2012:
Paper on the use of UPP2SF for pacemaker design accepted - IEEE RTAS @CPSWEEK!

Project Overview:


Safety recalls of pacemakers and implantable cardioverter defibrillators due to firmware problems affected over 200,000 devices between 1990 and 2000, comprising 41% of the devices recalled. Nonetheless, the only method currently used to check for correctness of the device pperation is unit testing, where a playback of pre-recorded electrogram signals is used to determine if the input signal triggers a particular pacemaker response. This open-loop "tape" testing is unable to check for safety violations due to inappropriate stimulus by the pacemaker, as in the case of Pacemaker Mediated Tachycardia, where the pacemaker drives the heart into an unsafe state. There is, hence, a need for interactive closed-loop verification and testing of such systems.


Pacemaker operation is affected by the refractory and conduction properties of the heart, which are all timing based. Hence, it is natural to model the device and its interaction with the heart using an extension of the timed-automata formalism, which supports powerful verification techniques. We have created a model-driven development framework for safety-critical implantable cardiac devices that includes:
(a) timed-automata based modeling of the controller (i.e., pacemaker) in UPPAAL, model verification, and model-based estimation of the worst-case execution time;
(b) automatic translation of the model to Simulink/Stateflow using the UPP2SF tool;
(c) testing of the translated model; and
(d) automatic modular code synthesis, and testing on a hardware platform.

To enable the framework, we have developed the UPP2SF model-translation tool for automatic translation of verified models (in UPPAAL) to models that may be simulated and tested (in Simulink). Virtual Heart Model The translation guarantees that verified abstract models over-approximate the detailed models used downstream for simulation and code generation, thus ensuring that the closed-loop safety properties are retained through the tool-chain. Finally, for physiologically relevant testing and verification of implantable cardiac devices, we have designed a Virtual Heart Model that: (a) functionally expresses electrophysiological behavior of a healthy and heart during arrhythmia; (b) is formally structured to interface with both modeled and real pacemakers such that the timing of all activity is verifiable by model checking tools; and (c) unlike existing complex, high-order heart models used in (bio)medical research, enables real-time device simulation, and physical testing using the VHM hardware platform.

Toolchain: From VHM to PVS PVS hardware platform


Miroslav Pajic
Zhihao "Hao" Jiang
Prof. Rajeev Alur
Prof. Insup Lee
Prof. Rahul Mangharam
Prof. Oleg Sokolsky



tumblr hit tracking tool