Inevitably, it becomes more and more important to verify that the systems surrounding us have certain properties. This is indeed unavoidable for safety-critical systems such as power plants and intensive-care units. We refer to the term system in a broad sense: it may be man-made (e.g. a computer system) or natural (e.g. a patient in an intensive-care unit). Whereas in Model Checking it is assumed that one has complete knowledge about the functioning of the system, we consider an open-world scenario and assume that we can only observe the behaviour of the actual running system by sensors. Such an abstract sensor could sense e.g. the blood pressure of a patient or the air traffic observed by radar. Then the observed data are preprocessed appropriately and stored in a fact base. Based on the data available in the fact base, situation-awareness tools are supposed to help the user to detect certain situations that require intervention by an expert. Such situations could be that the heart-rate of a patient is rather high while the blood pressure is low, or that a collision of two aeroplanes is about to happen. Moreover, the information in the fact base can be used by monitors to verify that the system has certain properties. It is not realistic, however, to assume that the sensors always yield a complete description of the current state of the observed system. Thus, it makes sense to assume that information that is not present in the fact base is unknown rather than false. Moreover, very often one has some knowledge about the functioning of the system. This background knowledge can be used to draw conclusions about the possible future behaviour of the system. Employing description logics (DLs) is one way to deal with these requirements. In this thesis, we tackle the sketched problem in three different contexts: (i) runtime verification using a temporalised DL, (ii) temporalised query entailment, and (iii) verification in DL-based action formalisms.

Die fraktionierte stereotaktisch geführte Radiotherapie stellt eine Möglichkeit der Behandlung intrakranieller Tumoren dar, bei denen eine chirurgische Resektion nicht oder nicht vollständig möglich ist. Ziel dieser Arbeit war der Vergleich der Dosisverteilung von Bestrahlungsplänen, die mittels fluenzmodulierter (IMRT) und 3D konformaler stereotaktisch geführter Bestrahlungstechnik (conformal beam) für Hypophysenadenome und petroclivale Meningeome erstellt wurden. Auf Basis des CT-Datensatzes eines Alderson-Phantoms erfolgten zunächst die systematische Untersuchung der IMRT Eingabeparameter und die Definition von Dosis-Volumen-Constraints für beide Tumorentitäten. Im Anschluss wurden die gewonnenen Erkenntnisse bei der fluenzmodulierten Bestrahlungsplanung von 10 realen Patienten, 5 je Tumorentität, angewendet. Zusätzlich wurde für jeden dieser Patienten ein 3D konformaler Bestrahlungsplan erstellt. Die Evaluation der Bestrahlungspläne erfolgte durch verschiedene quantitativer Parameter unter Einbeziehung der subjektiven Beurteilung der Dosisverteilung. Bei beiden Tumorentitäten lieferte in je 4 von 5 Fällen die IMRT einen Vorteil gegenüber der conformal beam Bestrahlung, der vor allem auf der besseren Erfassung, Dosishomogenität und höheren Median-Dosis im bestrahlten Zielvolumen (PTV) beruhte. Komplex geformte Zielvolumina profitierten dabei besonders von der Fluenzmodulation. Dem stand jedoch in einigen Fälle eine stärke Belastung der Risikoorgane (OAR) mit einer höheren Dosis und die generell höhere Anzahl notwendiger Monitoreinheiten gegenüber. Zuletzt wurde auf Basis von MatLAB eine Software entwickelt, welche die Verifikation von stereotaktisch geführten IMRT-Bestrahlungen und die Analyse von Winston-Lutz-Tests ermöglicht.

Golog is a powerful programming language for logic-based agents. The primitives of the language are actions whose preconditions and effects are defined in a Situation Calculus action theory using first-order logic. To describe possible courses of actions the programmer can freely combine imperative control structures with constructs for non-deterministic choice, leaving it to the system to resolve the non-determinism in a suitable manner. Golog has been successfully used for high-level decision making in the area of cognitive robotics. Obviously, it is important to verify certain properties of a Golog program before executing it on a physical robot. However, due to the high expressiveness of the language the verification problem is in general undecidable. In this thesis, we study the verification problem for Golog programs over actions defined in action languages based on Description Logics and explore the boundary between decidable and undecidable fragments.

Diese Arbeit untersucht den Einfluss von Daten auf das Verhalten und die Korrektheit eines verteilten Systems. Ein verteiltes System besteht aus mehreren Services. Ein Service ist eine selbständige, plattformunabhängige Einheit, die anderen Services eine bestimmte Funktionalität über eine wohldefinierte Schnittstelle zur Verfügung stellt. In dieser Arbeit betrachten wir die Interaktion von jeweils genau zwei Services miteinander. Zwei Services, die erfolgreich miteinander zusammenarbeiten können, nennen wir Partner. Ein Service heißt bedienbar, wenn er mindestens einen Partner hat. Ziel der Arbeit ist es, zu untersuchen, wann zwei Services Partner sind, und für einen Service zu entscheiden, ob dieser bedienbar ist. Aufgrund der Daten kann der Zustandsraum eines Service sehr groß oder sogar unendlich groß werden. Wir untersuchen zwei Klassen von Services mit unendlich vielen Zuständen. Für diese Klassen stellen wir Algorithmen vor, welche zu einem gegebenen Service einen Partner synthetisieren, falls ein solcher existiert. Auf diese Weise entscheiden wir konstruktiv die Bedienbarkeit eines Service. Weiterhin stellen wir Transformationsregeln für Partner vor und untersuchen, wie viel Speicherplatz ein Partner eines Services mindestens benötigt. / This thesis studies the influence of data on the behavior and the correctness of a distributed system. A distributed system consists of several services. A service is a self-contained, platform-independent entity which provides a certain functionality to other services via a well-defined interface.In this thesis, we consider the interaction of exactly two services. Two services that can successfully cooperate with each other are called partners. We call a service controllable, if the service has at least one partner. The goal of this thesis is to study the conditions for which two services are partners and to decide whether a given service is controllable. Due to the data, the state space of a service may be very large or even infinite. We investigate two classes of services with infinitely many states. For these classes, we present algorithms that synthesize a partner of a service, if it exists. This allows us to decide the controllability of a service constructively. Furthermore, we present transformation rules for partners and investigate the minimum amount of memory that a partner of a service needs.

Dienstorientierte Architekturen (SOA = Service Oriented Architecture) dienen dem Aufbau von lose miteinander verbundenen, verteilten Systemen, deren Komponenten eine minimale gemeinsame Systemsicht haben. Die wichtigsten Bausteine der SOA sind Dienste. Dienste sind selbstbeschreibende, eigenständige, plattform-unabhängige und frei verfügbare Komponenten, die über das Netzwerk interagieren. Das Hauptziel der SOA ist die transparente, flexible und dynamische Interaktion von Diensten und deren Benutzern innerhalb mehrerer zusammenhängender Domänen. Während die nativen Fähigkeiten von dienstorientierten Architekturen, wie Beschreibung, Entdeckung, Kommunikation und Bindung, bereits gut erfasst und standardisiert worden sind, ist das Problem der Dienstkomposition bisher noch nicht zufriedenstellend gelöst worden. Diese Dissertation hinterfragt die Grundvoraussetzung der SOA, die darin besteht, dass lediglich die Grundfunktionsweise von Diensten offen gelegt werden sollte, und demonstriert, dass auf der Grundlage einer semantischen Dienstbeschreibung (einschließlich funktionaler und nichtfunktionaler Eigenschaften) eine praktikable Lösung zur Dienstkomposition entwickelt werden kann (komponierbare Dienstarchitektur). Diese Lösung erfordert 1) erweiterte deskriptive Fähigkeiten und Suchmöglichkeiten durch die Entwicklung einer vertragsbasierten Beschreibungssprache einschließlich nichtfunktionaler Eigenschaften wie Sicherheit, Verlässlichkeit und Rechtzeitigkeit; 2) das Feststellen der Kompositionskorrektheit durch die Modellierung von Diensten als abstrakte Maschinen und die Entwicklung einer formalen Kompositionssprache und 3) automatische Dienstkomposition, indem Suchalgorithmen für die automatisierte und dynamische Selektion von Kompositionspartnern entwickelt werden. Abschließend wird der Prototyp eines Kompositionsservers für Web Services einschließlich Design und Implementierung beschrieben, um die Realisierbarkeit der vorgeschlagenen Architektur aufzuzeigen. / Service-oriented architecture (SOA) is focused on building loosely coupled distributed systems with minimal shared understanding among system components. The main building blocks in SOA are services. Services are self-descriptive, self-contained, platform-independent and openly-available components that interact over the network. The main goal of SOA is transparent, flexible and dynamic interaction of services and their clients over multiple interconnected domains. While native capabilities of service-oriented architectures, such as description, discovery, communication and binding, have been well understood and standardized, the issue of service composition has not yet been satisfactorily solved. This dissertation challenges the SOA postulate that service should disclose only basic functional signature, and demonstrates that based on semantic service description, including functional and non-functional properties, a viable solution for service composition can be developed (composable service architecture), that supports: 1) Extended descriptive and search capabilities by developing contract-based description language including non-functional properties such as security, dependability, timeliness; 2) Verification of composition correctness by modeling services as abstract machines and developing a formal composition language, and 3) Automatic service composition by treating automated and dynamic selection of composition partners as a search problem and developing search algorithms for that purpose. Finally, in order to show the viability of the proposed architectural solution, a prototype of Web Services composition server is described including design and implementation.

No description available.

Um Entwurf und Verifikation komplizierter verteilter Algorithmen leichter und verständlicher zu machen, wird oft eine Verfeinerungsmethode verwendet. Dabei wird ein einfacher Algorithmus, der gewünschte Eigenschaften erfüllt, schrittweise zu einem komplizierten Algorithmus verfeinert. In jedem Schritt sollen die gewünschten Eigenschaften erhalten bleiben. Für nachrichtenbasierte verteilte Algorithmen haben wir eine neue Verfeinerungsmethmode entwickelt. Wir beginnen mit einem Anfangsalgorithmus, der Aktionen enthält, die gemeinsame Aufgaben mehrerer Agenten beschreiben. In jedem Schritt verfeinern wir eine dieser Aktionen zu einem Netz, das nur solche Aktionen enthält, die die Aufgaben einzelner Agenten beschreiben. Jeder Schritt ist also eine Verteilung einer unverteilten Aktion. Die Analyse solcher Verfeinerungsschritte wird mit Hilfe eines neuen Verfeinerungsbegriffs - der verteilenden Verfeinerung - durchgeführt. Entscheidend dabei ist das Erhaltenbleiben der Halbordnungen des zu verfeinernden Algorithmus. Dies ist durch Kausalitäten der Aktionen der Agenten im lokalen Verfeinerungsnetz zu erreichen. Die Kausalitäten im lokalen Verfeinerungsnetz lassen sich einerseits beim Entwurf direkt durch Nachrichtenaustausch realisieren. Andererseits kann man bei der Verifikation die Gültigkeit einer Kausalität im lokalen Verfeinerungsnetz direkt vom Netz ablesen. Daher ist diese Methode leicht zu verwenden. Die Anwendung der Methode wird in der Arbeit an verschiedenen nicht trivialen Beispielen demonstriert. / In order to make design and verification of complicated distributed algorithms easier and more understandable, a refinement method is often used. A simple algorithm, which fulfills desired properties, is refined stepwise to a complicated algorithm. In each step the desired properties are preserved. For messages-based distributed algorithms we have developed a new refinement method. We begin with an initial algorithm, which contains actions, which describe common tasks of several agents. In each step we refine one of these actions to a net, which contains only such actions, which describe the tasks of individual agents. Thus, each step is a distribution of an undistributed action. The analysis of such refinement steps is accomplished with the help of a new refinement notation - the distributing refinement. Preservation of the partial order of the refined algorithm is important. This can be achieved by causalities of the actions of the agents in the local refinement net. Causalities in the local refinement net can be realized on the one hand at design directly by messages passing. On the other hand, at verification one can read the validity of causality in the local refinement net directly from the net. Therefore, this method is easy to use. The application of the method is demonstrated by several nontrivial examples in this thesis.

The proper composition of independently developed components of an embedded real- time system is complicated due to the fact that besides the functional behavior also the non-functional properties and in particular the timing have to be compatible. Nowadays related compatibility problems have to be addressed in a cumbersome integration and configuration phase at the end of the development process, that in the worst case may fail. Therefore, a number of formal approaches have been developed, which try to guide the upfront decomposition of the embedded real-time system into components such that integration problems related to timing properties can be excluded and that suitable configurations can be found. However, the proposed solutions require a number of strong assumptions that can be hardly fulfilled or the required analysis does not scale well. In this paper, we present an approach based on timed automata that can provide the required guarantees for the later integration without strong assumptions, which are difficult to match in practice. The approach provides a modular reasoning scheme that permits to establish the required guarantees for the integration employing only local checks, which therefore also scales. It is also possible to determine potential configuration settings by means of timed game synthesis. / Die korrekte Komposition individuell entwickelter Komponenten von eingebetteten Realzeitsystemen ist eine Herausforderung, da neben funktionalen Eigenschaften auch nicht funktionale Eigenschaften berücksichtigt werden müssen. Ein Beispiel hierfür ist die Kompatibilität von Realzeiteigenschaften, welche eine entscheidende Rolle in eingebetteten Systemen spielen. Heutzutage wird die Kompatibilität derartiger Eigenschaften in einer aufwändigen Integrations- und Konfigurationstests am Ende des Entwicklungsprozesses geprüft, wobei diese Tests im schlechtesten Fall fehlschlagen. Aus diesem Grund wurde eine Zahl an formalen Verfahren Entwickelt, welche eine frühzeitige Analyse von Realzeiteigenschaften von Komponenten erlauben, sodass Inkompatibilitäten von Realzeiteigenschaften in späteren Phasen ausgeschlossen werden können. Existierenden Verfahren verlangen jedoch, dass eine Reihe von Bedingungen erfüllt sein muss, welche von realen Systemen nur schwer zu erfüllen sind, oder aber, die verwendeten Analyseverfahren skalieren nicht für größere Systeme. In dieser Arbeit wird ein Ansatz vorgestellt, welcher auf dem formalen Modell des Timed Automaton basiert und der keine Bedingungen verlangt, die von einem realen System nur schwer erfüllt werden können. Der in dieser Arbeit vorgestellte Ansatz enthält ein Framework, welches eine modulare Analyse erlaubt, bei der ausschließlich miteinender kommunizierende Komponenten paarweise überprüft werden müssen. Somit wird eine skalierbare Analyse von Realzeiteigenschaften ermöglicht, die keine Bedingungen verlangt, welche nur bedingt von realen Systemen erfüllt werden können.

With the rise of electronic integration between organizations, the need for a precise specification of interaction behavior increases. Information systems, replacing interaction previously carried out by humans via phone, faxes and emails, require a precise specification for handling all possible situations. Such interaction behavior is described in process choreographies. Choreographies enumerate the roles involved, the allowed interactions, the message contents and the behavioral dependencies between interactions. Choreographies serve as interaction contract and are the starting point for adapting existing business processes and systems or for implementing new software components. As a thorough analysis and comparison of choreography modeling languages is missing in the literature, this thesis introduces a requirements framework for choreography languages and uses it for comparing current choreography languages. Language proposals for overcoming the limitations are given for choreography modeling on the conceptual and on the technical level. Using an interconnection modeling style, behavioral dependencies are defined on a per-role basis and different roles are interconnected using message flow. This thesis reveals a number of modeling "anti-patterns" for interconnection modeling, motivating further investigations on choreography languages following the interaction modeling style. Here, interactions are seen as atomic building blocks and the behavioral dependencies between them are defined globally. Two novel language proposals are put forward for this modeling style which have already influenced industrial standardization initiatives. While avoiding many of the pitfalls of interconnection modeling, new anomalies can arise in interaction models. A choreography might not be realizable, i.e. there does not exist a set of interacting roles that collectively realize the specified behavior. This thesis investigates different dimensions of realizability. / Elektronische Integration zwischen Organisationen erfordert eine präzise Spezifikation des Interaktionsverhaltens: Informationssysteme, die Kommunikation per Telefon, Fax und Email ablösen, können nicht so flexibel und selbständig auf Ausnahmesituationen reagieren wie Menschen. Choreographien ermöglichen es, Interaktionsverhalten genau zu spezifizieren. Diese Modelle zählen die beteiligten Rollen, die erlaubten Interaktionen, Nachrichteninhalte und Verhaltensabhängigkeiten auf und dienen somit als Interaktionsvertrag zwischen den Organisationen. Auch als Ausgangspunkt für eine Anpassung existierender Prozesse und Systeme sowie für die Implementierung neuer Softwarekomponenten finden Choreographien Anwendung. Da ein Vergleich von Choreographiemodellierungssprachen in der Literatur bislang fehlt, präsentiert diese Arbeit einen Anforderungskatalog, der als Basis für eine Evaluierung existierender Sprachen angewandt wird. Im Kern führt diese Arbeit Spracherweiterungen ein, um die Schwächen existierender Sprachen zu überwinden. Die vorgestellten Erweiterungen adressieren dabei Modellierung auf konzeptioneller und auf technischer Ebene. Beim Verlinkungsmodellierungsstil werden Verhaltensabhängigkeiten innerhalb der beteiligten Rollen spezifiziert und das Interaktionsverhalten entsteht durch eine Verlinkung der Kommunikationsaktivitäten. Diese Arbeit stellt einige "Anti-Pattern" für die Verlinkungsmodellierung vor, welche wiederum Untersuchungen bzgl. Choreographiesprachen des Interaktionsmodellierungsstils motivieren. Hier werden Interaktionen als atomare Blöcke verstanden und Verhaltensabhängigkeiten werden global definiert. Diese Arbeit führt zwei neue Choreographiesprachen dieses zweiten Modellierungsstils ein, welche bereits in industrielle Standardisierungsinitiativen eingeflossen sind. Während auf der einen Seite zahlreiche Fallstricke der Verlinkungsmodellierung umgangen werden, können in Interaktionsmodellen allerdings neue Anomalien entstehen. Eine Choreographie kann z.B. "unrealisierbar" sein, d.h. es ist nicht möglich interagierende Rollen zu finden, die zusammen genommen das spezifizierte Verhalten abbilden. Dieses Phänomen wird in dieser Arbeit über verschiedene Dimensionen von Realisierbarkeit untersucht.

Systems of Systems (SoS) have received a lot of attention recently. In this thesis we will focus on SoS that are built atop the techniques of Service-Oriented Architectures and thus combine the benefits and challenges of both paradigms. For this thesis we will understand SoS as ensembles of single autonomous systems that are integrated to a larger system, the SoS. The interesting fact about these systems is that the previously isolated systems are still maintained, improved and developed on their own. Structural dynamics is an issue in SoS, as at every point in time systems can join and leave the ensemble. This and the fact that the cooperation among the constituent systems is not necessarily observable means that we will consider these systems as open systems. Of course, the system has a clear boundary at each point in time, but this can only be identified by halting the complete SoS. However, halting a system of that size is practically impossible. Often SoS are combinations of software systems and physical systems. Hence a failure in the software system can have a serious physical impact what makes an SoS of this kind easily a safety-critical system. The contribution of this thesis is a modelling approach that extends OMG's SoaML and basically relies on collaborations and roles as an abstraction layer above the components. This will allow us to describe SoS at an architectural level. We will also give a formal semantics for our modelling approach which employs hybrid graph-transformation systems. The modelling approach is accompanied by a modular verification scheme that will be able to cope with the complexity constraints implied by the SoS' structural dynamics and size. Building such autonomous systems as SoS without evolution at the architectural level --- i. e. adding and removing of components and services --- is inadequate. Therefore our approach directly supports the modelling and verification of evolution. / Systems of Systems (SoS) sind ein seit längerem bekanntes Konzept, das jedoch in letzter Zeit vermehrt Aufmerksamkeit erhielt. Das Hauptaugenmerk dieser Arbeit wird auf SoS liegen, die mit Hilfe von Techniken aus Service-Orientierten Architekturen erstellt werden. Somit vereinen die hier betrachteten SoS die Vorteile und Herausforderungen beider Paradigmen. SoS können definiert werden als Zusammenschlüsse einzelner, autonomer Systeme, die zu einem größeren System integriert werden. In diesem Zusammenhang interessant ist, dass die ehemals isolierten Systeme nach wie vor isoliert voneinander weiterentwickelt und gewartet werden. Desweiteren kommt der Strukturdynamik innerhalb des SoS eine beachtliche Bedeutung zu, da jederzeit Systeme dem SoS beitreten und es verlassen können. Zusammen mit der Tatsache, dass die Kooperationen zwischen den konstituierenden Systemen nicht immer beobachtbar sind, führt dies dazu, dass wir diese Systeme als offene Systeme bezeichnen. Wobei das System natürlich jederzeit eine klar definierte Grenze besitzt, diese aber nur durch ein Anhalten des Systems zu bestimmen ist. Dies jedoch ist, von einer praktischen Perspektive aus betrachtet, unmöglich. Häufig stellen SoS eine Kombination aus Softwaresystemen und pyhsikalischen Systemen dar mit der Folge, dass ein Fehler in der Software eine SoS schnell eine immense physikalische Wirkung entwickeln kann. Von daher fallen SoS leicht in die Klasse der sicherheitskritischen Systeme. In dieser Arbeit werden wir einen Modellierungsansatz vorstellen, der die Sprache SoaML der OMG erweitert. Die grundlegenden Konzepte dieses Ansatzes sind die Modellierung mit Kollaborationen und Rollen als Abstraktionsebene über Komponenten. Der vorgestellte Ansatz erlaubt es uns SoS auf einer architekturellen Ebene zu betrachten. Die formale Semantik unseres Modellierungsansatzes ist durch hybride Graphtransformationssysteme gegeben. Abgestimmt auf die Modellierung werden wir ebenfalls ein Verfahren zu Verifikation von SoS vorstellen, welches trotz der inhärenten Komplexität von SoS, diese zu verifizieren. Die Modellierung und Verifikation von Evolution wird von unserem Ansatz direkt unterstützt.