Cookies on this website

We use cookies to ensure that we give you the best experience on our website. If you click 'Accept all cookies' we'll assume that you are happy to receive all cookies and you won't see this message again. If you click 'Reject all non-essential cookies' only necessary cookies providing core functionality such as security, network management, and accessibility will be enabled. Click 'Find out more' for information on how to change your cookie settings.

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.


Conference paper

Publication Date





657 - 660