{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T05:19:59Z","timestamp":1726031999518},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030172961"},{"type":"electronic","value":"9783030172978"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17297-8_8","type":"book-chapter","created":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T13:04:12Z","timestamp":1560258252000},"page":"215-242","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Logic-Based Formalization of System Requirements for Integrated Clinical Environments"],"prefix":"10.1007","author":[{"given":"Cinzia","family":"Bernardeschi","sequence":"first","affiliation":[]},{"given":"Andrea","family":"Domenici","sequence":"additional","affiliation":[]},{"given":"Paolo","family":"Masci","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,6,12]]},"reference":[{"key":"8_CR1","unstructured":"AAMI MDI\/2012-03-30 (2012) Medical device interoperability. Association for the Advancement of Medical Instrumentation"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"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\u20136. \n                    https:\/\/doi.org\/10.1109\/AIC-MITCSA.2016.7759905","DOI":"10.1109\/AIC-MITCSA.2016.7759905"},{"key":"8_CR3","unstructured":"ANSI\/HL7 V2.8.2-2015 (2015) Health level seven standard version 2.8.2 \u2014 an application protocol for electronic data exchange in healthcare environments. Health Level Seven International"},{"issue":"4","key":"8_CR4","doi-asserted-by":"publisher","first-page":"308","DOI":"10.2345\/0899-8205-46.4.308","volume":"46","author":"D Arney","year":"2012","unstructured":"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\u2013315. \n                    https:\/\/doi.org\/10.2345\/0899-8205-46.4.308","journal-title":"Biomed Instrum Technol"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"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\u2013Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, OpenAccess Series in Informatics (OASIcs), vol\u00a036, pp 124\u2013132, \n                    https:\/\/doi.org\/10.4230\/OASIcs.MCPS.2014.124","DOI":"10.4230\/OASIcs.MCPS.2014.124"},{"key":"8_CR6","doi-asserted-by":"publisher","DOI":"10.1515\/bmt-2017-0040","author":"D Arney","year":"2017","unstructured":"Arney D, Plourde J, Goldman JM (2017) OpenICE medical device interoperability platform overview and requirement analysis. Biomedizinische Technik Biomedical Engineering. \n                    https:\/\/doi.org\/10.1515\/bmt-2017-0040","journal-title":"Biomedizinische Technik Biomedical Engineering"},{"issue":"1","key":"8_CR7","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/TDSC.2004.2","volume":"1","author":"A. Avizienis","year":"2004","unstructured":"Avi\u017eienis A, Laprie JC, Randell B, Landwehr C (2004) Basic concepts and taxonomy of dependable and secure computing. IEEE Trans Depend Sec Comput 1:11\u201333. \n                    https:\/\/doi.org\/doi.ieeecomputersociety.org\/10.1109\/TDSC.2004.2","journal-title":"IEEE Transactions on Dependable and Secure Computing"},{"issue":"6","key":"8_CR8","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1016\/j.ipl.2016.02.001","volume":"116","author":"C Bernardeschi","year":"2016","unstructured":"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\u2013415. \n                    https:\/\/doi.org\/10.1016\/j.ipl.2016.02.001","journal-title":"Inf Process Lett"},{"key":"8_CR9","unstructured":"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\u201359"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"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 \u2013 Transforming healthcare through innovations in mobile and wireless technologies, ACM. \n                    https:\/\/doi.org\/10.4108\/eai.14-10-2015.2261701","DOI":"10.4108\/eai.14-10-2015.2261701"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"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\u2013140, \n                    https:\/\/doi.org\/10.1109\/ISCC.2016.7543728","DOI":"10.1109\/ISCC.2016.7543728"},{"issue":"6","key":"8_CR12","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1109\/TSE.2017.2694423","volume":"44","author":"C Bernardeschi","year":"2018","unstructured":"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\u2013533. \n                    https:\/\/doi.org\/10.1109\/TSE.2017.2694423","journal-title":"IEEE Trans Softw Eng"},{"key":"8_CR13","unstructured":"Butler R, Sjogren J (1998) A PVS graph theory library. Nasa technical memorandum 1998-206923, NASA Langley Research Center, Hampton, Virginia"},{"key":"8_CR14","doi-asserted-by":"publisher","DOI":"10.5772\/30322","author":"A Corsaro","year":"2012","unstructured":"Corsaro A, Schmidt DC (2012) The data distribution service - the communication middleware fabric for scalable and extensible systems-of-systems. INTECH. \n                    https:\/\/doi.org\/10.5772\/30322","journal-title":"INTECH"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/978-3-319-74781-1_21"},{"key":"8_CR16","unstructured":"F2761-2009 (2009) Medical devices and medical systems \u2014 essential safety requirements for equipment comprising the patient-centric integrated clinical environment (ICE) \u2014 Part 1: general requirements and conceptual model. ASTM International"},{"key":"8_CR17","unstructured":"FDA Guidance (2009) Design considerations and pre-market submission representations for interoperable medical devices \u2014 Guidance for industry and food and drug administration staff. US Food and Drug Administration"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Garc\u00eda-Valls M, Touahria IE (2017) On line service composition in the integrated clinical environment for ehealth and medical systems. Sensors 17(6). \n                    https:\/\/doi.org\/10.3390\/s17061333","DOI":"10.3390\/s17061333"},{"issue":"1","key":"8_CR19","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1109\/TII.2012.2198662","volume":"9","author":"M Garc\u00eda-Valls","year":"2013","unstructured":"Garc\u00eda-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\u2013236. \n                    https:\/\/doi.org\/10.1109\/TII.2012.2198662","journal-title":"IEEE Trans Ind Inform"},{"issue":"2","key":"8_CR20","doi-asserted-by":"publisher","first-page":"760","DOI":"10.2307\/2274726","volume":"56","author":"W. A. Howard","year":"1991","unstructured":"Girard JY, Lafont Y, Taylor P (1990) Proofs and types. Cambridge tracts in theoretical computer science, vol 7. Cambridge University Press, Cambridge. \n                    https:\/\/doi.org\/10.2307\/2274726","journal-title":"Journal of Symbolic Logic"},{"key":"8_CR21","unstructured":"Halpern NA (2014) Advanced informatics in the intensive care unit: possibilities and challenges. \n                    http:\/\/healthcare.nist.gov\/medicaldevices\/publications.html"},{"key":"8_CR22","unstructured":"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)"},{"key":"8_CR23","doi-asserted-by":"publisher","first-page":"678","DOI":"10.1109\/ACCESS.2015.2437951","volume":"3","author":"SMR Islam","year":"2015","unstructured":"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\u2013708. \n                    https:\/\/doi.org\/10.1109\/ACCESS.2015.2437951","journal-title":"IEEE Access"},{"issue":"5","key":"8_CR24","doi-asserted-by":"publisher","first-page":"375","DOI":"10.2345\/i0899-8205-40-5-375.1","volume":"40","author":"J Kabachinski","year":"2006","unstructured":"Kabachinski J (2006) What is health level 7? Biomed Instrum Technol 40(5):375\u2013379. \n                    https:\/\/doi.org\/10.2345\/i0899-8205-40-5-375.1","journal-title":"Biomed Instrum Technol"},{"key":"8_CR25","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-53956-5_13","volume-title":"Foundations of Health Information Engineering and Systems","author":"Franziska K\u00fchn","year":"2014","unstructured":"K\u00fchn F, Leucker M (2014) OR.NET: safe interconnection of medical devices. Springer, Berlin, pp 188\u2013198. \n                    https:\/\/doi.org\/10.1007\/978-3-642-53956-5_13"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"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 \u201912. IEEE Press, Piscataway, pp 26\u201332","DOI":"10.1109\/SEHC.2012.6227013"},{"key":"8_CR27","unstructured":"Larson BR, Hatcliff J (2014) Open patient-controlled analgesia infusion pump system requirements \u2014 DRAFT 0.11. Technical report, SAnToS TR 2014-6-1, Kansas State University"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"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 \u201913. IEEE Press, Piscataway, pp 28\u201334","DOI":"10.1109\/SEHC.2013.6602474"},{"key":"8_CR29","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-319-66284-8_20","volume-title":"Lecture Notes in Computer Science","author":"Fabio L. Leite","year":"2017","unstructured":"Leite FL, Adler R, Feth P (2017) Safety assurance for autonomous and collaborative medical cyber-physical systems. Springer International Publishing, Cham, pp 237\u2013248. \n                    https:\/\/doi.org\/10.1007\/978-3-319-66284-8_20"},{"key":"8_CR30","doi-asserted-by":"publisher","unstructured":"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 \u201903. ACM, New York, pp 126\u2013137. \n                    https:\/\/doi.org\/10.1145\/958491.958506","DOI":"10.1145\/958491.958506"},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"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\u2013137. \n                    https:\/\/doi.org\/10.1145\/958491.958506","DOI":"10.1145\/958491.958506"},{"key":"8_CR32","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-54804-8_14","volume-title":"Fundamental Approaches to Software Engineering","author":"Paolo Masci","year":"2014","unstructured":"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\u2013214. \n                    https:\/\/doi.org\/10.1007\/978-3-642-54804-8_14"},{"key":"8_CR33","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-319-06200-6_16","volume-title":"Lecture Notes in Computer Science","author":"Paolo Masci","year":"2014","unstructured":"Masci P, Zhang Y, Jones P, Oladimeji P, D\u2019Urso 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\u2013214. \n                    https:\/\/doi.org\/10.1007\/978-3-319-06200-6_16"},{"key":"8_CR34","unstructured":"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"},{"key":"8_CR35","doi-asserted-by":"publisher","unstructured":"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\u201915, pp 42\u201345. \n                    https:\/\/doi.org\/10.4108\/eai.14-10-2015.2261720","DOI":"10.4108\/eai.14-10-2015.2261720"},{"key":"8_CR36","doi-asserted-by":"publisher","first-page":"53","DOI":"10.4204\/EPTCS.240.4","volume":"240","author":"Gioacchino Mauro","year":"2017","unstructured":"Mauro G, Thimbleby H, Domenici A, Bernardeschi C (2017) Extending a user interface prototyping tool with automatic MISRA\u00a0C code generation. In: Dubois C, Masci P, M\u00e9ry 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\u201366. \n                    https:\/\/doi.org\/10.4204\/EPTCS.240.4","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"8_CR37","unstructured":"Mu\u00f1oz C (2003) Rapid prototyping in PVS. Technical report. NIA 2003-03, NASA\/CR-2003-212418, National Institute of Aerospace, Hampton, VA, USA"},{"key":"8_CR38","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre S, Rushby J, Shankar N (1992) PVS: A prototype verification system. In: Kapur D (ed) Automated deduction \u2014 CADE-11. Lecture notes in computer science, vol 607. Springer, Berlin, pp 748\u2013752. \n                    https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"8_CR39","doi-asserted-by":"publisher","unstructured":"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\u2013609. \n                    https:\/\/doi.org\/10.1109\/BHI.2016.7455971","DOI":"10.1109\/BHI.2016.7455971"},{"issue":"6","key":"8_CR40","doi-asserted-by":"publisher","first-page":"507","DOI":"10.2345\/0899-8205-44.6.507","volume":"44","author":"A Ray","year":"2010","unstructured":"Ray A, Jetley R, Jones PL, Zhang Y (2010) Model-based engineering for medical-device software. Biomed Instrum Technol 44(6):507\u2013518. \n                    https:\/\/doi.org\/10.2345\/0899-8205-44.6.507","journal-title":"Biomed Instrum Technol"},{"key":"8_CR41","unstructured":"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\u201327"},{"key":"8_CR42","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1007\/10722167_38","volume-title":"Computer Aided Verification","author":"John Rushby","year":"2000","unstructured":"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\u201319, 2000. Springer, Berlin, pp 508\u2013520. \n                    https:\/\/doi.org\/10.1007\/10722167_38"},{"key":"8_CR43","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-319-24255-2_19","volume-title":"Lecture Notes in Computer Science","author":"Krishna K. Venkatasubramanian","year":"2015","unstructured":"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\u2013266. \n                    https:\/\/doi.org\/10.1007\/978-3-319-24255-2_19"}],"container-title":["Computational Biology","Automated Reasoning for Systems Biology and Medicine"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17297-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T13:14:50Z","timestamp":1560258890000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17297-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030172961","9783030172978"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17297-8_8","relation":{},"ISSN":["1568-2684","2662-2432"],"issn-type":[{"type":"print","value":"1568-2684"},{"type":"electronic","value":"2662-2432"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}