Runtime verification of pacemaker using fuzzy logic and colored Petri-nets

Pacemaker is one of medical devices implanted in patients´ bodies helping their health. It is important to certify accuracy and efficiency of the implanted device in all situations. If the device´s software acts improperly, the patient´s life will be threatened. As there may be a bug in the medical device´s software, software verification is critical. Runtime software verification implies considering requirements of the end users while using the software. In this paper, we present a method to verify the pacemaker behavior. This method considers the fuzzy function of the pacemaker. Using Petri-net (PN) for software verification in addition to simplifying demonstration of the device function is fast and can readily cover concurrent conditions and semi-parallel inference. Moreover, the PN will have a more accurate than inference engine in dealing with unknown values. In this article, we used the Colored Petri-net (CPN) for verification of pacemaker, using MATLAB and CPN tool.