Toward provably correct models of ventricular cell function

Researchers in cardiac mechanics and electrophysiology develop computer models for analyzing complex experimental data. A key issue is model correctness: formally verifying that the model is performing as intended. We present an application of formal software engineering methods to an established electrophysiology model: the Beeler-Reuter (B-R) model of the mammalian ventricular myocyte. A formal specification fragment for the B- R model is developed, which captures the key drivers of the transmembrane potential, including four ionic currents (I_Na, I_s, I_x1, and I_k1) and a representation for the intracellular calcium ion concentration ( [Ca] ). Correctness- preserving transformations can be used to refine the specification into executable code, thereby assuring a provably correct implementation. The mathematical and logical tools presented here provide a rigorous approach to proving the correctness of ventricular cell models, thereby improving program implementation and verification.