{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,21]],"date-time":"2026-04-21T14:57:15Z","timestamp":1776783435591,"version":"3.51.2"},"reference-count":60,"publisher":"MDPI AG","issue":"11","license":[{"start":{"date-parts":[[2015,10,30]],"date-time":"2015-10-30T00:00:00Z","timestamp":1446163200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sensors"],"abstract":"<jats:p>Medical Cyber-Physical Systems (MCPS) are context-aware, life-critical systems with patient safety as the main concern, demanding rigorous processes for validation to guarantee user requirement compliance and specification-oriented correctness. In this article, we propose a model-based approach for early validation of MCPS, focusing on promoting reusability and productivity. It enables system developers to build MCPS formal models based on a library of patient and medical device models, and simulate the MCPS to identify undesirable behaviors at design time. Our approach has been applied to three different clinical scenarios to evaluate its reusability potential for different contexts. We have also validated our approach through an empirical evaluation with developers to assess productivity and reusability. Finally, our models have been formally verified considering functional and safety requirements and model coverage.<\/jats:p>","DOI":"10.3390\/s151127625","type":"journal-article","created":{"date-parts":[[2015,11,2]],"date-time":"2015-11-02T02:53:57Z","timestamp":1446432837000},"page":"27625-27670","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":29,"title":["A Model-Based Approach to Support Validation of Medical Cyber-Physical Systems"],"prefix":"10.3390","volume":"15","author":[{"given":"Lenardo","family":"Silva","sequence":"first","affiliation":[{"name":"Embedded Systems and Pervasive Computing Laboratory, Federal University of Campina Grande, 882 Apr\u00edgio Veloso Street, Universit\u00e1rio, Campina Grande 58429-900, Brazil"}]},{"given":"Hyggo","family":"Almeida","sequence":"additional","affiliation":[{"name":"Embedded Systems and Pervasive Computing Laboratory, Federal University of Campina Grande, 882 Apr\u00edgio Veloso Street, Universit\u00e1rio, Campina Grande 58429-900, Brazil"}]},{"given":"Angelo","family":"Perkusich","sequence":"additional","affiliation":[{"name":"Embedded Systems and Pervasive Computing Laboratory, Federal University of Campina Grande, 882 Apr\u00edgio Veloso Street, Universit\u00e1rio, Campina Grande 58429-900, Brazil"}]},{"given":"Mirko","family":"Perkusich","sequence":"additional","affiliation":[{"name":"Embedded Systems and Pervasive Computing Laboratory, Federal University of Campina Grande, 882 Apr\u00edgio Veloso Street, Universit\u00e1rio, Campina Grande 58429-900, Brazil"}]}],"member":"1968","published-online":{"date-parts":[[2015,10,30]]},"reference":[{"key":"ref_1","first-page":"124","article-title":"Design Pillars for Medical Cyber-Physical System Middleware","volume":"36","author":"Arney","year":"2014","journal-title":"OpenAccess Ser. Inform."},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Haque, S.A., Aziz, S.M., and Rahman, M. (2014). Review of Cyber-Physical System in Healthcare. Int. J. Distrib. Sens. Netw.","DOI":"10.1155\/2014\/217415"},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1109\/JPROC.2011.2165270","article-title":"Challenges and research directions in medical cyber-physical systems","volume":"100","author":"Lee","year":"2012","journal-title":"IEEE Proc."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"4837","DOI":"10.3390\/s150304837","article-title":"The Past, Present and Future of Cyber-Physical Systems: A Focus on Models","volume":"15","author":"Lee","year":"2015","journal-title":"Sensors"},{"key":"ref_5","unstructured":"Delaune, S.C., and Ladner, P.K. (2011). Fundamentals of Nursing: Standards & Practice, Cengage Learning. [4th ed.]."},{"key":"ref_6","unstructured":"Rosdahl, C.B., and Kowalski, M.T. (2012). Textbook of Basic Nursing, Wolters Kluwer Health Lippincott Williams & Wilkins. [10th ed.]."},{"key":"ref_7","first-page":"221","article-title":"Semiolog\u00eda de los Signos Vitales: Una Mirada Novedosa a un Problema Vigente","volume":"12","author":"Arenas","year":"2012","journal-title":"Arch. Med."},{"key":"ref_8","unstructured":"FDA CFR\u2014Code of Federal Regulations Title 21\u2014Part 820, Available online:http:\/\/www.accessdata.fda.gov\/scripts\/cdrh\/cfdocs\/cfcfr\/CFRSearch.cfm?CFRPart=820."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"642","DOI":"10.1109\/TPDS.2013.50","article-title":"From Offline toward Real Time: A Hybrid Systems Model Checking and CPS Codesign Approach for Medical Device Plug-and-Play Collaborations","volume":"25","author":"Li","year":"2014","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/s00766-013-0200-9","article-title":"Early modeling and validation of timed system requirements using Timed Use Case Maps","volume":"20","author":"Hassine","year":"2015","journal-title":"Requir. Eng."},{"key":"ref_11","unstructured":"FDA Medical Device Recall Report\u2014FY2003 to FY2012, Available online:http:\/\/www.webcitation.org\/6ZdUQoc4Q."},{"key":"ref_12","unstructured":"ASTM International ASTM F2761-09(2013). Available online:http:\/\/www.webcitation.org\/6ZdV3vBC1."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1109\/TII.2012.2226594","article-title":"Model-Driven Safety Analysis of Closed-Loop Medical Systems","volume":"10","author":"Pajic","year":"2012","journal-title":"IEEE Trans. Ind. Inform."},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1109\/JPROC.2011.2161241","article-title":"Cyber-Physical Modeling of Implantable Cardiac Medical Devices","volume":"100","author":"Jiang","year":"2012","journal-title":"IEEE Proc."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10009-013-0289-7","article-title":"Closed-loop verification of medical devices with model abstraction and refinement","volume":"16","author":"Jiang","year":"2014","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Miller, B., Vahid, F., and Givargis, T. (2012, January 28\u201330). Digital Mockups for the Testing of a Medical Ventilator. Proceedings of the 2nd ACM SIGHIT International Health Informatics Symposium (IHI), Miami, FL, USA.","DOI":"10.1145\/2110363.2110473"},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"1839","DOI":"10.1109\/TBME.2011.2176939","article-title":"Control-Relevant Models for Glucose Control Using A Priori Patient Characteristics","volume":"59","author":"Dassau","year":"2012","journal-title":"IEEE Trans. Biomed. Eng."},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Kang, W., Wu, P., Rahmaniheris, M., Sha, L., Berlin, R.B., and Goldman, J.M. (2013, January 20\u201322). Towards organ-centric compositional development of safe networked supervisory medical systems. Proceedings of the IEEE 26th International Symposium on Computer-Based Medical Systems (CBMS), Porto, Portugal.","DOI":"10.1109\/CBMS.2013.6627779"},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"King, A.L., Feng, L., Sokolsky, O., and Lee, I. (2013, January 19\u201320). Assuring the safety of on-demand medical cyber-physical systems. Proceedings of the IEEE 1st International Conference on Cyber-Physical Systems, Networks, and Applications (CPSNA), Taipei, Taiwan.","DOI":"10.1109\/CPSNA.2013.6614238"},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Simalatsar, A., and de Micheli, G. (2012, January 11\u201313). Medical guidelines reconciling medical software and electronic devices: Imatinib case-study. Proceedings of the IEEE 12th International Conference on Bioinformatics Bioengineering (BIBE), Larnaca, Cyprus.","DOI":"10.1109\/BIBE.2012.6399700"},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1109\/LES.2013.2276434","article-title":"Improving the Trustworthiness of Medical Device Software with Formal Verification Methods","volume":"5","author":"Li","year":"2013","journal-title":"IEEE Embed. Syst. Lett."},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Murugesan, A., Sokolsky, O., Rayadurgam, S., Whalen, M., Heimdahl, M., and Lee, I. (2014, January 14\u201317). Linking abstract analysis to concrete design: A hierarchical approach to verify medical CPS safety. Proceedings of the ACM\/IEEE 5th International Conference on Cyber-Physical Systems (ICCPS), Berlin, Germany.","DOI":"10.1109\/ICCPS.2014.6843718"},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Agha, G. (1986). Actors: A Model of Concurrent Computation in Distributed Systems, MIT Press.","DOI":"10.7551\/mitpress\/1086.001.0001"},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1109\/32.6156","article-title":"The TAME project: Towards improvement-oriented software environments","volume":"14","author":"Basili","year":"1988","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_25","unstructured":"Mathworks Available online:http:\/\/www.mathworks.com\/products\/sldesignverifier."},{"key":"ref_26","unstructured":"Berkeley, U.C. Available online:http:\/\/ptolemy.eecs.berkeley.edu\/ptolemyII."},{"key":"ref_27","unstructured":"Katzung, B.G., Masters, S.B., and Trevor, A.J. (2012). Basic & Clinical Pharmacology, McGraw-Hill Companies, Inc.. [12th ed.]."},{"key":"ref_28","unstructured":"Hair, J.F., Black, W.C., Babin, B.J., Anderson, R.E., and Tatham, R.L. (2009). An\u00e1lise Multivariada de Dados, Bookman. [6th ed.]."},{"key":"ref_29","unstructured":"PHYSIONET MIMIC II Databases, National Institutes of Health (NIH), 2009. Available online:http:\/\/physionet.org\/mimic2."},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"ADA (2004). Diagnosis and Classification of Diabetes Mellitus. Diabetes Care, 27, s5\u2013s10.","DOI":"10.2337\/diacare.27.2007.S5"},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"2360","DOI":"10.1016\/j.jacc.2006.09.020","article-title":"ACC\/AHA\/HRS 2006 Key Data Elements and Definitions for Electrophysiological Studies and Procedures: A Report of the American College of Cardiology\/American Heart Association Task Force on Clinical Data Standards (ACC\/AHA\/HRS Writing Committee to Develop Data Standards on Electrophysiology)","volume":"48","author":"Buxton","year":"2006","journal-title":"J. Am. Coll. Cardiol."},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"1206","DOI":"10.1161\/01.HYP.0000107251.49515.c2","article-title":"Seventh Report of the Joint National Committee on Prevention, Detection, Evaluation, and Treatment of High Blood Pressure","volume":"42","author":"Chobanian","year":"2003","journal-title":"Hypertension"},{"key":"ref_33","doi-asserted-by":"crossref","first-page":"287","DOI":"10.4158\/EP.17.2.287","article-title":"American Association of Clinical Endocrinologists Medical Guidelines for Clinical Practice for Developing a Diabetes Mellitus Comprehensive Care Plan: Executive Summary","volume":"17","author":"Handelsman","year":"2011","journal-title":"Endocr. Pract."},{"key":"ref_34","unstructured":"McGee, S.R. (2007). Evidence-Based Physical Diagnosis, Saunders Elsevier. [2nd ed.]."},{"key":"ref_35","doi-asserted-by":"crossref","unstructured":"NHBPEP (2004). The Fourth Report on the Diagnosis, Evaluation, and Treatment of High Blood Pressure in Children and Adolescents. Pediatrics, 114, 555\u2013576.","DOI":"10.1542\/peds.114.2.S2.555"},{"key":"ref_36","unstructured":"Jain, R. (1991). The Art of Computer Systems Performance Analysis: Techniques for Experimental Design, Measurement, Simulation, and Modeling, John Wiley & Sons, Inc."},{"key":"ref_37","doi-asserted-by":"crossref","unstructured":"McCullagh, P., and Nelder, J.A. (1989). Generalized Linear Models, Chapman and Hall. [2nd ed.].","DOI":"10.1007\/978-1-4899-3242-6"},{"key":"ref_38","doi-asserted-by":"crossref","unstructured":"Cassandras, C.G., and Lafortune, S. (2008). Introduction to Discrete Event Systems, Springer. [2nd ed.].","DOI":"10.1007\/978-0-387-68612-7"},{"key":"ref_39","unstructured":"Mathworks PID Controller, Discrete PID Controller. Available online:http:\/\/www.mathworks.com\/help\/simulink\/slref\/pidcontroller.html."},{"key":"ref_40","unstructured":"Mathworks MATLAB. Available online:http:\/\/www.mathworks.com\/products\/matlab\/."},{"key":"ref_41","doi-asserted-by":"crossref","first-page":"1456","DOI":"10.1172\/JCI110398","article-title":"Physiologic Evaluation of Factors Controlling Glucose Tolerance in Man: Measurement of Insulin Sensitivity and Beta-Cell Glucose Sensitivity from the Response to Intravenous Glucose","volume":"68","author":"Bergman","year":"1981","journal-title":"J. Clin. Investig."},{"key":"ref_42","doi-asserted-by":"crossref","first-page":"3093","DOI":"10.1007\/s13369-012-0456-2","article-title":"Artificial Pancreas Coupled Vital Signs Monitoring for Improved Patient Safety","volume":"38","author":"Khan","year":"2013","journal-title":"Arab. J. Sci. Eng."},{"key":"ref_43","unstructured":"Franklin, G.F., Powell, J.D., and Emami-Naeini, A. (2002). Feedback Control of Dynamic Systems, Prentice Hall. [4th ed.]."},{"key":"ref_44","unstructured":"Ogata, K. (1997). Modern Control Engineering, Prentice Hall. [3rd ed.]."},{"key":"ref_45","unstructured":"FDA Classify Your Medical Device. Available online:http:\/\/www.webcitation.org\/6ZdUv0YwI."},{"key":"ref_46","unstructured":"ROCHE ACCU-CHEK Spirit Insulin Pump System: Pump User Guide. Available online:http:\/\/www.webcitation.org\/6ZdVHOgBx."},{"key":"ref_47","unstructured":"Diabetes.co.uk Basal Bolus\u2014Basal Bolus Injection Regimen. Available online:http:\/\/www.webcitation.org\/6ZdVLD7NE."},{"key":"ref_48","unstructured":"Lee, E.A., and Seshia, S.A. (2015). Introduction to Embedded Systems, A Cyber-Physical Systems Approach, LeeSeshia.Org.. [2nd ed.]."},{"key":"ref_49","doi-asserted-by":"crossref","unstructured":"Silva, L.C., Perkusich, M., Bublitz, F.M., Almeida, H.O., and Perkusich, A. (2014, January 24\u201328). A Model-Based Architecture for Testing Medical Cyber-Physical Systems. Proceedings of the 29th Annual ACM Symposium on Applied Computing (SAC), Gyeongju, Korea.","DOI":"10.1145\/2554850.2555028"},{"key":"ref_50","unstructured":"Ptolemaeus, C. (2014). System Design, Modeling, and Simulation Using Ptolemy II, Ptolemy.Org."},{"key":"ref_51","unstructured":"Silva, L.C., Almeida, H.O., Perkusich, A., and Perkusich, M. A Model-Based Approach to Support Validation of Medical Cyber-Physical Systems. Available online:http:\/\/sites.google.com\/site\/mbatomcps\/."},{"key":"ref_52","unstructured":"NIH (2014). Asthma, Available online:http:\/\/www.nhlbi.nih.gov\/health\/health-topics\/topics\/asthma."},{"key":"ref_53","unstructured":"WHO 10 Facts about Diabetes. Available online:http:\/\/www.webcitation.org\/6ZdVT2Scz."},{"key":"ref_54","unstructured":"WHO World Health Statistics. Available online:http:\/\/www.who.int\/gho\/publications\/world_health_statistics\/2012\/en\/."},{"key":"ref_55","first-page":"219","article-title":"Gerenciamento Eletr\u00f4nico do Diabetes","volume":"9","author":"Gomes","year":"2009","journal-title":"Dir. Soc. Bras. Diabetes"},{"key":"ref_56","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/52.391832","article-title":"Case studies for method and tool evaluation","volume":"12","author":"Kitchenham","year":"1995","journal-title":"IEEE Softw"},{"key":"ref_57","unstructured":"Washizaki, H., Yamamoto, H., and Fukazawa, Y. (2004, January 5). A metrics suite for measuring reusability of software components. Proceedings of the 2003 Ninth International Software Metrics Symposium, Sydney, Australia."},{"key":"ref_58","unstructured":"Mathworks Stateflow, 2014. Available online:http:\/\/www.mathworks.com\/products\/stateflow\/."},{"key":"ref_59","unstructured":"Utting, M., and Legeard, B. (2007). Practical Model-Based Testing: A Tools Approach, Morgan Kaufmann Publishers Inc."},{"key":"ref_60","unstructured":"Bacic, M. (2005, January 12\u201315). On hardware-in-the-loop simulation. Proceedings of the 44th IEEE Conference on Decision and Control and the European Control Conference (CDC-ECC), Seville, Spain."}],"container-title":["Sensors"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1424-8220\/15\/11\/27625\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T20:51:11Z","timestamp":1760215871000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1424-8220\/15\/11\/27625"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,10,30]]},"references-count":60,"journal-issue":{"issue":"11","published-online":{"date-parts":[[2015,11]]}},"alternative-id":["s151127625"],"URL":"https:\/\/doi.org\/10.3390\/s151127625","relation":{},"ISSN":["1424-8220"],"issn-type":[{"value":"1424-8220","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,10,30]]}}}