OASIcs.MCPS.2014.100.pdf
- Filesize: 433 kB
- 13 pages
Document
Evaluating On-line Model Checking in UPPAAL-SMC using a Laser Tracheotomy Case Study
Authors
-
Part of:
Volume:
5th Workshop on Medical Cyber-Physical Systems
Series: Open Access Series in Informatics (OASIcs) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2014-04-14
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)
https://doi.org/10.4230/OASIcs.MCPS.2014.100
https://doi.org/10.4230/OASIcs.MCPS.2014.100
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.
Keywords
- On-line Model Checking
- Laser Tracheotomy
- UPPAAL-SMC
- Patient-in-the-loop
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads