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

Any Issues?

Feedback on the Current Page

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail