HeartVerify

HeartVerify is a framework for the analysis and verification of pacemaker software and personalised heart models. Models are specified in MATLAB Stateflow and are analysed using Cosmos tool that implements, amongst others, statistical model checking. This approximate verification method is based on the sampling of system's trajectories followed by their statistical analysis, and enables the analysis of complex nonlinear dynamics of the heart, where precise (numerical) verification methods typically fail. One important feature of HeartVerify is its modularity, which allows configuring and testing different heart and pacemaker models in a plug-and-play fashion, without changing their communication interface or the verification engine. HeartVerify supports the verification of probabilistic properties, together with additional analyses such as simulation, generation of probability density function plots (see figure) and parametric analyses.

Our HeartVerify tool won the Valuable Artifact Prize 2015!

To know more about usage and features of HeartVerify, download the technical report below.

Parameter synthesis

Verification is useful in establishing key correctness properties of cardiac pacemakers, but has limitations, in that it is not clear how to redesign the model if it fails to satisfy a given property. Instead, parameter synthesis aims to automatically find optimal values of parameters to guarantee that a given property is satisfied. Our work focuses on synthesising pacemaker parameters that are safe, robust and, at the same time, able to optimise a given quantitative requirement such as energy consumption or patient's clinical indicators. We solve this problem by combining symbolic methods (SMT solving) for ruling out parameters that violate heart safety (red areas in the figure) with approximate methods and sampling for optimising the quantitative requirement.

Hardware-in-the-loop energy optimisation

Though not critical for patient's life, energy efficiency of cardiac pacemakers is crucial because it reduces the frequency of device re-implantations, thus improving patients' quality of life. To achieve effective energy optimisation, we take a hardware-in-the-loop (HIL) simulation approach: the pacemaker model is encoded into hardware and interacts with a computer simulation of the heart model. In addition, a power monitor is attached to the pacemaker to provide real-time power consumption measurements. We realise a fully automated optimisation workflow, where HIL simulation is used to build a probabilistic power consumption model from power measurement data. Thus obtained model is used by the optimisation algorithm to find pacemaker parameters that e.g., minimise consumption or maximise battery lifetime. To prevent optimal parameters violating heart safety, we additionally employ parameter synthesis methods so as to restrict the search for parameters to those that guarantee a given safety property.