TU Darmstadt / ULB / TUbiblio

On the Application of Formal Techniques for Dependable Concurrent Systems

Saissi, Habib (2019)
On the Application of Formal Techniques for Dependable Concurrent Systems.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung

Kurzbeschreibung (Abstract)

The pervasiveness of computer systems in virtually every aspect of daily life entails a growing dependence on them. These systems have become integral parts of our societies as we continue to use and rely on them on a daily basis. This trend of digitalization is set to carry on, bringing forth the question of how dependable these systems are. Our dependence on these systems is in acute need for a justification based on rigorous and systematic methods as recommended by internationally recognized safety standards. Ensuring that the systems we depend on meet these recommendations is further complicated by the increasingly widespread use of concurrent systems, which are notoriously hard to analyze due to the substantial increase in complexity that the interactions between different processing entities engenders.

In this thesis, we introduce improvements on existing formal analysis techniques to aid in the development of dependable concurrent systems. Applying formal analysis techniques can help us avoid incidents with catastrophic consequences by uncovering their triggering causes well in advance. This work focuses on three types of analyses: data-flow analysis, model checking and error propagation analysis. Data-flow analysis is a general static analysis technique aimed at predicting the values that variables can take at various points in a program. Model checking is a well-established formal analysis technique that verifies whether a program satisfies its specification. Error propagation analysis (EPA) is a dynamic analysis whose purpose is to assess a program's ability to withstand unexpected behaviors of external components. We leverage data-flow analysis to assist in the design of highly available distributed applications. Given an application, our analysis infers rules to distribute its workload across multiple machines, improving the availability of the overall system. Furthermore, we propose improvements to both explicit and bounded model checking techniques by exploiting the structure of the specification under consideration. The core idea behind these improvements lies in the ability to abstract away aspects of the program that are not relevant to the specification, effectively shortening the verification time. Finally, we present a novel approach to EPA based on symbolic modeling of execution traces. The symbolic scheme uses a dynamic sanitizing algorithm to eliminate effects of non-determinism in the execution traces of multi-threaded programs.The proposed approach is the first to achieve a 0% rate of false positives for multi-threaded programs.

The work in this thesis constitutes an improvement over existing formal analysis techniques that can aid in the development of dependable concurrent systems, particularly with respect to availability and safety.

Typ des Eintrags: Dissertation
Erschienen: 2019
Autor(en): Saissi, Habib
Art des Eintrags: Erstveröffentlichung
Titel: On the Application of Formal Techniques for Dependable Concurrent Systems
Sprache: Englisch
Referenten: Suri, Prof. Neeraj ; Kinder, Prof. Johannes
Publikationsjahr: 2019
Ort: Darmstadt
Datum der mündlichen Prüfung: 29 März 2019
URL / URN: https://tuprints.ulb.tu-darmstadt.de/8600
Kurzbeschreibung (Abstract):

The pervasiveness of computer systems in virtually every aspect of daily life entails a growing dependence on them. These systems have become integral parts of our societies as we continue to use and rely on them on a daily basis. This trend of digitalization is set to carry on, bringing forth the question of how dependable these systems are. Our dependence on these systems is in acute need for a justification based on rigorous and systematic methods as recommended by internationally recognized safety standards. Ensuring that the systems we depend on meet these recommendations is further complicated by the increasingly widespread use of concurrent systems, which are notoriously hard to analyze due to the substantial increase in complexity that the interactions between different processing entities engenders.

In this thesis, we introduce improvements on existing formal analysis techniques to aid in the development of dependable concurrent systems. Applying formal analysis techniques can help us avoid incidents with catastrophic consequences by uncovering their triggering causes well in advance. This work focuses on three types of analyses: data-flow analysis, model checking and error propagation analysis. Data-flow analysis is a general static analysis technique aimed at predicting the values that variables can take at various points in a program. Model checking is a well-established formal analysis technique that verifies whether a program satisfies its specification. Error propagation analysis (EPA) is a dynamic analysis whose purpose is to assess a program's ability to withstand unexpected behaviors of external components. We leverage data-flow analysis to assist in the design of highly available distributed applications. Given an application, our analysis infers rules to distribute its workload across multiple machines, improving the availability of the overall system. Furthermore, we propose improvements to both explicit and bounded model checking techniques by exploiting the structure of the specification under consideration. The core idea behind these improvements lies in the ability to abstract away aspects of the program that are not relevant to the specification, effectively shortening the verification time. Finally, we present a novel approach to EPA based on symbolic modeling of execution traces. The symbolic scheme uses a dynamic sanitizing algorithm to eliminate effects of non-determinism in the execution traces of multi-threaded programs.The proposed approach is the first to achieve a 0% rate of false positives for multi-threaded programs.

The work in this thesis constitutes an improvement over existing formal analysis techniques that can aid in the development of dependable concurrent systems, particularly with respect to availability and safety.

Alternatives oder übersetztes Abstract:
Alternatives AbstractSprache

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.

Deutsch
URN: urn:nbn:de:tuda-tuprints-86009
Sachgruppe der Dewey Dezimalklassifikatin (DDC): 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Fachbereich(e)/-gebiet(e): 20 Fachbereich Informatik
20 Fachbereich Informatik > Zuverlässige Eingebettete Softwaresysteme
Hinterlegungsdatum: 26 Mai 2019 19:55
Letzte Änderung: 26 Mai 2019 19:55
PPN:
Referenten: Suri, Prof. Neeraj ; Kinder, Prof. Johannes
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: 29 März 2019
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen