Formal validation of QRS wave within ECG

Electrical sensors are used to detect and record the electrical activity of the heart over a period of time, this operation is referred to as Electrocardiography (ECG) in medical science. Hence ECG is composed of a set of signal waves that repeats themselves and are usually useful in medical diagnosis, where certain ECG patterns and the occupancy of specific waves, such as the QRS wave, may indicate certain heart problems. In this paper, we extend our previous results where we provided a high level model for ECG wave, with a more concrete model for QRS waves at several levels of abstraction in order to validate the specification of the QRS waves and several properties related to its behavior. We use formal method since medical applications still suffer from design and understanding problems when implemented in ICT context despite the use of thorough test through simulation techniques which may lead to ambiguities and incompleteness in the developed methods for using ECG specifications in medical diagnosis. We used the Event-B formal method to successfully formalize the QRS wave in the ECG of the heart system at several levels of abstraction, and then defined and validated several properties that are related to its wavelet shape and behavior.