Volume
OASIcs, Volume 36
5th Workshop on Medical Cyber-Physical Systems
- Part of: Series: Open Access Series in Informatics (OASIcs)
Event
MCPS 2014, April 14, 2014, Berlin, GermanyEditors
Publication Details
- published at: 2014-04-14
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-66-8
- DBLP: db/conf/mcps/mcps2014
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
OASIcs, Volume 36, MCPS'14, Complete Volume
Abstract
OASIcs, Volume 36, MCPS'14, Complete Volume
Cite as
5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@Proceedings{turau_et_al:OASIcs.MCPS.2014,
title = {{OASIcs, Volume 36, MCPS'14, Complete Volume}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
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},
URN = {urn:nbn:de:0030-drops-45403},
doi = {10.4230/OASIcs.MCPS.2014},
annote = {Keywords: Conference proceedings}
}
Document
Front Matter
Frontmatter, Table of Contents, Preface, Workshop Organization
Abstract
Frontmatter, Table of Contents, Preface, Workshop Organization
Cite as
5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. i-x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{turau_et_al:OASIcs.MCPS.2014.i,
author = {Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
title = {{Frontmatter, Table of Contents, Preface, Workshop Organization}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {i--x},
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.i},
URN = {urn:nbn:de:0030-drops-45174},
doi = {10.4230/OASIcs.MCPS.2014.i},
annote = {Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}
Document
A Generic User Interface Architecture for Analyzing Use Hazards in Infusion Pump Software
Abstract
This paper presents a generic infusion pump user interface (GIP-UI) architecture that intends to capture the common characteristics and functionalities of interactive software incorporated in broad classes of infusion pumps. It is designed to facilitate the identification of use hazards and their causes in infusion pump designs. This architecture constitutes our first effort at establishing a model-based risk analysis methodology that helps manufacturers identify and mitigate use hazards in their products at early stages of the development life-cycle.
The applicability of the GIP-UI architecture has been confirmed in a hazard analysis focusing on the number entry software of existing infusion pumps, in which the GIP-UI architecture is used to identify a substantial set of user interface design errors that may contribute to use hazards found in infusion pump incidents.
Cite as
Paolo Masci, Yi Zhang, Paul Jones, Harold Thimbleby, and Paul Curzon. A Generic User Interface Architecture for Analyzing Use Hazards in Infusion Pump Software. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{masci_et_al:OASIcs.MCPS.2014.1,
author = {Masci, Paolo and Zhang, Yi and Jones, Paul and Thimbleby, Harold and Curzon, Paul},
title = {{A Generic User Interface Architecture for Analyzing Use Hazards in Infusion Pump Software}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {1--14},
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.1},
URN = {urn:nbn:de:0030-drops-45185},
doi = {10.4230/OASIcs.MCPS.2014.1},
annote = {Keywords: Infusion Pump, Hazard analysis, Use hazards, User Interface, Interactive software, Design errors}
}
Document
An Approach to Integrate Distributed Systems of Medical Devices in High Acuity Environments
Abstract
This paper presents a comprehensive solution to build a distributed system of medical devices in high acuity environments. It is based on the concept of a Service Oriented Medical Device Architecture. It uses the Devices Profile for Web Services as a transport layer protocol and enhances it to the Medical Devices Profile for Web Service (MDPWS) to meet medical requirements. By applying the ISO/IEEE 11073 Domain Information Model, device data can be semantically described and exchanged by means of a generic service interface. Data model and service interface are subsumed under the Basic Integrated Clinical Environment Specification (BICEPS).
MDPWS and BICEPS are implemented as part of the publically available openSDC stack. Performance measurements and a real world setup prove that openSDC is feasible to be deployed in distributed systems of medical devices.
Cite as
David Gregorczyk, Stefan Fischer, Timm Busshaus, Stefan Schlichting, and Stephan Pöhlsen. An Approach to Integrate Distributed Systems of Medical Devices in High Acuity Environments. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 15-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{gregorczyk_et_al:OASIcs.MCPS.2014.15,
author = {Gregorczyk, David and Fischer, Stefan and Busshaus, Timm and Schlichting, Stefan and P\"{o}hlsen, Stephan},
title = {{An Approach to Integrate Distributed Systems of Medical Devices in High Acuity Environments}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {15--27},
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.15},
URN = {urn:nbn:de:0030-drops-45191},
doi = {10.4230/OASIcs.MCPS.2014.15},
annote = {Keywords: Integrated Clinical Environment, Devices Profile for Web Services, ISO/IEEE 11073}
}
Document
Simulations of the Cardiovascular System Using the Cardiovascular Simulation Toolbox
Abstract
In the present document, six mathematical models of the cardiovascular system are studied and implemented in MATLAB R2013a using an updated version of the Cardiovascular Simulation Toolbox proposed by O. Barnea at the Tel-Aviv University. All the mathematical models are based on electrical lumped-parameter analogies. The results of the simulations are compared with a list of expected hemodynamic parameters and contrasted with laboratory values.
Cite as
Gabriela Ortiz-León, Marta Vílchez-Monge, and Juan J. Montero-Rodríguez. Simulations of the Cardiovascular System Using the Cardiovascular Simulation Toolbox. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 28-37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{ortizleon_et_al:OASIcs.MCPS.2014.28,
author = {Ortiz-Le\'{o}n, Gabriela and V{\'\i}lchez-Monge, Marta and Montero-Rodr{\'\i}guez, Juan J.},
title = {{Simulations of the Cardiovascular System Using the Cardiovascular Simulation Toolbox}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {28--37},
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.28},
URN = {urn:nbn:de:0030-drops-45207},
doi = {10.4230/OASIcs.MCPS.2014.28},
annote = {Keywords: Biomedic, Cardiovascular, MATLAB, Simulation}
}
Document
Adaptive Failure Detection and Correction in Dynamic Patient-Networks
Abstract
Wireless sensors have been studied over recent years for different promising applications with high value for individuals and society. A good example are wireless sensor networks for patients allowing for better and more efficient monitoring of patients in hospitals or even early discharge form hospital and monitoring at home. These visions have hardly led research as reliability is and issue with wireless networks to be known error-prone. In life critical applications like health care this is not an aspect to be handled carelessly. Fail-safety is an important property for patient monitoring systems.
The AA4R project of the Hamburg University of Technology researches on a fail-safe patient monitoring system. Our vision is a dynamically distributed system using suitable devices in the area of a patient. The data in the network is stored with redundancy on several nodes. Patient data is analyzed in the network and uploaded to a medical server.
As devices appear, disappear and fail, so do the services being executed on those devices. This article focuses on a Reincarnation Service (RS) to track the functionality of the processes. The RS takes suitable actions when a failure is detected to correct or isolate the failure. Checking of the nodes is done adaptively to achieve a good response time to failures and reduce the power consumption.
Cite as
Martin Ringwelski, Andreas Timm-Giel, and Volker Turau. Adaptive Failure Detection and Correction in Dynamic Patient-Networks. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 38-48, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{ringwelski_et_al:OASIcs.MCPS.2014.38,
author = {Ringwelski, Martin and Timm-Giel, Andreas and Turau, Volker},
title = {{Adaptive Failure Detection and Correction in Dynamic Patient-Networks}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {38--48},
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.38},
URN = {urn:nbn:de:0030-drops-45215},
doi = {10.4230/OASIcs.MCPS.2014.38},
annote = {Keywords: Wireless Sensor Networks, Fail-Safety, Health Monitoring, Failure Masking, Distributed Systems}
}
Document
Challenges and Opportunities in Design of Control Algorithm for Artificial Pancreas
Abstract
With discovery of the insulin, Type-1 diabetes converted from a fatal and acute to a chronic disease which includes micro-vascular complications which range from Kidney disease to stroke and micro-vascular complications such as retinopathy, nephropathy and neuropathy. Artificial pancreas is a solution to improve the quality of life for people with this very fast growing disease in the world and to reduce the costs. Despite technological advances e.g., in subcutaneous sensors and actuators for insulin injection, modeling of blood glucose dynamics and control algorithms still need significant improvement. In this paper, we investigate challenges and opportunities for development of efficient algorithm for designing robust artificial pancreas. We discuss the state of the art and summarize clinical and in silico assessment results. We contrast conventional integer order system approach with a newly proposed fractal control and summarize its benefits.
Cite as
Mahboobeh Ghorbani and Paul Bogdan. Challenges and Opportunities in Design of Control Algorithm for Artificial Pancreas. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 49-57, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{ghorbani_et_al:OASIcs.MCPS.2014.49,
author = {Ghorbani, Mahboobeh and Bogdan, Paul},
title = {{Challenges and Opportunities in Design of Control Algorithm for Artificial Pancreas}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {49--57},
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.49},
URN = {urn:nbn:de:0030-drops-45221},
doi = {10.4230/OASIcs.MCPS.2014.49},
annote = {Keywords: Cyber-Physical Systems, Artificial Pancreas, Optimal and Model Predictive Control, Fractal Model Predictive}
}
Document
Automatic Resource Scaling for Medical Cyber-Physical Systems Running in Private Cloud Computing Architecture
Abstract
Cloud computing and its related virtualization technologies have become one of dominant trends to deploy software, compute difficult problems, store different types of data, and stream real-time video and audio. Due to its benefits from cost-efficiency and scalability to maintain server solutions, many organizations are migrating their server applications running on physical servers to virtual servers in cloud computing infrastructures. Moreover, cloud computing has enabled mobile and battery-powered devices to operate without strong processing power and large storage capacity. However, it is not trivial to use this trendy technology for medical Cyber Physical Systems (CPSs) which require processing tasks’ requests to send instructions to the local actuator within specified deadlines. Since a medical CPS device monitoring a patient’s vital signs may not have a second chance to recover from an erroneous state, achieving cost-efficiency with higher resource utilization in cloud computing may not be the ultimate goal to configure the healthcare IT infrastructure with medical CPS devices. In this paper, we focus on private cloud infrastructures with the fair resource sharing mechanism in order to run medical CPS applications. First, we introduce our medical CPS device model used for designing our cloud infrastructure following the Integrated Clinical Environment (ICE) standard developed by the Medical Device Plug-and-Play (MDPnP) project. Second, we investigate limitations to deploy CPS applications using existing auto-scaling mechanisms. Finally, we propose our novel middleware with a virtual resource sharing mechanism inspired by autonomic computing, and present its performance evaluation results simulated in the OpenStack private cloud.
Cite as
Yong woon Ahn and Albert Mo Kim Cheng. Automatic Resource Scaling for Medical Cyber-Physical Systems Running in Private Cloud Computing Architecture. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 58-65, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{ahn_et_al:OASIcs.MCPS.2014.58,
author = {Ahn, Yong woon and Cheng, Albert Mo Kim},
title = {{Automatic Resource Scaling for Medical Cyber-Physical Systems Running in Private Cloud Computing Architecture}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {58--65},
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.58},
URN = {urn:nbn:de:0030-drops-45234},
doi = {10.4230/OASIcs.MCPS.2014.58},
annote = {Keywords: Auto-Scaling, Cloud Computing, Medical Cyber-Physical System Device, Virtualization, Autonomic-Computing}
}
Document
Modeling of Reconfigurable Medical Ultrasonic Applications in BIP
Abstract
Medical ultrasonic imaging applications require high quality of images produced in real-time often with limited resources available.
Deadlock-freedom and confluency must be guaranteed to ensure the correctness of the applications, while feasibility and optimality properties are required to provide the best Quality of Service (QoS) within available resources. In this paper we introduce BIP (Behavior-Interaction-Priority) framework components as main building blocks to model such applications in a correct-by-construction manner. Based on those components we model a reconfigurable multi-mode processing pipeline for ultrasonic imaging that supports QoS management by topology reconfiguration. Finally, as a proof of concept, we present a simple quality controller as a well-triggered component, which when combined with the processing pipeline can manipulate the quality of image processing.
Cite as
Stefanos Skalistis and Alena Simalatsar. Modeling of Reconfigurable Medical Ultrasonic Applications in BIP. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 66-79, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{skalistis_et_al:OASIcs.MCPS.2014.66,
author = {Skalistis, Stefanos and Simalatsar, Alena},
title = {{Modeling of Reconfigurable Medical Ultrasonic Applications in BIP}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {66--79},
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.66},
URN = {urn:nbn:de:0030-drops-45246},
doi = {10.4230/OASIcs.MCPS.2014.66},
annote = {Keywords: Reconfigurable Pipelines, Quality of Service, Medical Ultrasonic Applications, Component-based System Design, Behavior-Interaction-Priority Modal Flow}
}
Document
A Domain Specific Language for Performance Evaluation of Medical Imaging Systems
Abstract
We propose iDSL, a domain specific language and toolbox for performance evaluation of Medical Imaging Systems. iDSL provides transformations to MoDeST models, which are in turn converted into UPPAAL and discrete-event MODES models. This enables automated performance evaluation by means of model checking and simulations. iDSL presents its results visually. We have tested iDSL on two example image processing systems. iDSL has successfully returned differentiated delays, resource utilizations and delay bounds. Hence, iDSL helps in evaluating and choosing between design alternatives, such as the effects of merging subsystems onto one platform or moving functionality from one platform to another.
Cite as
Freek van den Berg, Anne Remke, and Boudewijn R. Haverkort. A Domain Specific Language for Performance Evaluation of Medical Imaging Systems. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 80-93, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{vandenberg_et_al:OASIcs.MCPS.2014.80,
author = {van den Berg, Freek and Remke, Anne and Haverkort, Boudewijn R.},
title = {{A Domain Specific Language for Performance Evaluation of Medical Imaging Systems}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {80--93},
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.80},
URN = {urn:nbn:de:0030-drops-45257},
doi = {10.4230/OASIcs.MCPS.2014.80},
annote = {Keywords: Domain Specific Language, Performance Evaluation, Simulation, Model Checking, Medical Systems}
}
Document
A Safety Argument Strategy for PCA Closed-Loop Systems: A Preliminary Proposal
Abstract
The emerging network-enabled medical devices impose new challenges for the safety assurance of medical cyber-physical systems (MCPS). In this paper, we present a case study of building a high-level safety argument for a patient-controlled analgesia (PCA) closed-loop system, with the purpose of exploring potential methodologies for assuring the safety of MCPS.
Cite as
Lu Feng, Andrew L. King, Sanjian Chen, Anaheed Ayoub, Junkil Park, Nicola Bezzo, Oleg Sokolsky, and Insup Lee. A Safety Argument Strategy for PCA Closed-Loop Systems: A Preliminary Proposal. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 94-99, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{feng_et_al:OASIcs.MCPS.2014.94,
author = {Feng, Lu and King, Andrew L. and Chen, Sanjian and Ayoub, Anaheed and Park, Junkil and Bezzo, Nicola and Sokolsky, Oleg and Lee, Insup},
title = {{A Safety Argument Strategy for PCA Closed-Loop Systems: A Preliminary Proposal}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {94--99},
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.94},
URN = {urn:nbn:de:0030-drops-45263},
doi = {10.4230/OASIcs.MCPS.2014.94},
annote = {Keywords: Medical Cyber-Physical Systems, Safety Argument, Assurance Cases, Patient-Controlled Analgesia Infusion Pump, Closed-Loop Systems}
}
Document
Evaluating On-line Model Checking in UPPAAL-SMC using a Laser Tracheotomy Case Study
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}
}
Document
Integrating Safety Assessment into the Design of Healthcare Service-Oriented Architectures
Abstract
Most healthcare organisations are service-oriented, fundamentally centred on critical services provided by medical and nursing staff. Increasingly, these human-centric services rely on software-intensive systems, i.e. medical devices and health informatics, for improving different aspects of healthcare, e.g. enhancing efficiency through automation and patient safety through smart alarm systems. However, many healthcare services are categorised as high risk and as such it is vital to analyse the ways in which the software-based systems can contribute to unintentional harm and potentially compromise patient safety. This paper proposes an approach to modelling and analysing Service-Oriented Architectures (SOAs) used in healthcare, with emphasis on identifying and classifying potential hazardous behaviour. The paper also considers how the safety case for these SOAs can be developed in a modular manner. The approach is illustrated through a case study based on three services: ambulance, electronic health records and childbirth services.
Cite as
Ibrahim Habli, Abdulaziz Al-Humam, Tim Kelly, and Leila Fahel. Integrating Safety Assessment into the Design of Healthcare Service-Oriented Architectures. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 113-123, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{habli_et_al:OASIcs.MCPS.2014.113,
author = {Habli, Ibrahim and Al-Humam, Abdulaziz and Kelly, Tim and Fahel, Leila},
title = {{Integrating Safety Assessment into the Design of Healthcare Service-Oriented Architectures}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {113--123},
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.113},
URN = {urn:nbn:de:0030-drops-45289},
doi = {10.4230/OASIcs.MCPS.2014.113},
annote = {Keywords: Healthcare, Safety, Assurance, Service-Oriented Architecture}
}
Document
Design Pillars for Medical Cyber-Physical System Middleware
Abstract
Our goal is to improve patient outcomes and safety through medical device interoperability. To achieve this, it is not enough to build a technically perfect system. We present here our work toward the validation of middleware for use in interoperable medical cyber-physical systems. This includes clinical requirements, together with our methodology for collecting them, and a set of eighteen `design pillars' that document the non-functional requirements and design goals that we believe are necessary to build a successful interoperable medical device system. We discuss how the clinical requirements and design pillars are involved in the selection of a middleware for our OpenICE implementation.
Cite as
David Arney, Jeff Plourde, Rick Schrenker, Pratyusha Mattegunta, Susan F. Whitehead, and Julian M. Goldman. Design Pillars for Medical Cyber-Physical System Middleware. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 124-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{arney_et_al:OASIcs.MCPS.2014.124,
author = {Arney, David and Plourde, Jeff and Schrenker, Rick and Mattegunta, Pratyusha and Whitehead, Susan F. and Goldman, Julian M.},
title = {{Design Pillars for Medical Cyber-Physical System Middleware}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {124--132},
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.124},
URN = {urn:nbn:de:0030-drops-45294},
doi = {10.4230/OASIcs.MCPS.2014.124},
annote = {Keywords: Medical Device Interoperability, Clinical Requirements, Design Pillars, Requirements Elicitation, Validation}
}
Document
OR.NET - Approaches for Risk Analysis and Measures of Dynamically Interconnected Medical Devices
Abstract
Nowadays, it lacks an open, standardized and dynamic interconnection of medical devices. All existing combinations of medical devices consist of isolated solutions with proprietary interfaces, as no common standards for networking and the exchange of data of medical devices exist. This situation leads to confusing operating rooms and inefficient operations. Thus, new strategies need to be developed for the authorization of dynamically interconnected medical devices. Primarily, those concern of an acquisition and methodical adaption of new requirements and risks resulting from this way of interconnection.
The approach is to develop a method for a risk analysis for interconnected medical devices, which is structured modular and consists of a risk assessment of the standalone device and a risk analysis for the interconnection considering the risks involved in the transfer of functions. When interconnecting the medical devices the risk analysis of each of the devices is taken and they are compared by a gap analysis. Through this strategy it will be possible to realize a standard-compliant dynamic interconnection of medical products, which would be advantageous both for clinic operators and producers. This paper presents the current situation of the authorization of combined medical devices and proposes a strategy for the risk management of dynamically interconnected medical devices as a substantial part of the authorization.
Cite as
Franziska Kühn, Martin Leucker, and Alexander Mildner. OR.NET - Approaches for Risk Analysis and Measures of Dynamically Interconnected Medical Devices. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 133-136, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{kuhn_et_al:OASIcs.MCPS.2014.133,
author = {K\"{u}hn, Franziska and Leucker, Martin and Mildner, Alexander},
title = {{OR.NET - Approaches for Risk Analysis and Measures of Dynamically Interconnected Medical Devices}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {133--136},
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.133},
URN = {urn:nbn:de:0030-drops-45300},
doi = {10.4230/OASIcs.MCPS.2014.133},
annote = {Keywords: Modular Risk Analysis, Medical Device Interconnection, OR.NET, Development Method}
}
Document
Automated Verification of Quantitative Properties of Cardiac Pacemaker Software
Abstract
This poster paper reports on a model-based framework for software quality assurance for cardiac pacemakers developed in Simulink and described in [Chen/Diciolla/Kwiatkowska/Mereacre - Information&Computation, 2013]. A novel hybrid heart model is proposed that is suitable for quantitative verification of pacemakers.
The heart model is formulated at the level of cardiac cells, can be adapted to patient data, and incorporates stochasticity. We validate the model by demonstrating that its composition with a pacemaker model can be used to check safety properties by means of approximate probabilistic verification.
Cite as
Marta Kwiatkowska and Alexandru Mereacre. Automated Verification of Quantitative Properties of Cardiac Pacemaker Software. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 137-140, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{kwiatkowska_et_al:OASIcs.MCPS.2014.137,
author = {Kwiatkowska, Marta and Mereacre, Alexandru},
title = {{Automated Verification of Quantitative Properties of Cardiac Pacemaker Software}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {137--140},
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.137},
URN = {urn:nbn:de:0030-drops-45317},
doi = {10.4230/OASIcs.MCPS.2014.137},
annote = {Keywords: Pacemakers, Verification, Simulink}
}
Document
Potential Advantages of Applying Assurance Case Modeling to Requirements Engineering for Interoperable Medical Device Systems
Abstract
This poster describes our initial work in applying assurance cases to the requirements engineering processes necessary in building interoperable medical device systems.
Cite as
Rick Schrenker, Jeff Plourde, Diego Alonso, David Arney, and Julian M. Goldman. Potential Advantages of Applying Assurance Case Modeling to Requirements Engineering for Interoperable Medical Device Systems. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 141-142, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{schrenker_et_al:OASIcs.MCPS.2014.141,
author = {Schrenker, Rick and Plourde, Jeff and Alonso, Diego and Arney, David and Goldman, Julian M.},
title = {{Potential Advantages of Applying Assurance Case Modeling to Requirements Engineering for Interoperable Medical Device Systems}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {141--142},
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.141},
URN = {urn:nbn:de:0030-drops-45326},
doi = {10.4230/OASIcs.MCPS.2014.141},
annote = {Keywords: Assurance Case, Goal Structured Notation, Requirements Engineering, Interoperability, Medical Device}
}
Document
Process-Oriented Analysis for Medical Devices
Abstract
Medical Cyber Physical Systems are widely used in modern healthcare environments. Such systems are considered life-critical due to the severity of consequences that faults may cause. Effective methods, techniques and tools for modeling and analyzing medical critical systems are of major importance for ensuring system reliability and patient safety.
This work is looking at issues concerning different types of medical industry needs including safety analysis, testing, conformance checking, performance analysis and optimization. We explore the possibility of addressing these issues by exploiting information recorded in logs generated by medical devices during execution. Process-oriented analysis of logs is known as process mining, a novel field that has gained considerable interest in
several contexts in the last decade.
Process mining techniques will be applied to an industrial use case provided by Fresenius, a manufacturer of medical devices, for analyzing process logs generated by an infusion pump.
Cite as
Vasiliki Sfyrla, Josep Carmona, and Pascal Henck. Process-Oriented Analysis for Medical Devices. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 143-146, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{sfyrla_et_al:OASIcs.MCPS.2014.143,
author = {Sfyrla, Vasiliki and Carmona, Josep and Henck, Pascal},
title = {{Process-Oriented Analysis for Medical Devices}},
booktitle = {5th Workshop on Medical Cyber-Physical Systems},
pages = {143--146},
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.143},
URN = {urn:nbn:de:0030-drops-45335},
doi = {10.4230/OASIcs.MCPS.2014.143},
annote = {Keywords: Process Logs, Process Mining, Discovery, Formal Analysis, Infusion Pump}
}