A framework for the verification of an ECG biosensor algorithm

ElectroCardioGram(ECG) bio-sensors are used to detect and transmit the electrical activity of the heart over a period of time. The ECGs are treated by a signal processing unit inside the bio-sensor to detect and identify heart related medical conditions. Testing and verification of bio-sensor is of paramount importance as faults in these critical systems may lead to loss of life. However, due to the complexity of these systems traditional testing methods might not be adequate to provide high level of assurance about the correctness of their operation. In this paper, we propose a verification framework where we utilize simulation and formal methods to validate the correctness of the ECG bio-sensor. The framework is used to verify ECG bio-sensor at several levels of abstractions, including the signal processing level, where the ECG signal attributes, signal processing algorithm including its filters, detection and analysis algorithms, and triggering the alarm are modeled.