Logic-Based Formalization of System Requirements for Integrated Clinical Environments

  • Cinzia Bernardeschi
  • Andrea DomeniciEmail author
  • Paolo Masci
Part of the Computational Biology book series (COBO, volume 30)


The concepts of integrated clinical environments and smart intensive care units refer to complex technological infrastructures where health care relies on interoperating medical devices monitored and coordinated by software applications under human supervision. These complex socio-technical systems have stringent safety requirements that can be met with rigorous and precise development methods. This chapter presents an approach to the formalization of system requirements for integrated clinical environments, using the Prototype Verification System, a theorem-proving environment based on a higher-order logic language. The approach is illustrated by modeling safety-related requirements affecting various aspects of an integrated clinical environment, and in particular the communication network. A simple but realistic wireless communication protocol will be used as an example of computer-assisted verification.


  1. 1.
    AAMI MDI/2012-03-30 (2012) Medical device interoperability. Association for the Advancement of Medical InstrumentationGoogle Scholar
  2. 2.
    Ahmed HS, Ali AA (2016) Smart intensive care unit design based on wireless sensor network and internet of things. In: 2016 Al-Sadeq international conference on multidisciplinary in IT and communication science and applications (AIC-MITCSA), pp 1–6.
  3. 3.
    ANSI/HL7 V2.8.2-2015 (2015) Health level seven standard version 2.8.2 — an application protocol for electronic data exchange in healthcare environments. Health Level Seven InternationalGoogle Scholar
  4. 4.
    Arney D, Goldman JM, Bhargav-Spantzel A, Basu A, Taborn M, Pappas G, Robkin M (2012) Simulation of medical device network performance and requirements for an integrated clinical environment. Biomed Instrum Technol 46(4):308–315. Scholar
  5. 5.
    Arney D, Plourde J, Schrenker R, Mattegunta P, Whitehead SF, Goldman JM (2014) Design pillars for medical cyber-physical system middleware. In: Turau V, Kwiatkowska M, Mangharam R, Weyer C (eds) 5th Workshop on medical cyber-physical systems, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, OpenAccess Series in Informatics (OASIcs), vol 36, pp 124–132,
  6. 6.
    Arney D, Plourde J, Goldman JM (2017) OpenICE medical device interoperability platform overview and requirement analysis. Biomedizinische Technik Biomedical Engineering. Scholar
  7. 7.
    Avižienis A, Laprie JC, Randell B, Landwehr C (2004) Basic concepts and taxonomy of dependable and secure computing. IEEE Trans Depend Sec Comput 1:11–33. Scholar
  8. 8.
    Bernardeschi C, Domenici A (2016) Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system. Inf Process Lett 116(6):409–415. Scholar
  9. 9.
    Bernardeschi C, Domenici A, Masci P (2014) Integrated simulation of implantable cardiac pacemaker software and heart models. In: CARDIOTECHNIX 2014, 2d international congress on cardiovascular technology, SCITEPRESS, pp 55–59Google Scholar
  10. 10.
    Bernardeschi C, Domenici A, Masci P (2015) Towards a formalization of system requirements for an integrated clinical environment. In: 5th EAI international conference on wireless mobile communication and healthcare – Transforming healthcare through innovations in mobile and wireless technologies, ACM.
  11. 11.
    Bernardeschi C, Domenici A, Masci P (2016) Modeling communication network requirements for an integrated clinical environment in the prototype verification system. In: 2016 IEEE symposium on computers and communication (ISCC), IEEE, pp 135–140,
  12. 12.
    Bernardeschi C, Domenici A, Masci P (2018) A PVS-simulink integrated environment for model-based analysis of cyber-physical systems. IEEE Trans Softw Eng 44(6):512–533. Scholar
  13. 13.
    Butler R, Sjogren J (1998) A PVS graph theory library. Nasa technical memorandum 1998-206923, NASA Langley Research Center, Hampton, VirginiaGoogle Scholar
  14. 14.
    Corsaro A, Schmidt DC (2012) The data distribution service - the communication middleware fabric for scalable and extensible systems-of-systems. INTECH. Scholar
  15. 15.
    Domenici A, Fagiolini A, Palmieri M (2017) Integrated simulation and formal verification of a simple autonomous vehicle. In: 1st workshop on formal co-simulation of cyber-physical systems. Springer, in pressGoogle Scholar
  16. 16.
    F2761-2009 (2009) Medical devices and medical systems — essential safety requirements for equipment comprising the patient-centric integrated clinical environment (ICE) — Part 1: general requirements and conceptual model. ASTM InternationalGoogle Scholar
  17. 17.
    FDA Guidance (2009) Design considerations and pre-market submission representations for interoperable medical devices — Guidance for industry and food and drug administration staff. US Food and Drug AdministrationGoogle Scholar
  18. 18.
    García-Valls M, Touahria IE (2017) On line service composition in the integrated clinical environment for ehealth and medical systems. Sensors 17(6).
  19. 19.
    García-Valls M, Lopez IR, Villar LF (2013) iLAND: an enhanced middleware for real-time reconfiguration of service oriented distributed real-time systems. IEEE Trans Ind Inform 9(1):228–236. Scholar
  20. 20.
    Girard JY, Lafont Y, Taylor P (1990) Proofs and types. Cambridge tracts in theoretical computer science, vol 7. Cambridge University Press, Cambridge. Scholar
  21. 21.
    Halpern NA (2014) Advanced informatics in the intensive care unit: possibilities and challenges.
  22. 22.
    Harrison MD, Masci P, Campos JC, Curzon P (2014) Demonstrating that medical devices satisfy user related safety requirements. In: 4th international symposium on foundations of healthcare information engineering and systems (FHIES2014)Google Scholar
  23. 23.
    Islam SMR, Kwak D, Kabir MH, Hossain M, Kwak KS (2015) The internet of things for health care: a comprehensive survey. IEEE Access 3:678–708. Scholar
  24. 24.
    Kabachinski J (2006) What is health level 7? Biomed Instrum Technol 40(5):375–379. Scholar
  25. 25.
    Kühn F, Leucker M (2014) OR.NET: safe interconnection of medical devices. Springer, Berlin, pp 188–198. Scholar
  26. 26.
    Larson B, Hatcliff J, Procter S, Chalin P (2012) Requirements specification for apps in medical application platforms. In: Proceedings of the 4th international workshop on software engineering in health care, SEHC ’12. IEEE Press, Piscataway, pp 26–32Google Scholar
  27. 27.
    Larson BR, Hatcliff J (2014) Open patient-controlled analgesia infusion pump system requirements — DRAFT 0.11. Technical report, SAnToS TR 2014-6-1, Kansas State UniversityGoogle Scholar
  28. 28.
    Larson BR, Hatcliff J, Chalin P (2013) Open source patient-controlled analgesic pump requirements documentation. In: Proceedings of the 5th international workshop on software engineering in health care, SEHC ’13. IEEE Press, Piscataway, pp 28–34Google Scholar
  29. 29.
    Leite FL, Adler R, Feth P (2017) Safety assurance for autonomous and collaborative medical cyber-physical systems. Springer International Publishing, Cham, pp 237–248. Scholar
  30. 30.
    Levis P, Lee N, Welsh M, Culler D (2003a) TOSSIM: Accurate and scalable simulation of entire TinyOS applications. In: Proceedings of the 1st international conference on embedded networked sensor systems, SenSys ’03. ACM, New York, pp 126–137.
  31. 31.
    Levis P, Lee N, Welsh M, Culler D (2003b) TOSSim: accurate and scalable simulation of entire TinyOS applications. In: Proceedings of the international conference on embedded networked sensor systems. ACM Press, New York, pp 126–137.
  32. 32.
    Masci P, Zhang Y, Jones P, Curzon P, Thimbleby H (2014a) Formal verification of medical device user interfaces using PVS. In: Gnesi S, Rensink A (eds) Fundamental approaches to software engineering. Lecture notes in computer science, vol 8411. Springer, Berlin, pp 200–214. Scholar
  33. 33.
    Masci P, Zhang Y, Jones P, Oladimeji P, D’Urso E, Bernardeschi C, Curzon P, Thimbleby H (2014b) Combining PVSio with state flow. In: Proceedings of the 6th international symposium on NASA formal methods. vol 8430. Springer, New York, pp 209–214. Scholar
  34. 34.
    Masci P, Mallozzi P, De Angelis FL, Di Marzo Serugendo G, Curzon P (2015a) Using PVSio-web and SAPERE for rapid prototyping of user interfaces in integrated clinical environments. In: Verisure2015, Workshop on verification and assurance, co-located with CAV2015Google Scholar
  35. 35.
    Masci P, Oladimeji P, Mallozzi P, Curzon P, Thimbleby H (2015b) PVSio-web: mathematically based tool support for the design of interactive and interoperable medical systems. In: Proceedings of the 5th EAI international conference on wireless mobile communication and healthcare, ICST, MOBIHEALTH’15, pp 42–45.
  36. 36.
    Mauro G, Thimbleby H, Domenici A, Bernardeschi C (2017) Extending a user interface prototyping tool with automatic MISRA C code generation. In: Dubois C, Masci P, Méry D (eds) Proceedings of the third workshop on formal integrated development environment, Limassol, Cyprus, November 8, 2016, Open Publishing Association, Electronic proceedings in theoretical computer science, vol 240, pp 53–66. Scholar
  37. 37.
    Muñoz C (2003) Rapid prototyping in PVS. Technical report. NIA 2003-03, NASA/CR-2003-212418, National Institute of Aerospace, Hampton, VA, USAGoogle Scholar
  38. 38.
    Owre S, Rushby J, Shankar N (1992) PVS: A prototype verification system. In: Kapur D (ed) Automated deduction — CADE-11. Lecture notes in computer science, vol 607. Springer, Berlin, pp 748–752. Scholar
  39. 39.
    Rausch TL, Judd TM (2016) Using integrated clinical environment data for health technology management. In: 2016 IEEE-EMBS international conference on biomedical and health informatics (BHI), pp 607–609.
  40. 40.
    Ray A, Jetley R, Jones PL, Zhang Y (2010) Model-based engineering for medical-device software. Biomed Instrum Technol 44(6):507–518. Scholar
  41. 41.
    Rhoads JG, Cooper T, Fuchs K, Schluter P, Zambuto RP (2010) Medical device interoperability and the integrating the healthcare enterprise (IHE) Initiative. Biomed Instrum Technol (suppl).:21–27Google Scholar
  42. 42.
    Rushby J (2000) Verification diagrams revisited: Disjunctive invariants for easy verification. In: Emerson EA, Sistla AP (eds) Proceedings of the computer aided verification: 12th international conference, CAV 2000, Chicago, July 15–19, 2000. Springer, Berlin, pp 508–520. Scholar
  43. 43.
    Venkatasubramanian KK, Vasserman EY, Sfyrla V, Sokolsky O, Lee I (2015) Requirement engineering for functional alarm system for interoperable medical devices. Springer International Publishing, Cham, pp 252–266. Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Cinzia Bernardeschi
    • 1
  • Andrea Domenici
    • 1
    Email author
  • Paolo Masci
    • 2
  1. 1.Department of Information EngineeringUniversity of PisaPisaItaly
  2. 2.HASLab, INESC TEC & Universidade do MinhoBragaPortugal

Personalised recommendations