TY - JOUR
T1 - Design Verifiably Correct Model Patterns to Facilitate Modeling Medical Best Practice Guidelines with Statecharts
AU - Guo, Chunhui
AU - Fu, Zhicheng
AU - Zhang, Zhenyu
AU - Ren, Shangping
AU - Sha, Lui
N1 - Funding Information:
Manuscript received May 22, 2018; revised October 1, 2018; accepted October 27, 2018. Date of publication November 5, 2018; date of current version July 31, 2019. This work was supported by the National Science Foundation under Grant NSF CNS 1545008, Grant NSF CNS 1842710, and Grant NSF CNS 1545002. (Corresponding author: Chunhui Guo.) C. Guo and Z. Fu are with the Department of Computer Science, Illinois Institute of Technology, Chicago, IL 60616 USA (e-mail: cguo13@hawk.iit.edu; zfu11@hawk.iit.edu).
Publisher Copyright:
© 2014 IEEE.
PY - 2019/8
Y1 - 2019/8
N2 - Improving patient care safety is an ultimate objective for medical cyber-physical systems. A recent study shows that the patients' death rate can be significantly reduced by computerizing medical best practice guidelines. To facilitate the development of computerized medical best practice guidelines, statecharts are often used as a modeling tool because of their high resemblances to disease and treatment models and their capabilities to provide rapid prototyping and simulation for clinical validations. However, some implementations of statecharts, such as Yakindu statecharts, are priority-based and have synchronous execution semantics which makes it difficult to model certain functionalities that are essential in modeling medical guidelines, such as two-way communications and configurable execution orders. Rather than introducing new statechart elements or changing the statechart implementation's underline semantics, we use existing basic statechart elements to design model patterns for the commonly occurring issues. In particular, we show the design of model patterns for two-way communications and configurable execution orders and formally prove the correctness of these model patterns. We further use a simplified airway laser surgery scenario as a case study to demonstrate how the developed model patterns address the two-way communication and configurable execution order issues and their impact on validation and verification of medical safety properties.
AB - Improving patient care safety is an ultimate objective for medical cyber-physical systems. A recent study shows that the patients' death rate can be significantly reduced by computerizing medical best practice guidelines. To facilitate the development of computerized medical best practice guidelines, statecharts are often used as a modeling tool because of their high resemblances to disease and treatment models and their capabilities to provide rapid prototyping and simulation for clinical validations. However, some implementations of statecharts, such as Yakindu statecharts, are priority-based and have synchronous execution semantics which makes it difficult to model certain functionalities that are essential in modeling medical guidelines, such as two-way communications and configurable execution orders. Rather than introducing new statechart elements or changing the statechart implementation's underline semantics, we use existing basic statechart elements to design model patterns for the commonly occurring issues. In particular, we show the design of model patterns for two-way communications and configurable execution orders and formally prove the correctness of these model patterns. We further use a simplified airway laser surgery scenario as a case study to demonstrate how the developed model patterns address the two-way communication and configurable execution order issues and their impact on validation and verification of medical safety properties.
KW - Medical guideline modeling
KW - statechart models
KW - verifiably correct model patterns
UR - http://www.scopus.com/inward/record.url?scp=85056168641&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85056168641&partnerID=8YFLogxK
U2 - 10.1109/JIOT.2018.2879475
DO - 10.1109/JIOT.2018.2879475
M3 - Article
AN - SCOPUS:85056168641
SN - 2327-4662
VL - 6
SP - 6276
EP - 6284
JO - IEEE Internet of Things Journal
JF - IEEE Internet of Things Journal
IS - 4
M1 - 8521661
ER -