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 (INa, Is, Ix1 , and IK1) 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.