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.
@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} }
Feedback for Dagstuhl Publishing