Im Rahmen dieser Arbeit werden die Nebenläufigkeit, Konsistenz und Latenz in asynchronen Interaktiven Echtzeitsystemen durch die Techniken des Profilings und des Model Checkings untersucht. Zu Beginn wird erläutert, warum das asynchrone Modell das vielversprechendste für die Nebenläufigkeit in einem Interaktiven Echtzeitsystem ist. Hierzu wird ein Vergleich zu anderen Modellen gezogen. Darüber hinaus wird ein detaillierter Vergleich von Synchronisationstechnologien, welche die Grundlage für Konsistenz schaffen, durchgeführt. Auf der Grundlage dieser beiden Vergleiche und der Betrachtung anderer Systeme wird ein Synchronisationskonzept entwickelt. Auf dieser Basis wird die Nebenläufigkeit, Konsistenz und Latenz mit zwei Verfahren untersucht. Die erste Technik ist das Profiling, wobei einige neue Darstellungsformen von gemessenen Daten entwickelt werden. Diese neu entwickelten Darstellungsformen werden in der Implementierung eines Profilers verwendet. Als zweite Technik wird das Model Checking analysiert, welches bisher noch nicht im Kontext von Interaktiven Echtzeitsystemen verwendet wurde. Model Checking dient dazu, die Verhaltensweise eines Interaktiven Echtzeitsystems vorherzusagen. Diese Vorhersagen werden mit den Messungen aus dem Profiler verglichen. / In this thesis the concurrency, latency, and consistency of asynchronous Realtime Interactive Systems (RIS) are analyzed using profiling and model checking. At the beginning, it is described why the Asynchronous Model is the most promising model to increase concurrency in a RIS. Therefore, it is compared to several other models. Furthermore, synchronization techniques are compared, which are used to provide consistency in a concurrent application. Upon both results, a synchronization concept is created. Using this concept, the concurrency, latency, and consistency are analyzed using two techniques. The first technique is profiling. New visualizations are developed to visualize profiling data measured by profiling. The second technique is model checking. In this thesis, model checking is used for the first time in context of a RIS. Model checking is used to predict the behavior of a RIS. The predicition and the measurement from the profiling are compared.

Today, information and communication systems are ubiquitous and consist very often of several interacting and communicating components. One reason is the widespread use of multi-core processors and the increasing amount of concurrent software for the efficient usage of multi-core processors. Also, the dissemination of distributed emergent technologies like sensor networks or the internet of things is growing. Additionally, a lot of internet protocols are client-server architectures with clients which execute computations in parallel and servers that can handle requests of several clients in parallel. Systems which consist of several interacting and communicating components are often very complex and due to their complexity also prone to errors. Errors in systems can have dramatic consequenses, especially in safety-critical areas where human life can be endangered by incorrect system behavior. Hence, it is inevitable to have methods that ensure the proper functioning of such systems. This thesis aims on improving the verifiability of asynchronous concurrent systems using symbolic model checking based on Binary Decision Diagrams (BDDs). An asynchronous concurrent system is a system that consists of several components, from which only one component can execute a transition at a time. Model checking is a formal verification technique. For a given system description and a set of desired properties, the validity of the properties for the system is decided in model checking automatically by software tools called model checkers. The main problem of model checking is the state-space explosion problem. One approach to reduce this problem is the use of symbolic model checking. There, system states and transitions are not stored explicitely as in explicit model checking. Instead, in symbolic model checking sets of states and sets of transitions are stored and also manipulated together. The data structure which is used in this thesis to store those sets are BDDs. BDD-based symbolic model checking has already been used successful in industry for several times. Nevertheless, BDD-based symbolic model checking still suffers from the state-space explosion problem and further improvements are necessary to improve its applicability. Central operations in BDD-based symbolic model checking are the computation of successor and predecessor states of a given set of states. Those computations are called image computations. They are applied repeatedly in BDD-based symbolic model checking to decide the validity of properties for a given system description. Hence, their efficient execution is crucial for the memory and runtime requirements of a model checker. In an image computation a BDD for a set of transitions and a BDD for a set of states are combined to compute a set of successor or predecessor states. Often, also the size of the BDDs to represent the transition relation is critical for the successful use of model checking. To further improve the applicability of symbolic model checking, we present in this thesis new data structures to store the transition relation of asynchronous concurrent systems. Additionally, we present new image computation algorithms. Both can lead to large runtime and memory reductions for BDD-based symbolic model checking. Asynchronous concurrent systems often contain symmetries. A technique to exploit those symmetries to diminish the state-space explosion problem is symmetry reduction. In this thesis we also present a new efficient algorithm for symmetry reduction in BDD-based symbolic model checking. / In unserem Alltag kommen wir heute ständig mit Systemen der Informations- und Kommunikationstechnik in Kontakt. Diese bestehen häufig aus mehreren interagierenden und kommunizierenden Komponenten, wie zum Beispiel nebenläufige Software zur effizienten Nutzung von Mehrkernprozessoren oder Sensornetzwerke. Systeme, die aus mehreren interagierenden und kommunizierenden Komponenten bestehen sind häufig komplex und dadurch sehr fehleranfällig. Daher ist es wichtig zuverlässige Methoden, die helfen die korrekte Funktionsweise solcher Systeme sicherzustellen, zu besitzen. Im Rahmen dieser Doktorarbeit wurden neue Methoden zur Verbesserung der Verifizierbarkeit von asynchronen nebenläufigen Systemen durch Anwendung der symbolischen Modellprüfung mit binären Entscheidungsdiagrammen (BDDs) entwickelt. Ein asynchrones nebenläufiges System besteht aus mehreren Komponenten, von denen zu einem Zeitpunkt jeweils nur eine Komponente Transitionen ausführen kann. Die Modellprüfung ist eine Technik zur formalen Verifikation, bei der die Gültigkeit einer Menge von zu prüfenden Eigenschaften für eine gegebene Systembeschreibung automatisch durch Softwarewerkzeuge, die Modellprüfer genannt werden, entschieden wird. Das Hauptproblem der symbolischen Modellprüfung ist das Problem der Zustandsraumexplosion und es sind weitere Verbesserungen notwendig, um die symbolische Modellprüfung häufiger erfolgreich durchführen zu können. Bei der BDD-basierten symbolischen Modellprüfung werden Mengen von Systemzuständen und Mengen von Transitionen jeweils durch BDDs repräsentiert. Zentrale Operationen bei ihr sind die Berechnung von Nachfolger- und Vorgängerzuständen von gegebenen Zustandsmengen, welche Bildberechnungen genannt werden. Um die Gültigkeit von Eigenschaften für eine gegebene Systembeschreibung zu überprüfen, werden wiederholt Bildberechnungen durchgeführt. Daher ist ihre effiziente Berechnung entscheidend für eine geringe Laufzeit und einen niedrigen Speicherbedarf der Modellprüfung. In einer Bildberechnung werden ein BDD zur Repräsentation einer Menge von Transitionen und ein BDD für eine Menge von Zuständen kombiniert, um eine Menge von Nachfolger- oder Vorgängerzuständen zu berechnen. Oft ist auch die Größe von BDDs zur Repräsentation der Transitionsrelation von Systemen entscheidend für die erfolgreiche Anwendbarkeit der Modellprüfung. In der vorliegenden Arbeit werden neue Datenstrukturen zur Repräsentation der Transitionsrelation von asynchronen nebenläufigen Systemen bei der BDD-basierten symbolischen Modellprüfung vorgestellt. Zusätzlich werden neue Algorithmen zur Durchführung von Bildberechnungen präsentiert. Beides kann zu großen Reduktionen der Laufzeit und des Speicherbedarfs führen. Asynchrone nebenläufige Systeme besitzen häufig Symmetrien. Eine Technik zur Reduktion des Problems der Zustandsraumexplosion ist die Symmetriereduktion. In dieser Arbeit wird ebenfalls ein neuer effizienter Algorithmus zur Symmetriereduktion bei der symbolischen Modellprüfung mit BDDs aufgeführt.

Die Komplexität heutiger Geschäftsabläufe und die Menge der zu verwaltenden Daten stellen hohe Anforderungen an die Entwicklung und Wartung von Geschäftsanwendungen. Ihr Umfang entsteht unter anderem aus der Vielzahl von Modellentitäten und zugehörigen Nutzeroberflächen zur Bearbeitung und Analyse der Daten. Dieser Bericht präsentiert neuartige Konzepte und deren Umsetzung zur Vereinfachung der Entwicklung solcher umfangreichen Geschäftsanwendungen. Erstens: Wir schlagen vor, die Datenbank und die Laufzeitumgebung einer dynamischen objektorientierten Programmiersprache zu vereinen. Hierzu organisieren wir die Speicherstruktur von Objekten auf die Weise einer spaltenorientierten Hauptspeicherdatenbank und integrieren darauf aufbauend Transaktionen sowie eine deklarative Anfragesprache nahtlos in dieselbe Laufzeitumgebung. Somit können transaktionale und analytische Anfragen in derselben objektorientierten Hochsprache implementiert werden, und dennoch nah an den Daten ausgeführt werden. Zweitens: Wir beschreiben Programmiersprachkonstrukte, welche es erlauben, Nutzeroberflächen sowie Nutzerinteraktionen generisch und unabhängig von konkreten Modellentitäten zu beschreiben. Um diese abstrakte Beschreibung nutzen zu können, reichert man die Domänenmodelle um vormals implizite Informationen an. Neue Modelle müssen nur um einige Informationen erweitert werden um bereits vorhandene Nutzeroberflächen und -interaktionen auch für sie verwenden zu können. Anpassungen, die nur für ein Modell gelten sollen, können unabhängig vom Standardverhalten, inkrementell, definiert werden. Drittens: Wir ermöglichen mit einem weiteren Programmiersprachkonstrukt die zusammenhängende Beschreibung von Abläufen der Anwendung, wie z.B. Bestellprozesse. Unser Programmierkonzept kapselt Nutzerinteraktionen in synchrone Funktionsaufrufe und macht somit Prozesse als zusammenhängende Folge von Berechnungen und Interaktionen darstellbar. Viertens: Wir demonstrieren ein Konzept, wie Endnutzer komplexe analytische Anfragen intuitiver formulieren können. Es basiert auf der Idee, dass Endnutzer Anfragen als Konfiguration eines Diagramms sehen. Entsprechend beschreibt ein Nutzer eine Anfrage, indem er beschreibt, was sein Diagramm darstellen soll. Nach diesem Konzept beschriebene Diagramme enthalten ausreichend Informationen, um daraus eine Anfrage generieren zu können. Hinsichtlich der Ausführungsdauer sind die generierten Anfragen äquivalent zu Anfragen, die mit konventionellen Anfragesprachen formuliert sind. Das Anfragemodell setzen wir in einem Prototypen um, der auf den zuvor eingeführten Konzepten aufsetzt.

Eine der stärksten Erweiterungen der klassischen Theorie formaler Sprachen und Automaten ist die Einbeziehung von Gewichten oder Vielfachheiten aus einem Halbring. Diese Dissertation untersucht gewichtete Automaten über Strukturen mit Nebenläufigkeit. Wir erweitern die Arbeit von Lodaya und Weil und erhalten so ein Modell gewichteter verzweigender Automaten, in dem die Berechnung des Gewichts einer parallelen Komposition anders als die einer sequentiellen Komposition gehandhabt wird. Die von Lodaya und Weil eingeführten Automaten modellieren Nebenläufigkeit durch Verzweigen. Ein verzweigender Automat ist ein endlicher Automat mit drei verschiedenen Typen von Transitionen. Sequentielle Transitionen überführen durch Ausführen eines Ereignisses einen Zustand in einen anderen. Dagegen sind Gabel- und Binde-Transitionen für das Verzweigen verantwortlich. Läufe dieser Automaten werden beschrieben durch sequentiell-parallele posets, kurz sp-posets. Alle Transitionen des Automaten werden in unserem Modell mit Gewichten versehen. Neben dem Nichtdeterminismus und der sequentiellen Komposition wollen wir nun auch die parallele Komposition quantitativ behandeln. Dafür benötigen wir eine Gewichtsstruktur mit einer Addition, einer sequentiellen und einer parallelen Multiplikation. Solch eine Struktur, genannt Bihalbring, besteht damit de facto aus zwei Halbringen mit derselben additiven Struktur. Weiterhin muss die parallele Multiplikation kommutativ sein. Das Verhalten eines gewichteten verzweigenden Automaten ist dann eine Funktion, die jeder sp-poset ein Element eines Bihalbrings zuordnet. Das Hauptresultat charakterisiert das Verhalten dieser Automaten im Sinne von Kleenes und Schützenbergers Sätzen über das Zusammenfallen der Klassen der erkennbaren und der rationalen Sprachen bzw. formalen Potenzreihen. Darüber hinaus untersuchen wir den Abschluss dieser Verhalten unter allen rationalen Operationen und unter dem Hadamard-Produkt. Letztlich diskutieren wir Zusammenhänge zwischen Reihen und Sprachen im Rahmen verzweigender Automaten. / One of the most powerful extensions of classical formal language and automata theory is the consideration of weights or multiplicities from a semiring. This thesis investigates weighted automata over structures incorporating concurrency. Extending work by Lodaya and Weil, we propose a model of weighted branching automata in which the calculation of the weight of a parallel composition is handled differently from the calculation of the weight of a sequential composition. The automata as proposed by Lodaya and Weil model concurrency by branching. A branching automaton is a finite-state device with three different types of transitions. Sequential transitions transform a state into another one by executing an action. In contrast, fork and join transitions are responsible for branching. Executions of such systems can be described by sequential-parallel posets, or sp-posets for short. In the model considered here all kinds of transitions are equipped with weights. Beside non-determinism and sequential composition we would like to deal with the parallel composition in a quantitative way. Therefore, we are in need of a weight structure equipped with addition, a sequential, and, moreover, a parallel multiplication. Such a structure, called a bisemiring, is actually composed of two semirings with the same additive structure. Moreover, the parallel multiplication has to be commutative. Now, the behavior of a weighted branching automaton is a function that associates with every sp-poset an element from the bisemiring. The main result characterizes the behavior of these automata in the spirit of Kleene's and Schützenberger's theorems about the coincidence of recognizable and rational languages, and formal power series, respectively. Moreover, we investigate the closure of behaviors under all rational operations and under Hadamard-product. Finally, we discuss connections between series and languages within our setting.

Eine der stärksten Erweiterungen der klassischen Theorie formaler Sprachen und Automaten ist die Einbeziehung von Gewichten oder Vielfachheiten aus einem Halbring. Diese Dissertation untersucht gewichtete Automaten über Strukturen mit Nebenläufigkeit. Wir erweitern die Arbeit von Lodaya und Weil und erhalten so ein Modell gewichteter verzweigender Automaten, in dem die Berechnung des Gewichts einer parallelen Komposition anders als die einer sequentiellen Komposition gehandhabt wird. Die von Lodaya und Weil eingeführten Automaten modellieren Nebenläufigkeit durch Verzweigen. Ein verzweigender Automat ist ein endlicher Automat mit drei verschiedenen Typen von Transitionen. Sequentielle Transitionen überführen durch Ausführen eines Ereignisses einen Zustand in einen anderen. Dagegen sind Gabel- und Binde-Transitionen für das Verzweigen verantwortlich. Läufe dieser Automaten werden beschrieben durch sequentiell-parallele posets, kurz sp-posets. Alle Transitionen des Automaten werden in unserem Modell mit Gewichten versehen. Neben dem Nichtdeterminismus und der sequentiellen Komposition wollen wir nun auch die parallele Komposition quantitativ behandeln. Dafür benötigen wir eine Gewichtsstruktur mit einer Addition, einer sequentiellen und einer parallelen Multiplikation. Solch eine Struktur, genannt Bihalbring, besteht damit de facto aus zwei Halbringen mit derselben additiven Struktur. Weiterhin muss die parallele Multiplikation kommutativ sein. Das Verhalten eines gewichteten verzweigenden Automaten ist dann eine Funktion, die jeder sp-poset ein Element eines Bihalbrings zuordnet. Das Hauptresultat charakterisiert das Verhalten dieser Automaten im Sinne von Kleenes und Schützenbergers Sätzen über das Zusammenfallen der Klassen der erkennbaren und der rationalen Sprachen bzw. formalen Potenzreihen. Darüber hinaus untersuchen wir den Abschluss dieser Verhalten unter allen rationalen Operationen und unter dem Hadamard-Produkt. Letztlich diskutieren wir Zusammenhänge zwischen Reihen und Sprachen im Rahmen verzweigender Automaten. / One of the most powerful extensions of classical formal language and automata theory is the consideration of weights or multiplicities from a semiring. This thesis investigates weighted automata over structures incorporating concurrency. Extending work by Lodaya and Weil, we propose a model of weighted branching automata in which the calculation of the weight of a parallel composition is handled differently from the calculation of the weight of a sequential composition. The automata as proposed by Lodaya and Weil model concurrency by branching. A branching automaton is a finite-state device with three different types of transitions. Sequential transitions transform a state into another one by executing an action. In contrast, fork and join transitions are responsible for branching. Executions of such systems can be described by sequential-parallel posets, or sp-posets for short. In the model considered here all kinds of transitions are equipped with weights. Beside non-determinism and sequential composition we would like to deal with the parallel composition in a quantitative way. Therefore, we are in need of a weight structure equipped with addition, a sequential, and, moreover, a parallel multiplication. Such a structure, called a bisemiring, is actually composed of two semirings with the same additive structure. Moreover, the parallel multiplication has to be commutative. Now, the behavior of a weighted branching automaton is a function that associates with every sp-poset an element from the bisemiring. The main result characterizes the behavior of these automata in the spirit of Kleene's and Schützenberger's theorems about the coincidence of recognizable and rational languages, and formal power series, respectively. Moreover, we investigate the closure of behaviors under all rational operations and under Hadamard-product. Finally, we discuss connections between series and languages within our setting.

Multi-core processors require a program to be decomposable into independent parts that can execute in parallel in order to scale performance with the number of cores. But parallel programming is hard especially when the program requires state, which many system programs use for optimization, such as for example a cache to reduce disk I/O. Most prevalent parallel programming models do not support a notion of state and require the programmer to synchronize state access manually, i.e., outside the realms of an associated optimizing compiler. This prevents the compiler to introduce parallelism automatically and requires the programmer to optimize the program manually. In this dissertation, we propose a programming language/compiler co-design to provide a new programming model for implicit parallel programming with state and a compiler that can optimize the program for a parallel execution. We define the notion of a stateful function along with their composition and control structures. An example implementation of a highly scalable server shows that stateful functions smoothly integrate into existing programming language concepts, such as object-oriented programming and programming with structs. Our programming model is also highly practical and allows to gradually adapt existing code bases. As a case study, we implemented a new data processing core for the Hadoop Map/Reduce system to overcome existing performance bottlenecks. Our lambda-calculus-based compiler automatically extracts parallelism without changing the program's semantics. We added further domain-specific semantic-preserving transformations that reduce I/O calls for microservice programs. The runtime format of a program is a dataflow graph that can be executed in parallel, performs concurrent I/O and allows for non-blocking live updates.

In dieser Arbeit geht es um die schrittweise Verfeinerung verteilter Algorithmen. Dabei wird ein einfacher Algorithmus, der einige gewünschte Eigenschaften hat, Schritt für Schritt zu einem komplexen Algorithmus verfeinert, der konkrete Implementationsanforderungen erfüllt, so daß in jedem Schritt die gewünschten Eigenschaften erhalten bleiben. Wir stellen einen neuen eigenschaftserhaltenden Verfeinerungsbegriff vor, der auf der kausalen Ordnung der Aktionen eines Algorithmus basiert. Diesen Begriff definieren wir als Transitionsverfeinerung für elementare Petrinetze und diskutieren Beweiskriterien. Danach definieren und diskutieren wir die simultane Verfeinerung mehrerer Transitionen. Zur Modellierung komplexer verteilter Algorithmen sind elementare Petrinetze oft nicht adäquat. Wir benutzen deshalb algebraische Petrinetze. Wir definieren Transitionsverfeinerung für algebraische Petrinetze und stellen einen Zusammenhang zur simultanen Verfeinerung von Transitionen in elementaren Petrinetzen her. Transitionsverfeinerung ist besonders für Verfeinerungsschritte geeignet, in denen synchrone Kommunikation zwischen Agenten durch asynchronen Nachrichtenaustausch ersetzt wird. Wir zeigen dies am Beispiel eines komplexen verteilten Algorithmus, zur Berechnung des minimalen spannenden Baumes in einem gewichteten Graphen. Wir zeigen die Korrektheit dieses Algorithmus in mehreren Schritten, von denen einige Schritte Transitionsverfeinerungen sind. In anderen Schritten sind klassische Verfeinerungsbegriffe ausreichend. Wir übertragen deshalb auch einen klassischen Verfeinerungsbegriff in unser formales Modell. / The topic of this PhD thesis is the stepwise refinement of distributed algorithms. Stepwise refinement starts with a simple algorithm with certain desired properties. This algorithm is refined step by step such that the desired properties are preserved in each refinement step. The result is a complex distributed algorithm which satisfies concrete implementation requirements and which still has the desired properties. We propose a new property preserving notion of refinement which is based on the causal ordering of actions of an algorithm. We call this notion transition refinement and we define it first for elementary Petri nets. Furthermore, we discuss proof criteria. Then, we define and discuss the simultaneous refinement of several transitions. For modelling complex distributed algorithms, we use algebraic Petri nets instead of elementary Petri nets. We define transition refinement for algebraic Petri nets, and we show its relationship to simultaneous transition refinement in elementary Petri nets. Transition refinement is particularly suitable for refinement steps in which synchronous communication between agents is replaced by asynchronous message passing. We show this by means of a complex distributed algorithm for determining the minimal spanning tree of a weighted graph. We prove the correctness of this algorithm in several steps. Some of these steps are transition refinements. For other steps, well-known notions of refinement are sufficient. Therefore, we also carry over a well-known notion of refinement into our formal model.