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

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

Fingerprint Dive into the research topics of 'Design Verifiably Correct Model Patterns to Facilitate Modeling Medical Best Practice Guidelines with Statecharts'. Together they form a unique fingerprint.

  • Cite this