Formal modeling of biomedical signal acquisition systems: source of evidence for certification

Biomedical signal acquisition systems are software-intensive medical systems composed of processors, transducers, amplifiers, filters, and converters. We present in this article a formal modeling methodology of biomedical signal acquisition systems using Colored Petri Nets (CPN) and based on a frequency-domain approach. In the methodology, a reference model represents the main features of these medium risk systems. We argue that this kind of model is useful to assist manufacturers to reduce the number of defects in systems and to generate safety and effectiveness evidence throughout certification. Therefore, we describe two main contributions in this article. We provide a reference model of biomedical signal acquisition systems and show how manufacturers can generate evidence by means of an electrocardiography (ECG) case study. We carried out the case study by extending the reference model to represent the behavior of an ECG system using a basic cardiac monitor configuration based on the single-lead, heart rate monitor front end (AD8232) and the low power precision analog microcontroller, ARM cortex M3 with dual sigma-delta converters (ADUCM360). We verified the model against safety requirements with the model checking technique (safety evidence) and validated it by comparing output signals with a filtered ECG record available on the PHYSIONET ECG-ID database in the frequency and time domains (effectiveness evidence). This methodology enables manufacturers to identify defects in systems earlier in the development process aiming to decrease costs and development time.