Real-time systems do not only require that the logical operations are correct. Equally important is that the specified time constraints always are complied. This has successfully been studied before for mono-processor systems. However, as the hardware in the systems gets more complex, the previous approaches become invalidated. For example, multi-processor systems-on-chip (MPSoC) get more and more common every day, and together with a shared memory, the bus access time is unpredictable in nature. This has recently been resolved, but a safe and not too pessimistic cache analysis approach for MPSoC has not been investigated before. This thesis has resulted in designed and implemented algorithms for cache analysis on real-time MPSoC with a shared communication infrastructure. An additional advantage is that the algorithms include improvements compared to previous approaches for mono-processor systems. The verification of these algorithms has been performed with the help of data flow analysis theory. Furthermore, it is not known how different types of cache miss characteristic of a task influence the worst case execution time on MPSoC. Therefore, a program that generates randomized tasks, according to different parameters, has been constructed. The parameters can, for example, influence the complexity of the control flow graph and average distance between the cache misses.

Value-range analysis is a static analysis technique based on arguing about the values that a variable may take on a given program point. It can be used to prove absence of run-time errors such as out-of-bound array accesses. Since value-range analysis collects information on each program point, data-flow analysis can be used in association with it. The main goal of this work is designing and implementing such a value-range analysis tool. The work begins with an introduction into the topic, an explanation of data-flow and value-range analyses and a description of abstract interpretation, which provides the formal basis of the analyser. The core of this work is the design, implementation, testing and evaluation of the analyser. In the conclusion, our personal experience obtained in the area of the thesis is mentioned, along with a discussion of a possible future development of the designed tool.

Seit 1983 begründet die Publikationsreihe "Graph Minors" von N. Robertson und P.D. Seymour im Wesentlichen die Minorentheorie mit mächtigen Hilfsmitteln wie der Baumzerlegung und weitreichenden Resultaten wie dem Minorensatz. Für gerichtete Graphen existiert allerdings noch keine einheitliche Minorentheorie und verschiedene Ansätze werden in dieser Arbeit systematisiert. Einige gerichtete Versionen der Baumzerlegung (gerichtete Baumzerlegung nach B. Reed, arboreale, D- und DAG-Zerlegung) werden unter einheitlichen Aspekten untersucht. Die D-Weite ist dabei besonders vielversprechend. Enge Verbindungen zu zwei gerichteten Räuber-und-Gendarmen-Spielen werden unter analogen Aspekten betrachtet und sind wichtige Hilfsmittel. Der zentrale Begriff des Minoren ist im Wesentlichen für ungerichtete Graphen definiert und eine gerichtete Version wirft einige Probleme auf, welche untersucht werden. In \"Directed Tree-Width\" schlugen T. Johnson, N. Robertson, P.D. Seymour und R. Thomas 2001 einen Kompromiss vor. Durch Einschränkung der möglichen Kontraktionen soll der gewonnen Minorenbegriff mit einigen fundamentalen Anforderungen vereinbar sein und trotzdem ein mächtiges Werkzeug darstellen. Dieser Ansatz wird mit einer Anforderungsliste systematisch verfolgt und schrittweise Einschränkungen betrachtet. Die gerichtete Version topologischer Minoren ist dabei besonders vielversprechend. Die Minorentheorie gerichteter Graphen wird auf reduzible Flussgraphen angewandt. Wesentliche Resultate sind Konstruktionen arborealer und D-Zerlegungen mit Weite <2, sowie Gegenbeispiele für die Beschränktheit der DAG-Weite. Analoge Resultate folgen für die jeweiligen gerichteten Räuber-und-Gendarmen-Spiele.

Seit 1983 begründet die Publikationsreihe "Graph Minors" von N. Robertson und P.D. Seymour im Wesentlichen die Minorentheorie mit mächtigen Hilfsmitteln wie der Baumzerlegung und weitreichenden Resultaten wie dem Minorensatz. Für gerichtete Graphen existiert allerdings noch keine einheitliche Minorentheorie und verschiedene Ansätze werden in dieser Arbeit systematisiert. Einige gerichtete Versionen der Baumzerlegung (gerichtete Baumzerlegung nach B. Reed, arboreale, D- und DAG-Zerlegung) werden unter einheitlichen Aspekten untersucht. Die D-Weite ist dabei besonders vielversprechend. Enge Verbindungen zu zwei gerichteten Räuber-und-Gendarmen-Spielen werden unter analogen Aspekten betrachtet und sind wichtige Hilfsmittel. Der zentrale Begriff des Minoren ist im Wesentlichen für ungerichtete Graphen definiert und eine gerichtete Version wirft einige Probleme auf, welche untersucht werden. In \"Directed Tree-Width\" schlugen T. Johnson, N. Robertson, P.D. Seymour und R. Thomas 2001 einen Kompromiss vor. Durch Einschränkung der möglichen Kontraktionen soll der gewonnen Minorenbegriff mit einigen fundamentalen Anforderungen vereinbar sein und trotzdem ein mächtiges Werkzeug darstellen. Dieser Ansatz wird mit einer Anforderungsliste systematisch verfolgt und schrittweise Einschränkungen betrachtet. Die gerichtete Version topologischer Minoren ist dabei besonders vielversprechend. Die Minorentheorie gerichteter Graphen wird auf reduzible Flussgraphen angewandt. Wesentliche Resultate sind Konstruktionen arborealer und D-Zerlegungen mit Weite <2, sowie Gegenbeispiele für die Beschränktheit der DAG-Weite. Analoge Resultate folgen für die jeweiligen gerichteten Räuber-und-Gendarmen-Spiele.:1 Einleitung 1.1 Grundbegriffe der Graphentheorie 1.2 Reduzibilität 2 Über Minoren von Graphen 2.1 Minoren von Graphen 2.2 Topologische Minoren von Graphen 2.3 Baumzerlegung und Baumweite tw(G) 2.4 Wegzerlegung und Wegbreite pw(G) 2.5 Räuber-und-Gendarmen-Spiele auf Graphen 2.6 Resultate und Anwendungen 3 Über Minoren von Digraphen 3.1 Übertragung der Minorenrelation auf Digraphen 3.2 Hindernisse bei der De?nition einer gerichteten Baumweite 3.3 Arboreale Weite dtw(D) 3.3.1 Arboreale Weite und Räuber-und-Gendarmen-Spiele 3.3.2 Resultate und Anwendungen 3.4 Gerichtete Baumweite dtwR(D) 3.5 D-Weite dw(D) 3.6 DAG-Weite dgw(D) 3.6.1 DAG-Weite und Räuber-und-Gendarmen-Spiele 3.6.2 Resultate und Anwendungen 3.7 Räuber-und-Gendarmen-Spiele auf Digraphen 3.8 Eingeschränkte Minorenrelation für Digraphen 3.8.1 Die Teilgraphenrelation für Digraphen 3.8.2 Die topologische Minorenrelation für Digraphen 3.8.3 Die Minorenrelation auf Digraphen nach JRST 3.8.4 Eingeschränkte Minorenrelationen 4 Verbindungen zwischen Reduzibilität und Minoren von Digraphen 4.1 Reduzibilität und initiale Wurzeldigraphen 4.2 Charakterisierung der Reduzibilität durch eingeschränkte Minoren 4.3 Resultate der Minorentheorie für reduzible initiale Wurzeldigraphen 5 Zusammenfassung und Ausblick Literaturverzeichnis Abbildungsverzeichnis

State explosion in model checking continues to be the primary obstacle to widespread use of software model checking. The large input ranges of variables used in software is the main cause of state explosion. As software grows in size and complexity the problem only becomes worse. As such, model checking research into data abstraction as a way of mitigating state explosion has become more and more important. Data abstractions aim to reduce the effect of large input ranges. This work focuses on a static program analysis technique called dead variable analysis. The goal of dead variable analysis is to discover variable assignments that are not used. When applied to model checking, this allows us to ignore the entire input range of dead variables and thus reduce the size of the explored state space. Prior research into dead variable analysis for model checking does not make full use of dynamic run-time information that is present during model checking. We present an algorithm for intraprocedural dead variable analysis that uses dynamic run-time information to find more dead variables on-the-fly and further reduce the size of the explored state space. We introduce a definition for the maximal state space reduction possible through an on-the-fly dead variable analysis and then show that our algorithm produces a maximal reduction in the absence of non-determinism.