Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-4048
Main Title: Automated composition of timed services in medical applications
Translated Title: Automatisierte Komposition zeitbehafteter Services in medizinischen Anwendungen
Author(s): Stöhr, Daniel
Advisor(s): Glesner, Sabine
Referee(s): Glesner, Sabine
Weske, Mathias
Nestmann, Uwe
Granting Institution: Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik
Type: Doctoral Thesis
Language: English
Language Code: en
Abstract: Die Entwicklung von Controller-Programmen, die verteilte Komponenten in sicherheits- und zeitkritischen Umgebungen steuern, ist eine sehr schwierige und zeitaufwändige Aufgabe. Einerseits soll die Korrektheit sichergestellt werden, was langwierige Phasen der Qualitätssicherung erfordert. Andererseits soll die Entwicklungszeit kurz sein, um die Kosten niedrig zu halten und eine geringe Produkteinführungszeit zu erzielen. In dieser Dissertation greifen wir dieses Problem auf, um die Lücke zwischen kurzer Entwicklungszeit und qualitativ korrekten Entwicklungsergebnissen, insbesondere unter sicherheits- und zeitkritischen Anforderungen, zu schließen. Wir gehen unser Problem mit Mitteln der automatisierten Service-Komposition an. Im Kontext der Service-Orientierung kann der Controller als ein Orchestrator betrachtet werden, der eine Service-Komposition koordiniert. Wir stellen einen Ansatz vor, der in der Lage ist, automatisiert Orchestrator-Modelle für eine Eingabemenge beteiligter Services zu generieren, die als Timed I/O Automata (TIOA) modelliert werden. Die Kompositionsanforderungen werden in der Temporallogik Timed CTL (TCTL) ausgedrückt. Der generierte Orchestrator ist selbst ein TIOA, der die ein- und ausgehenden Signale der anderen Automaten anspricht. Die Algorithmen, die den Kompositionsprozess durchführen, haben wir basierend auf nicht-zeitbehafteten Planungsalgorithmen und zeitbehaftetem Model Checking entwickelt. Unser Ansatz beherrscht Service-Verhalten und Kompositionsanforderungen, die komplex und zeitbehaftet sind, insbesondere beliebig verschachtelte und verkettete TCTL-Formeln. Damit geht unsere Arbeit über die Möglichkeiten früher Ansätze der Automatisierten Service-Komposition und Planungstheorie hinaus. Diese erlauben lediglich eine sehr eingeschränkte Untermenge von TCTL oder weniger ausdrucksmächtige Sprachen. Jedoch benötigen wir die zusätzliche Ausdrucksstärke in vielen praktischen Anwendungen. Ein Beispiel sind medizinische Systeme, in denen Geräte-Services Aktionen wiederholt in bestimmten zeitlichen Abständen ausführen sollen. Unsere Arbeit leistet folgende Beiträge zum aktuellen Forschungsstand. Wir stellen ein formal fundiertes Framework zur automatisierten Komposition zeitbehafteter Services zur Verfügung, basierend auf neuen Planungsalgorithmen zur Realisierung des Kompositionsprozesses. Darüber hinaus stellen wir einen Algorithmus zur Konstruktion von Orchestrator-Modellen aus Plänen zur Verfügung. Wir haben unsere Algorithmen symbolisch formuliert, sodass wir von effizienten Abstraktionstechniken aus dem Bereich des symbolischen Model Checking profitieren können. Abschließend haben wir einen Prototyp unseres Frameworks implementiert und diesen mit zwei Fallstudien aus der medizinischen Domäne, einer Schmerzmittelpumpe und einem Behandlungsprozess für Schlaganfallpatienten der Charité-Universitätsklinik, evaluiert.
The development of controller programs that coordinate distributed components in safety and time-critical environments is a very complex task. On the one hand, correctness has to be assured, which results in extensive phases of quality assurance. On the other hand, development time has to be short to achieve low development costs and a short time-to-market. In this thesis, we address the problem of closing the gap between a short development time and results that are correct w.r.t. functional and non-functional, especially time-related requirements. We tackle our problem by means of automated service composition. In the context of service-oriented computing, a controller is an orchestrator that coordinates a service composition. We present an approach that enables us to automatically generate orchestrator models for a given set of timed services, described as Timed I/O Automata (TIOA). The composition requirements are expressed in the temporal logic Timed CTL (TCTL). The generated orchestrator is a TIOA handling the input and output actions of the individual automata. For performing the composition process, we present algorithms based on ideas from untimed planning theory and timed model checking. Our approach copes with complex, time-related service behavior and specifications, especially with TCTL formulas that are arbitrarily nested and chained. This improves previous approaches from both automated service composition and planning theory. Existing approaches only offer a very restricted subset of TCTL or less expressive languages. However, the additional expressiveness we offer is required in many practical applications. An example are medical systems, where device services have to repeat actions infinitely often in given time steps. Our main contributions are: We provide an automated, formally founded composition framework for timed services. The core of our framework consists of new planning algorithms realizing the composition process. Moreover, we provide an algorithm for constructing controller models out of generated plans. We formulate our algorithms symbolically to benefit from efficient abstraction techniques of symbolic model checking. Finally, we have implemented a prototype of our framework and evaluated it with two case studies from the medical domain: a PCA pump and a treatment process for stroke patients at the Charité University Hospital.
URI: urn:nbn:de:kobv:83-opus4-51172
http://depositonce.tu-berlin.de/handle/11303/4345
http://dx.doi.org/10.14279/depositonce-4048
Exam Date: 3-Apr-2014
Issue Date: 20-May-2014
Date Available: 20-May-2014
DDC Class: 000 Informatik, Informationswissenschaft, allgemeine Werke
Subject(s): Automatisierte Service-Komposition
Controller-Synthese
TCTL
Temporales Planen
Zeitbehaftete Automaten
Automated service composition
Controller synthesis
TCTL
Temporal planning
Timed automata
Usage rights: Terms of German Copyright Law
Appears in Collections:Technische Universität Berlin » Fakultäten & Zentralinstitute » Fakultät 4 Elektrotechnik und Informatik » Institut für Softwaretechnik und Theoretische Informatik » Publications

Files in This Item:
File Description SizeFormat 
stoehr_daniel.pdf5.38 MBAdobe PDFThumbnail
View/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.