Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
AAMI MDI/2012-03-30 (2012) Medical device interoperability. Association for the Advancement of Medical Instrumentation
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. https://doi.org/10.1109/AIC-MITCSA.2016.7759905
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 International
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. https://doi.org/10.2345/0899-8205-46.4.308
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, https://doi.org/10.4230/OASIcs.MCPS.2014.124
Arney D, Plourde J, Goldman JM (2017) OpenICE medical device interoperability platform overview and requirement analysis. Biomedizinische Technik Biomedical Engineering. https://doi.org/10.1515/bmt-2017-0040
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. https://doi.org/doi.ieeecomputersociety.org/10.1109/TDSC.2004.2
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. https://doi.org/10.1016/j.ipl.2016.02.001
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–59
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. https://doi.org/10.4108/eai.14-10-2015.2261701
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, https://doi.org/10.1109/ISCC.2016.7543728
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. https://doi.org/10.1109/TSE.2017.2694423
Butler R, Sjogren J (1998) A PVS graph theory library. Nasa technical memorandum 1998-206923, NASA Langley Research Center, Hampton, Virginia
Corsaro A, Schmidt DC (2012) The data distribution service - the communication middleware fabric for scalable and extensible systems-of-systems. INTECH. https://doi.org/10.5772/30322
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 press
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 International
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 Administration
García-Valls M, Touahria IE (2017) On line service composition in the integrated clinical environment for ehealth and medical systems. Sensors 17(6). https://doi.org/10.3390/s17061333
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. https://doi.org/10.1109/TII.2012.2198662
Girard JY, Lafont Y, Taylor P (1990) Proofs and types. Cambridge tracts in theoretical computer science, vol 7. Cambridge University Press, Cambridge. https://doi.org/10.2307/2274726
Halpern NA (2014) Advanced informatics in the intensive care unit: possibilities and challenges. http://healthcare.nist.gov/medicaldevices/publications.html
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)
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. https://doi.org/10.1109/ACCESS.2015.2437951
Kabachinski J (2006) What is health level 7? Biomed Instrum Technol 40(5):375–379. https://doi.org/10.2345/i0899-8205-40-5-375.1
Kühn F, Leucker M (2014) OR.NET: safe interconnection of medical devices. Springer, Berlin, pp 188–198. https://doi.org/10.1007/978-3-642-53956-5_13
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–32
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 University
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–34
Leite FL, Adler R, Feth P (2017) Safety assurance for autonomous and collaborative medical cyber-physical systems. Springer International Publishing, Cham, pp 237–248. https://doi.org/10.1007/978-3-319-66284-8_20
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. https://doi.org/10.1145/958491.958506
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. https://doi.org/10.1145/958491.958506
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. https://doi.org/10.1007/978-3-642-54804-8_14
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. https://doi.org/10.1007/978-3-319-06200-6_16
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 CAV2015
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. https://doi.org/10.4108/eai.14-10-2015.2261720
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. https://doi.org/10.4204/EPTCS.240.4
Muñoz C (2003) Rapid prototyping in PVS. Technical report. NIA 2003-03, NASA/CR-2003-212418, National Institute of Aerospace, Hampton, VA, USA
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. https://doi.org/10.1007/3-540-55602-8_217
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. https://doi.org/10.1109/BHI.2016.7455971
Ray A, Jetley R, Jones PL, Zhang Y (2010) Model-based engineering for medical-device software. Biomed Instrum Technol 44(6):507–518. https://doi.org/10.2345/0899-8205-44.6.507
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–27
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. https://doi.org/10.1007/10722167_38
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. https://doi.org/10.1007/978-3-319-24255-2_19
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Bernardeschi, C., Domenici, A., Masci, P. (2019). Logic-Based Formalization of System Requirements for Integrated Clinical Environments. In: Liò, P., Zuliani, P. (eds) Automated Reasoning for Systems Biology and Medicine. Computational Biology, vol 30. Springer, Cham. https://doi.org/10.1007/978-3-030-17297-8_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-17297-8_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-17296-1
Online ISBN: 978-3-030-17297-8
eBook Packages: Computer ScienceComputer Science (R0)