CMACS Researchers Perform First Automated Formal Analysis of Realistic Cardiac Cell Model

January 26, 2011

In a multi-institutional effort led by Radu Grosu and Ezio Bartocci of Stony Brook University, Flavio Fenton of Cornell University, and Colas Le Guernic of New York University, CMACS researchers have succeeded in carrying out the first automated formal analysis of a realistic cardiac cell model. The model in question is the Minimal Cardiac Cell Model of Fenton and colleagues, and the analysis performed involved determining the parameter ranges that lead to loss of excitability, a precursor to cardiac disorders such as ventricular tachycardia and fibrillation. Key to the approach was to first transform Fenton's minimal model into a multiaffine hybrid automaton, a modeling paradigm commonly used in the analysis of Genetic Regulatory Networks. This allowed the researchers to leverage tools developed for GRNs to successfully identify the parameter ranges of interest. A paper describing the research has been submitted for publication in a leading Computer Science modeling and verification conference.