DROPS

Document

DOI: 10.4230/OASIcs.MCPS.2014.100

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

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

Published in: OASIcs, Volume 36, 5th Workshop on Medical Cyber-Physical Systems (2014)

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

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)

Copy BibTex To Clipboard

@InProceedings{ma_et_al:OASIcs.MCPS.2014.100,
  author =	{Ma, Xintao and Rinast, Jonas and Schupp, Sibylle and Gollmann, Dieter},
  title =	{{Evaluating On-line Model Checking in UPPAAL-SMC using a Laser Tracheotomy Case Study}},
  booktitle =	{5th Workshop on Medical Cyber-Physical Systems},
  pages =	{100--112},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-66-8},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{36},
  editor =	{Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.MCPS.2014.100},
  URN =		{urn:nbn:de:0030-drops-45279},
  doi =		{10.4230/OASIcs.MCPS.2014.100},
  annote =	{Keywords: On-line Model Checking, Laser Tracheotomy, UPPAAL-SMC, Patient-in-the-loop}
}

Search Results

Documents authored by Rinast, Jonas

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

Abstract

Cite as

Thanks for your feedback!

Could not send message