Evaluating On-line Model Checking in UPPAAL-SMC using a Laser Tracheotomy Case Study

Ma, Xintao; Rinast, Jonas; Schupp, Sibylle; Gollmann, Dieter

doi:10.4230/OASIcs.MCPS.2014.100

Document

Evaluating On-line Model Checking in UPPAAL-SMC using a Laser Tracheotomy Case Study

Authors Xintao Ma, Jonas Rinast, Sibylle Schupp, Dieter Gollmann

Part of: Volume: 5th Workshop on Medical Cyber-Physical Systems (MCPS 2014)
Part of: Series: Open Access Series in Informatics (OASIcs)
License: Creative Commons Attribution 3.0 Unported license
Publication Date: 2014-04-14

PDF

File

PDF

OASIcs.MCPS.2014.100.pdf

Filesize: 433 kB
13 pages

Document Identifiers

DOI: 10.4230/OASIcs.MCPS.2014.100
URN: urn:nbn:de:0030-drops-45279

Subject Classification

Keywords

On-line Model Checking
Laser Tracheotomy
UPPAAL-SMC
Patient-in-the-loop

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Abstract

On-line model checking is a variant of model checking that evaluates properties of a system concurrently while deployed, which allows overcoming limitations of inaccurate system models. In this paper we conduct a laser tracheotomy case study to evaluate the feasibility of using the statistical model checker UPPAAL-SMC for on-line model checking in a medical application. Development of automatic on-line model checking relies on the precision of the prediction and real-time capabilities as real-time requirements must be met. We evaluate the case study with regards to these qualities and our results show that using UPPAAL-SMC in an on-line model checking context is practical: relative prediction errors were only 2% on average and guarantees could be established within reasonable time during our experiments.

Cite As Get BibTex

Xintao Ma, Jonas Rinast, Sibylle Schupp, and Dieter Gollmann. Evaluating On-line Model Checking in UPPAAL-SMC using a Laser Tracheotomy Case Study. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 100-112, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/OASIcs.MCPS.2014.100

Author Details

Xintao Ma

Jonas Rinast

Sibylle Schupp

Dieter Gollmann

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail