Der Einzug von Computersystemen in nahezu allen Bereichen des täglichen Lebens führt zu einer zunehmenden Abhängigkeit von ihnen. Diese Systeme sind zu einem festen Bestandteil unserer Gesellschaft geworden, da wir sie täglich nutzen und uns auf sie verlassen. Dieser Digitalisierungstrend wird sich fortsetzen, so dass sich die Frage stellt, wie zuverlässig diese Systeme sind. Unsere Abhängigkeit von diesen Systemen erfordert dringend Rechtfertigung aufgrund strenger und systematischer Methoden, die von international anerkannten Sicherheitsstandards empfohlen werden. Die Sicherstellung, dass die Systeme, auf die wir angewiesen sind, die Empfehlungen der Sicherheitsstandards erfüllen, wird durch den zunehmend verbreiteten Einsatz von nebenläufigen Systemen zusätzlich erschwert. Nebenläufige Systeme sind bekanntermaßen schwer zu analysieren, da die Interaktionen zwischen verschiedenen Verarbeitungseinheiten erheblich komplexer werden. In dieser Arbeit stellen wir Verbesserungen an bestehenden formalen Analysetechniken vor, um die Entwicklung zuverlässiger nebenläufiger Systeme zu unterstützen. Die Anwendung formaler Analysetechniken kann dazu beitragen, Vorfälle mit katastrophalen Folgen zu vermeiden, indem ihre auslösenden Ursachen frühzeitig aufgedeckt werden.

Diese Arbeit konzentriert sich auf drei Arten von Analysen: Datenflussanalyse, Model Checking und Error-Propagation-Analyse. Die Datenflussanalyse ist eine allgemeine statische Analysetechnik, die darauf abzielt, die Werte vorherzusagen, die Variablen an verschiedenen Stellen eines Programms annehmen können. Model Checking ist eine etablierte formale Analysetechnik, mit der überprüft wird, ob ein Programm seinen Spezifikationen erfüllt. Die Error-Propagation-Analyse (EPA) ist eine dynamische Analyse, deren Zweck es ist, zu bewerten ob ein Programm unerwartetem Verhalten externer Komponenten standhalten kann. Wir nutzen Datenflussanalysen, um das Design hochverfügbarer verteilter Anwendungen zu unterstützen. Bei einer Anwendung werden in unserer Analyse Regeln festgelegt, um die Arbeitslast auf mehrere Maschinen zu verteilen und die Verfügbarkeit des Gesamtsystems zu verbessern. Darüber hinaus schlagen wir Verbesserungen sowohl für explizites Model Checking als auch für Bounded Model Checking vor, indem die Struktur der betrachteten Spezifikation genutzt wird. Die Kernidee hinter unseren Verbesserungen liegt in der Fähigkeit, Aspekte des Programms, die für die Spezifikation nicht relevant sind, zu abstrahieren. Schließlich stellen wir einen neuen Ansatz für die EPA vor, der auf der symbolischen Modellierung von Ausführungen basiert. Der symbolische Ansatz verwendet einen dynamischen Sanitizing-Algorithmus, um die Auswirkungen von Nicht-Determinismus in Ausführungen von Multi-Threaded-Programmen zu beseitigen. Der vorgeschlagene Ansatz ist der erste, der bei Multi-Threaded-Programmen eine False-Positives Rate von 0% erzielt.

Die vorliegende Arbeit stellt eine Verbesserung gegenüber bestehenden formalen Analysetechniken dar, die zur Entwicklung zuverlässiger nebenläufiger Systeme beitragen können, insbesondere hinsichtlich der Verfügbarkeit und Sicherheit.