Modeling Cardiac Pacemakers With Timed Coloured Petri Nets And Related Tools

Abstract

Verification Grand Challenge is one of the Grand Challenges for Computing Research. Verification, which is the strict proof of the correctness of software according to its specifications, results in reliable software and potential cost reductions. In addition, the capabilities of other software engineering techniques, such as requirements analysis and testing, can be complemented and extended by verification. Medical devices are well-known examples of safety-critical systems which require significant advances in verification (among other areas). The failure of safety-critical systems not only damages property or the environment but could also lead to human fatality. Therefore, software verification is one approach to prevent such negative consequences. The cardiac pacemaker is an electronic device that monitors and controls the heart rhythm via sensing and pacing operations. The pacemaker treats cardiac arrhythmia, defined as abnormal patterns of the heartbeat. The Software Quality Research Laboratory at McMaster University proposed the pacemaker system specification as a pilot problem for the Verified Software Initiative. This research utilizes formal methods to model and verify the interdisciplinary requirements of pacemaker systems. It additionally provides customizable data to assess and optimize various algorithms and parameters.