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 article, we present a method to verify the pacemaker behavior. This method considers the fuzzy function of the pacemaker. Using Petri-nets 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 Petri-net will have a more accurate than inference engine in dealing with unknown values. In this article, we used the colored Petri-net for verification of pacemaker, using MATLAB and CPN tool.