Software & Systems Modeling

, Volume 18, Issue 2, pp 1467–1485 | Cite as

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

  • Alvaro SobrinhoEmail author
  • Leandro Dias da Silva
  • Angelo Perkusich
  • Paulo Cunha
  • Thiago Cordeiro
  • Antonio Marcus Nogueira Lima
Regular Paper


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.


Biomedical signal acquisition systems Colored petri nets Formal methods Model checking Frequency-domain approach 



The authors would like to thank the Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES), Fundação de Amparo a Pesquisa de Alagoas (FAPEAL) and Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq) for supporting this research.


  1. 1.
    Alemzadeh, H., Iyer, R., Kalbarczyk, Z., Raman, J.: Analysis of safety-critical computer failures in medical devices. IEEE Secur. Priv. 11(4), 14–26 (2013)Google Scholar
  2. 2.
    Analog Devices: Single-Lead, Heart Rate Monitor Front End Data Sheet AD8232 (2013)Google Scholar
  3. 3.
    Analog Devices: Low Power, Precision Analog Microcontroller with Dual Sigma-Delta ADCs, ARM Cortex-M3, Data Sheet ADuCM360/ADuCM361 (2014)Google Scholar
  4. 4.
    Arney, D., Jetley, R., Jones, P., Lee, I., Sokolsky, O.: Formal methods based development of a pca infusion pump reference model: Generic infusion pump (gip) project. In: Joint Workshop on High Confidence Medical Devices, Software, and Systems and Medical Device Plug-and-Play Interoperability, pp. 23–33 (2007)Google Scholar
  5. 5.
    Barbosa, P., Morais, M., Galdino, K., Andrade, M., Gomes, L., Moutinho, F., de Figueiredo, J.: Towards medical device behavioural validation using petri nets. In: IEEE 26th International Symposium on Computer-Based Medical Systems (CBMS), pp. 4–10 (2013)Google Scholar
  6. 6.
    Chandrakar, B., Yadav, O., Chandra, V.: A survey of noise removal techniques for ecg signals. Int. J. Adv. Res. Comput. Commun. Eng. 2(3), 1354–1357 (2013)Google Scholar
  7. 7.
    Chavan, M.S., Agarwala, R.A., Uplane, M.D.: Interference reduction in ecg using digital fir filters based on rectangular window. WSEAS Trans. Signal Process. 4(5), 340–349 (2008)Google Scholar
  8. 8.
    Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge, MA (1999)zbMATHGoogle Scholar
  9. 9.
    Desel, J., Reisig, W.: The concepts of petri nets. Softw. Syst. Model. 14(2), 669–683 (2014)Google Scholar
  10. 10.
    FDA: Medical device classification procedures (Revised as of April 2016)Google Scholar
  11. 11.
    Goldberger, A., Amaral, L., Glass, L., Hausdorff, J.M., Ivanov, P.C., Mark, R., Mietus, J., Moody, G., Peng, C.K., Stanley, H.: Physiobank, physiotoolkit, and physionet: components of a new research resource for complex physiologic signals. Circulation 23(101), 215–220 (2000)Google Scholar
  12. 12.
    Han, J., Ding, Q., Xiong, A., Zhao, X.: A state-space emg model for the estimation of continuous joint movements. IEEE Trans. Industr. Electron. 62(7), 4267–4275 (2015)Google Scholar
  13. 13.
    Hawkins, R., Habli, I., Kelly, T., McDermid, J.: Assurance cases and prescriptive software safety certification: a comparative study. Saf. Sci. 59, 55–71 (2013)Google Scholar
  14. 14.
    Jensen, K., Kristensen, L.M.: Coloured Petri Nets: Modelling and Validation of Concurrent Systems, 1st edn. Springer, Berlin (2009)zbMATHGoogle Scholar
  15. 15.
    Jensen, K., Kristensen, L.M.: Colored petri nets: a graphical language for formal modeling and validation of concurrent systems. Commun. ACM 58(6), 61–70 (2015)Google Scholar
  16. 16.
    Jensen, K., Kristensen, L.M., Wells, L.: Coloured petri nets and cpn tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transfer 9(3), 213–254 (2007)Google Scholar
  17. 17.
    Jiang, Z., Pajic, M., Alur, R., Mangharam, R.: Closed-loop verification of medical devices with model abstraction and refinement. Int. J. Softw. Tools Technol. Transfer 16(2), 191–213 (2014)Google Scholar
  18. 18.
    Jiang, Z., Pajic, M., Mangharam, R.: Cyber-physical modeling of implantable cardiac medical devices. Proc. IEEE 100(1), 122–137 (2012)Google Scholar
  19. 19.
    Kim, B., Ayoub, A., Sokolsky, O., Lee, I., Jones, P., Zhang, Y., Jetley, R.: Safety-assured development of the gpca infusion pump software. In: Proceedings of the Ninth ACM International Conference on Embedded Software, EMSOFT ’11, pp. 155–164 (2011)Google Scholar
  20. 20.
    Kim, J., Kang, I., Choi, J., Lee, I., Kang, S.: Formal synthesis of application and platform behaviors of embedded software systems. Softw. Syst. Model. 14(2), 839–859 (2013)Google Scholar
  21. 21.
    Kitchin, C., Counts, L.: A designer’s guide to instrumentation amplifiers, 3th edn. Analog Devices (2006)Google Scholar
  22. 22.
    Kligfield, P., Gettes, L.S., Bailey, J.J., Childers, R., Deal, B.J., Hancock, E.W., van Herpen, G., Kors, J.A., Macfarlane, P., Mirvis, D.M., Pahlm, O., Rautaharju, P., Wagner, G.S.: Recommendations for the standardization and interpretation of the electrocardiogram: Part I: the electrocardiogram and its technology: a scientific statement from the american heart association electrocardiography and arrhythmias committee, council on clinical cardiology; the american college of cardiology foundation; and the heart rhythm society endorsed by the international society for computerized electrocardiology. Circulation 115(10), 1306–1324 (2007)Google Scholar
  23. 23.
    Kloetzer, M., Mahulea, C., Belta, C., Silva, M.: An automated framework for formal verification of timed continuous petri nets. IEEE Trans. Ind. Inf. 6(3), 460–471 (2010)Google Scholar
  24. 24.
    Koch, I.: Petri nets in systems biology. Softw. Syst. Model. 14(2), 703–710 (2014)Google Scholar
  25. 25.
    Lee, Y.S., Kim, D.J., Kim, J.O., Kim, H.: New fmeca methodology using structural importance and fuzzy theory. IEEE Trans. Power Syst. 26(4), 2364–2370 (2011)Google Scholar
  26. 26.
    Li, S., Xu, L.D., Wang, X.: A continuous biomedical signal acquisition system based on compressed sensing in body sensor networks. IEEE Trans. Ind. Inf. 9(3), 1764–1771 (2013)Google Scholar
  27. 27.
    Li, T., Tan, F., Wang, Q., Bu, L., Cao, J., Liu, X.: From offline toward real time: a hybrid systems model checking and cps codesign approach for medical device plug-and-play collaborations. IEEE Trans. Parallel Distrib. Syst. 25(3), 642–652 (2014)Google Scholar
  28. 28.
    Lin, C.L., Shen, W.: Generation of assurance cases for medical devices. In: Lee, R. (ed.) Computer and Information Science, Studies in Computational Intelligence, vol. 566, pp. 127–140. Springer, Berlin (2015)Google Scholar
  29. 29.
    Mashkoor, A.: Model-driven development of high-assurance active medical devices. Soft. Qual. J. 24(3), 571–596 (2016)Google Scholar
  30. 30.
    Méry, D., Singh, N.K.: Formal specification of medical systems by proof-based refinement. ACM Trans. Embed. Comput. Syst. 12(1), 1–25 (2013)Google Scholar
  31. 31.
    Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised), 1th edn. MIT Press (1997)Google Scholar
  32. 32.
    Mitros, P.: Filters with decreased passband error. IEEE Trans. Circuits Syst. II Express Br. 63(2), 131–135 (2016)Google Scholar
  33. 33.
    Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)Google Scholar
  34. 34.
    Pajic, M., Mangharam, R., Sokolsky, O., Arney, D., Goldman, J., Lee, I.: Model-driven safety analysis of closed-loop medical systems. IEEE Trans. Ind. Inf. 10(1), 3–16 (2014)Google Scholar
  35. 35.
    Pelgrom, M.: Analog-to-Digital Conversion, 1st edn. Springer, Netherlands (2010)Google Scholar
  36. 36.
    Qadir, J., Hasan, O.: Applying formal methods to networking: theory, techniques, and applications. IEEE Commun. Surv. Tutor. 17(1), 256–291 (2015)Google Scholar
  37. 37.
    Rao, K.R., Kim, D.N., Hwang, J.J.: Fast Fourier Transform—Algorithms and Applications, 1st edn. Springer, Netherlands (2010)zbMATHGoogle Scholar
  38. 38.
    Razzaq, N., Sheikh, S.A.A., Salman, M., Zaidi, T.: An intelligent adaptive filter for elimination of power line interference from high resolution electrocardiogram. IEEE Access 4, 1676–1688 (2016)Google Scholar
  39. 39.
    Schlechtingen, M., Santos, I.F., Achiche, S.: Using data-mining approaches for wind turbine power curve monitoring: a comparative study. IEEE Trans. Sustain. Energy 4(3), 671–679 (2013)Google Scholar
  40. 40.
    Sedra, A.S., Smith, K.C.: Microelectronic Circuits, 6th edn. Oxford University Press, Oxford (2009)Google Scholar
  41. 41.
    Seifi, Y., Suriadi, S., Foo, E., Boyd, C.: Analysis of two authorization protocols using colored petri nets. Int. J. Inf. Secur. 14(3), 221–247 (2015)Google Scholar
  42. 42.
    Silva, L.C., Almeida, H.O., Perkusich, A., Perkusich, M.: A model-based approach to support validation of medical cyber-physical systems. Sensors 15(11), 27625–27670 (2015)Google Scholar
  43. 43.
    Sobrinho, A., Perkusich, A., Dias da Silva, L., Cordeiro, T., Rego, J., Cunha, P.: Towards medical device certification: a colored petri nets model of a surface electrocardiography device. In: 40th Annual Conference of the IEEE Industrial Electronics Society, pp. 2645–2651 (2014)Google Scholar
  44. 44.
    Sobrinho, A., Perkusich, A., Dias da Silva, L., Cunha, P.: Using colored petri nets for the requirements engineering of a surface electrogastrography system. In: IEEE International Conference on Industrial Informatics (INDIN), pp. 221–226 (2014)Google Scholar
  45. 45.
    Sun, X., Zhang, Y.: Design and implementation of portable ecg and body temperature monitor. In: International Symposium on Computer, Consumer and Control, pp. 188–192 (2014)Google Scholar
  46. 46.
    Tran, T.V., Chung, W.Y.: IEEE-802.15.4-based low-power body sensor node with RF energy harvester. Bio Med. Mater. Eng. 24, 3503–3510 (2014)Google Scholar
  47. 47.
    Wolf, K.: The petri net twist in explicit model checking. Softw. Syst. Model. 14(2), 711–717 (2014)Google Scholar
  48. 48.
    Wu, D., Schnieder, E.: Scenario-based system design with colored petri nets: an application to train control systems. Softw. Syst. Model. 1–23 (2016). doi: 10.1007/s10270-016-0517-1

Copyright information

© Springer-Verlag GmbH Germany 2017

Authors and Affiliations

  1. 1.Federal Rural University of the SemiaridPau dos FerrosBrazil
  2. 2.Federal University of AlagoasMaceióBrazil
  3. 3.Federal University of Campina GrandeCampina GrandeBrazil
  4. 4.Federal Institute of AlagoasArapiracaBrazil

Personalised recommendations