title: A Model-Based Approach to Support Validation of Medical Cyber-Physical Systems.
abstract: 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.
authors.affiliation: Embedded Systems and Pervasive Computing Laboratory, Federal University of Campina Grande, 882 Aprígio Veloso Street, Universitário, Campina Grande 58429-900, Brazil. lenardo.silva@embedded.ufcg.edu.br.
authors.forename: Lenardo C
authors.initials: LC
authors.lastname: Silva
authors.affiliation: Embedded Systems and Pervasive Computing Laboratory, Federal University of Campina Grande, 882 Aprígio Veloso Street, Universitário, Campina Grande 58429-900, Brazil. hyggo@dsc.ufcg.edu.br.
authors.forename: Hyggo O
authors.initials: HO
authors.lastname: Almeida
authors.affiliation: Embedded Systems and Pervasive Computing Laboratory, Federal University of Campina Grande, 882 Aprígio Veloso Street, Universitário, Campina Grande 58429-900, Brazil. perkusic@dee.ufcg.edu.br.
authors.forename: Angelo
authors.initials: A
authors.lastname: Perkusich
authors.affiliation: Embedded Systems and Pervasive Computing Laboratory, Federal University of Campina Grande, 882 Aprígio Veloso Street, Universitário, Campina Grande 58429-900, Brazil. mirko.perkusich@embedded.ufcg.edu.br.
authors.forename: Mirko
authors.initials: M
authors.lastname: Perkusich
mesh_terms: D003198:Computer Simulation; D003491:Cybernetics; D003695:Delivery of Health Care / Q000379:methods / Q000592:standards; D004864:Equipment and Supplies; D006801:Humans; D008490:Medical Informatics / Q000379:methods / Q000592:standards; D008962:Models, Theoretical; D008991:Monitoring, Physiologic / Q000379:methods / Q000592:standards; D061214:Patient Safety; D012044:Regression Analysis
keywords: clinical scenarios; early validation; formal methods; medical cyber-physical systems; medical devices; model-based development; patient model; simulation