Article Preview
TopIntroduction
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.