Guided Test Case Generation for Enhanced ECG Bio-Sensors Functional Verification

Guided Test Case Generation for Enhanced ECG Bio-Sensors Functional Verification

Hussam Al Hamadi (Khalifa University, Abu Dhabi, United Arab Emirates), Amjad Gawanmeh (Khalifa University, Abu Dhabi, United Arab Emirates) and Mahmoud Al-Qutayri (Khalifa University, Abu Dhabi, United Arab Emirates)
Copyright: © 2017 |Pages: 20
DOI: 10.4018/IJEHMC.2017100101
OnDemand PDF Download:
No Current Special Offers


Testing and verifying the operation of bio-sensor nodes is essential due to the sensitivity and safety-critical aspects of their applications. Simulation technique is frequently used for this task; however, a proper set of test cases is required in order to carry out the simulation process. This paper focuses on enhancing the verification operations of an ElectroCardioGram (ECG) biomedical sensor node through simulation. It presents a new methodology for guided Test Cases Generation (TCG) of ECG signals from formal design specifications. Event-B invariants are used to specify ECG requirements, and then a new algorithm is used to translate these specifications into proper ECG signal parameters. These parameters are subsequently used to control the required shape of the ECG in order to have a wide range of scenarios. The primary objective of this work is to provide ECG test cases to detect design errors in biomedical algorithms. In addition, it can complement the usage of the limited ECG databases currently available to verify the correct operation of ECG bio-sensors.
Article Preview


The Electrocardiography (ECG) provides essential information related to the well-being of the human heart, e.g. the electrical activities of the heart nodes, the detection of abnormal behavior, and the thickness measurement of the heart chambers' walls. All ECG sensors have Receptors and Transducers that work (Azucena et al., 2015) to transform the human organ (heart) activities into electrical signals so-called ECG. It consists of three types of waves: P, QRS and T waves as shown in the Figure 1. These different waves are produced from the activity of different parts of the heart, the sinoatrial (SA) node in the heart system depolarizes the right and left atria, causing contraction, which producing the P wave. The depolarization wave reaches the atrioventricular (AV) node to allow the atria to finish contracting and the AV node depolarizes both ventricles which generates the QRS wave. The ventricles are re-polarized and causing the T wave. The segment in our previous was introduced as a period of time where the heart system is considered to be in the idle case (Chazal et al., 2004).

Figure 1.

ECG signal specification in (ECG Basics, 2015)


The continuous advances in integrated circuits have enabled the integration of sensors, processors, wireless communication and other functional blocks on a single device. This has led to the availability of systems-on-chip ECG devices that are able to capture and perform a full analysis of the heart signal. In this work, we focus on verifying the functionality of some of the algorithms used by an ECG sensor node to analyze heart signals and extract its key features to aid the medical diagnosis process.

Pan Tompkins algorithm (Pan & Tompkins, 1985) is a real-time algorithm for detecting QRS of ECG signals and representing them in a sequential set of peaks. Therefore, the Pan Tompkins output helps in measuring the RR-interval of the heart system and identifying abnormal behaviors. Due to the simplicity of the Pan-Tompkins algorithm, it has been used in many ECG biomedical sensors (Chung, 2009), and therefore, it is going to be adopted in this work as well.

In a previous work, we used Event-B (Abrial, 2010) to develop a framework that formalizes the abstract level of ECG sensor model and verify it (Al Hamadi et al., 2014). Our verification framework is based on refining the abstract level of the ECG sensor to reach lower levels of abstraction and overcome the complexity of formalizing the Pan Tompkins algorithm. In addition, we defined the ECG components and their relation to formalize their behavior and use them in the ECG sensor model. The complete formal model of the ECG sensor was able to verify the functional requirements of the sensor algorithm and design using the Rodin platform. This was achieved by presenting the design objectives including classifying normal and abnormal behaviors into formal properties (Abrial et al., 2010). In this paper, the objective is to guide the simulation process by using the formal properties and let the flag system's feedback guide the ongoing process for more flag coverage and thus for more functionality and code coverage. A Test Case Generation (TCG) setup have been developed to translate the formal syntax of the formal properties, which will be introduced in this paper, and generate its equivalent ECG traces to use them in the simulation process. The feedback of the generated ECGs explores the cases that can be expressed in an additional set of properties.

The rest of the paper is organized as follows. Section 2 describes the motivation with respect to the related work. Section 3 details the methodology of TCG and describes its components. In Section 4, we discuss the performance evaluation of the TCG and present the flag groups and their feedback in guiding the TCG toward more coverage. Finally, Section 5 presents the conclusions of this work.

Complete Article List

Search this Journal:
Volume 13: 2 Issues (2022): 1 Released, 1 Forthcoming
Volume 12: 6 Issues (2021)
Volume 11: 4 Issues (2020)
Volume 10: 4 Issues (2019)
Volume 9: 4 Issues (2018)
Volume 8: 4 Issues (2017)
Volume 7: 4 Issues (2016)
Volume 6: 4 Issues (2015)
Volume 5: 4 Issues (2014)
Volume 4: 4 Issues (2013)
Volume 3: 4 Issues (2012)
Volume 2: 4 Issues (2011)
Volume 1: 4 Issues (2010)
View Complete Journal Contents Listing