TY - JOUR
T1 - A framework for supporting the development of verifiably safe medical best practice guideline systems
AU - Guo, Chunhui
AU - Fu, Zhicheng
AU - Zhang, Zhenyu
AU - Ren, Shangping
AU - Sha, Lui
N1 - Funding Information:
This work is supported in part by NSF CNS 1842710 , NSF CNS 1545008 , and NSF CNS 1545002 . Chunhui Guo is a Postdoc Researcher of the Department of Computer Science at San Diego State University. He obtained his Ph.D. in Computer Science from Illinois Institute of Technology in 2019. His research interests include Cyber-Physical Systems, Internet-of-Things, and Real-Time Systems. Zhicheng Fu is now a Ph.D. candidate in the Department of Computer Science at Illinois Institute of Technology. He earned his B.S. from Wuhan University, China, in 2011. His current research interests mainly focus on domain specific modeling, assumption management in system development and Cyber-Physical Systems. Zhenyu Zhang is now a Ph.D. candidate in the Department of Computer Science at San Diego State University. His research interests are in distributed systems and Cyber-Physical Systems. He earned his B.S. degree from the Wuhan University, China, in 2012 and his M.S. degree from the University of Wisconsin – La Crosse, in 2014. Shangping Ren is a Professor and the Chair of the Department of Computer Science at San Diego State University. She obtained her Ph.D. in CS from UIUC in 1997. Before she joined SDSU in 2018, she was a Professor at the Department of Computer Science in Illinois Institute of Technology from 2003 to 2017 and worked as a software engineer in industry for over five years. Her research interests are in the areas of cyber-physical systems, distributed systems, real-time systems, software engineering and cloud computing with focus on safety improvement of medical cyber-physical systems, and their software architecture and development, system reliability analysis under resource and deadline constraints, scheduling algorithm design for meeting reliability and deadline requirements, and resource optimization under cloud environment. Her research has been funded by NSF, Air Force Research Laboratory and Fermi National Accelerator Laboratory. Lui Sha graduated with Ph.D. from CMU in 1985. Currently, he is Donald B. Gillies Chair Professor of Computer Science and Drucker Eminent Faculty, University of Illinois at Urbana Champaign. In recent years, his team is developing the technologies for secure and certifiable multi-core avionics with aviation community and computational pathophysiology models for medical best practice guidance (“GPS”) systems with medical community. He is a co-recipient of IEEE Simon Ramo Medal (2016) and was a member of NASA Advisory Council (2015–2017) and a member of National Academy of Science’s Committee on Certifiably Dependable Software (2002–2004). He is a co-recipient of David Lubkowski Award for the Advancement of Digital Avionics (2009). He is a fellow of the IEEE and the ACM.
Funding Information:
This work is supported in part by NSF CNS 1842710, NSF CNS 1545008, and NSF CNS 1545002.
Publisher Copyright:
© 2019 Elsevier B.V.
PY - 2020/3
Y1 - 2020/3
N2 - Improving safety of patient care is an ultimate objective for medical systems. Though many medical best practice guidelines exist and are in hospital handbooks, they are often lengthy and difficult for medical professionals to remember and apply clinically. Hence, developing safe medical best practice guideline systems is an urgent need. The paper presents a framework to support the development of verifiably safe medical best practice guideline systems. The framework facilitates medical professionals’ participation in computer modeling, clinical validation, formal verification and root cause identification of safety failures at both model and code levels. To implement the framework, our strategies are to maximally utilize existing models/tools designed for validation and verification respectively, but build bridges among different selected models/tools. In particular, we use statechart tool to build statechart models for medical best practice guidelines and use statechart models to interact with medical professionals for clinical validations. The statechart models are then automatically transformed to verifiable models by the framework so that the safety properties can be formally verified. The computer models that are both validated by medical professionals and verified by formal verification tools are then used to generate computer executable code. To improve code level safety, the framework further transforms safety properties specified at the model level to runtime code monitors to ensure that these safety properties are complied at runtime. We use a simplified version of cardiac arrest treatment scenario provided to our team by Carle Foundation Hospital as a case study to evaluate the framework in developing a verifiably safe medical system.
AB - Improving safety of patient care is an ultimate objective for medical systems. Though many medical best practice guidelines exist and are in hospital handbooks, they are often lengthy and difficult for medical professionals to remember and apply clinically. Hence, developing safe medical best practice guideline systems is an urgent need. The paper presents a framework to support the development of verifiably safe medical best practice guideline systems. The framework facilitates medical professionals’ participation in computer modeling, clinical validation, formal verification and root cause identification of safety failures at both model and code levels. To implement the framework, our strategies are to maximally utilize existing models/tools designed for validation and verification respectively, but build bridges among different selected models/tools. In particular, we use statechart tool to build statechart models for medical best practice guidelines and use statechart models to interact with medical professionals for clinical validations. The statechart models are then automatically transformed to verifiable models by the framework so that the safety properties can be formally verified. The computer models that are both validated by medical professionals and verified by formal verification tools are then used to generate computer executable code. To improve code level safety, the framework further transforms safety properties specified at the model level to runtime code monitors to ensure that these safety properties are complied at runtime. We use a simplified version of cardiac arrest treatment scenario provided to our team by Carle Foundation Hospital as a case study to evaluate the framework in developing a verifiably safe medical system.
KW - Medical cyber-physical systems
KW - Medical guideline models
KW - Runtime verification
KW - Validation and verification
UR - http://www.scopus.com/inward/record.url?scp=85076866059&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85076866059&partnerID=8YFLogxK
U2 - 10.1016/j.sysarc.2019.101693
DO - 10.1016/j.sysarc.2019.101693
M3 - Article
AN - SCOPUS:85076866059
SN - 1383-7621
VL - 104
JO - Journal of Systems Architecture
JF - Journal of Systems Architecture
M1 - 101693
ER -