License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.MCPS.2014.100
URN: urn:nbn:de:0030-drops-45279
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4527/
Go to the corresponding OASIcs Volume Portal

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

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

pdf-format:
12.pdf (0.4 MB)

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.

BibTeX - Entry

@InProceedings{ma_et_al:OASIcs:2014:4527,
  author =	{Xintao Ma and Jonas Rinast and Sibylle Schupp and Dieter Gollmann},
  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 =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-66-8},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{36},
  editor =	{Volker Turau and Marta Kwiatkowska and Rahul Mangharam and Christoph Weyer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4527},
  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}
}

Keywords: On-line Model Checking, Laser Tracheotomy, UPPAAL-SMC, Patient-in-the-loop
Collection: 5th Workshop on Medical Cyber-Physical Systems
Issue Date: 2014
Date of publication: 14.04.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI