Design Verifiably Correct Model Patterns to Facilitate Modeling Medical Best Practice Guidelines with Statecharts

Chunhui Guo, Zhicheng Fu, Zhenyu Zhang, Shangping Ren, Lui Sha

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish (US)
Article number8521661
Pages (from-to)6276-6284
Number of pages9
JournalIEEE Internet of Things Journal
Volume6
Issue number4
DOIs
StatePublished - Aug 2019
Externally publishedYes

Fingerprint

Communication
Semantics
Laser surgery
Rapid prototyping
Cyber Physical System

Keywords

  • Medical guideline modeling
  • statechart models
  • verifiably correct model patterns

ASJC Scopus subject areas

  • Signal Processing
  • Information Systems
  • Hardware and Architecture
  • Computer Science Applications
  • Computer Networks and Communications

Cite this

Design Verifiably Correct Model Patterns to Facilitate Modeling Medical Best Practice Guidelines with Statecharts. / Guo, Chunhui; Fu, Zhicheng; Zhang, Zhenyu; Ren, Shangping; Sha, Lui.

In: IEEE Internet of Things Journal, Vol. 6, No. 4, 8521661, 08.2019, p. 6276-6284.

Research output: Contribution to journalArticle

Guo, Chunhui ; Fu, Zhicheng ; Zhang, Zhenyu ; Ren, Shangping ; Sha, Lui. / Design Verifiably Correct Model Patterns to Facilitate Modeling Medical Best Practice Guidelines with Statecharts. In: IEEE Internet of Things Journal. 2019 ; Vol. 6, No. 4. pp. 6276-6284.
@article{6c953817020c42bba687418148370d28,
title = "Design Verifiably Correct Model Patterns to Facilitate Modeling Medical Best Practice Guidelines with Statecharts",
abstract = "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.",
keywords = "Medical guideline modeling, statechart models, verifiably correct model patterns",
author = "Chunhui Guo and Zhicheng Fu and Zhenyu Zhang and Shangping Ren and Lui Sha",
year = "2019",
month = "8",
doi = "10.1109/JIOT.2018.2879475",
language = "English (US)",
volume = "6",
pages = "6276--6284",
journal = "IEEE Internet of Things Journal",
issn = "2327-4662",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
number = "4",

}

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

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

VL - 6

SP - 6276

EP - 6284

JO - IEEE Internet of Things Journal

JF - IEEE Internet of Things Journal

SN - 2327-4662

IS - 4

M1 - 8521661

ER -