Document Open Access Logo

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

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

Thumbnail PDF


  • Filesize: 433 kB
  • 13 pages

Document Identifiers

Author Details

Xintao Ma
Jonas Rinast
Sibylle Schupp
Dieter Gollmann

Cite AsGet 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)


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.
  • On-line Model Checking
  • Laser Tracheotomy
  • Patient-in-the-loop


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
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