Formalizing the Cardiac Pacemaker Resynchronization Therapy

For many years, formal methods have been used to design and develop critical systems in order to guarantee safety and security and the correctness of desired behaviours, through formal verification and validation techniques and tools. The development of high confidence medical devices such as the cardiac pacemaker, is one of the grand challenges in the area of verified software that need formal reasoning and proof-based development. This paper presents an example of how we used previous experience in developing a cardiac pacemaker using Event-B, to build an incremental proof-based development of a new pacemaker that uses Cardiac Resynchronization Therapy (CRT), also known as biventricular pacing or multisite pacing. In this work, we formalized the required behaviours of CRT including timing constraints and safety properties. We formalized the system using Event-B, and made use of the included Rodin tools to check the internal consistency with respect to safety properties, invariants and events. The system behaviours of the proven model were validated through the use of the ProB model checker.