318
5 Bewertung und Validierung
Logik erster Ordnung automatisieren. Es wurde zum ersten Mal im Jahr 1987 unter Verwendung binärer Entscheidungsdiagramme (BDDs) implementiert. Model
checking war dazu in der Lage, verschiedene Fehler in der Spezifikation des future
bus-Protokolls zu entdecken [104]. UPPAAL ist ein sehr viel genutztes Werkzeug
für das model checking13.
Diese Technik könnte beispielsweise genutzt werden, um Eigenschaften des Modells der Zugbewegungen aus Abb. 2.52 zu beweisen (siehe Seite 91). Es sollte
möglich sein, das Petrinetz in ein StateChart umzuwandeln und dann nachzuweisen,
dass die Anzahl der Züge zwischen Köln und Paris in der Tat konstant ist, wodurch
unsere Diskussion von Ortsinvarianten von Petrinetzen von Seite 89 bestätigt würde.
Weitere Techniken werden von Haubelt und Teich beschrieben [207].
5.10 Aufgaben
Die folgenden Aufgaben sollten entweder zu Hause oder während einer Anwesenheitsphase nach dem flipped classroom-Konzept [376] bearbeitet werden:
5.1: Wir betrachten ein Anwendungsbeispiel der Pareto-Optimalität auf der Basis
von Ergebnissen der Task Concurrency Management (TCM) Werkzeuge des IMECForschungszentrums. In diesem Beispiel werden verschiedene Optionen betrachtet, mit denen ein MPEG-4-Abspielprogramm auf Mehrkern-Prozessoren verteilt
werden können [595]. Wong et al. nehmen dabei an, dass eine Kombination von
StrongARM-Prozessoren und speziellen Hardwarebeschleunigern benutzt werden
soll. Vier Entwürfe erfüllen die Zeitbeschränkung von 30 ms (siehe Tabelle 5.4). Für
Tabelle 5.4 Prozessorkonfigurationen
Prozessorkonfiguration
1 2 3 4
Anzahl schneller Prozessoren
6 5 4 3
Anzahl langsamer Prozessoren 0 3 5 7
Anzahl Prozessoren insgesamt 6 8 9 10
die Kombinationen 1 und 4 erfüllt nur eine Abbildung von Tasks auf Prozessoren die
Zeitbeschränkung. Für die Kombinationen 2 und 3 gibt es verschiedene zulässige
Task/Prozessorzuordnungen. Diese werden in Abb. 5.33 gezeigt. Welche Fläche
im Raum der Zielkriterien ist durch mindestens eine Task/Prozessorzuordnung der
Konfiguration 3 dominiert? Gibt es eine Task/Prozessorzuordnung der Konfiguration 2, die nicht durch eine Task/Prozessorzuordnung der Konfiguration 3 dominiert wird? Welche Fläche im Raum der Zielkriterien dominiert mindestens eine
Task/Prozessorzuordnung der Konfiguration 3?
13 Siehe http://www.uppaal.org für die akademische und http://www.uppaal.com für die kommerzielle Version.
5 Bewertung und Validierung
Logik erster Ordnung automatisieren. Es wurde zum ersten Mal im Jahr 1987 unter Verwendung binärer Entscheidungsdiagramme (BDDs) implementiert. Model
checking war dazu in der Lage, verschiedene Fehler in der Spezifikation des future
bus-Protokolls zu entdecken [104]. UPPAAL ist ein sehr viel genutztes Werkzeug
für das model checking13.
Diese Technik könnte beispielsweise genutzt werden, um Eigenschaften des Modells der Zugbewegungen aus Abb. 2.52 zu beweisen (siehe Seite 91). Es sollte
möglich sein, das Petrinetz in ein StateChart umzuwandeln und dann nachzuweisen,
dass die Anzahl der Züge zwischen Köln und Paris in der Tat konstant ist, wodurch
unsere Diskussion von Ortsinvarianten von Petrinetzen von Seite 89 bestätigt würde.
Weitere Techniken werden von Haubelt und Teich beschrieben [207].
5.10 Aufgaben
Die folgenden Aufgaben sollten entweder zu Hause oder während einer Anwesenheitsphase nach dem flipped classroom-Konzept [376] bearbeitet werden:
5.1: Wir betrachten ein Anwendungsbeispiel der Pareto-Optimalität auf der Basis
von Ergebnissen der Task Concurrency Management (TCM) Werkzeuge des IMECForschungszentrums. In diesem Beispiel werden verschiedene Optionen betrachtet, mit denen ein MPEG-4-Abspielprogramm auf Mehrkern-Prozessoren verteilt
werden können [595]. Wong et al. nehmen dabei an, dass eine Kombination von
StrongARM-Prozessoren und speziellen Hardwarebeschleunigern benutzt werden
soll. Vier Entwürfe erfüllen die Zeitbeschränkung von 30 ms (siehe Tabelle 5.4). Für
Tabelle 5.4 Prozessorkonfigurationen
Prozessorkonfiguration
1 2 3 4
Anzahl schneller Prozessoren
6 5 4 3
Anzahl langsamer Prozessoren 0 3 5 7
Anzahl Prozessoren insgesamt 6 8 9 10
die Kombinationen 1 und 4 erfüllt nur eine Abbildung von Tasks auf Prozessoren die
Zeitbeschränkung. Für die Kombinationen 2 und 3 gibt es verschiedene zulässige
Task/Prozessorzuordnungen. Diese werden in Abb. 5.33 gezeigt. Welche Fläche
im Raum der Zielkriterien ist durch mindestens eine Task/Prozessorzuordnung der
Konfiguration 3 dominiert? Gibt es eine Task/Prozessorzuordnung der Konfiguration 2, die nicht durch eine Task/Prozessorzuordnung der Konfiguration 3 dominiert wird? Welche Fläche im Raum der Zielkriterien dominiert mindestens eine
Task/Prozessorzuordnung der Konfiguration 3?
13 Siehe http://www.uppaal.org für die akademische und http://www.uppaal.com für die kommerzielle Version.