Post on 22-Apr-2015
description
01/04/11
Formale Fundierung und e!zientere Implementierung der schrittbasierten TLDA-
InterleavingsemantikDiplomverteidigung
Niels Lohmann
nlohmann@informatik.hu-berlin.dehttp://www.informatik.hu-berlin.de/~nlohmann/studium
2
Diplom-verteidigung
Motivation der Arbeit
! Mit TLDA können verteilte Systeme spezifiziert werden. Und dann?
! Ziel: Modelchecker für TLDA
! Studienarbeit: Entwicklung und Implementierung einer Interleavingsemantik für TLDA
! Diplomarbeit: formale Fundierung und verbesserte Algorithmen
3
Diplom-verteidigung
Gliederung
1. Konsumenten-/Produzentensystem
2. Einführung in TLDA
3. Semantiken
4. Transitionssysteme
5. Formale Fundierung6. E!zientere Algorithmen
7. Ausblick
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
4
Diplom-verteidigung
Konsumenten-/Produzentensystem
! Der Produzent produziertspontan einen Gegenstandund legt ihn im Pu"er ab.
! Der Pu!er kann höchstens einen Gegenstand aufnehmen.
! Der Konsument entnimmtspontan Gegenstand ausdem Pu"er und konsumiert ihn.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
5
Diplom-verteidigung
verteiltes System mit drei Komponenten:
! Produzent:
Konsumenten-/Produzentensystem
ready toconsume
ready toremove
filledempty
ready todeliver
ready toproduce
produce
deliver
filling
emptying
remove
consume
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
5
Diplom-verteidigung
verteiltes System mit drei Komponenten:
! Produzent:
! Pu"er:
Konsumenten-/Produzentensystem
ready toconsume
ready toremove
filledempty
ready todeliver
ready toproduce
produce
deliver
filling
emptying
remove
consume
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
5
Diplom-verteidigung
verteiltes System mit drei Komponenten:
! Produzent:
! Pu"er:
! Konsument:
Konsumenten-/Produzentensystem
ready toconsume
ready toremove
filledempty
ready todeliver
ready toproduce
produce
deliver
filling
emptying
remove
consume
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
5
Diplom-verteidigung
verteiltes System mit drei Komponenten:
! Produzent:
! Pu"er:
! Konsument:
drei Systemvariablen:
Konsumenten-/Produzentensystem
ready toconsume
ready toremove
filledempty
ready todeliver
ready toproduce
produce
deliver
filling
emptying
remove
consume
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
6
Diplom-verteidigung
Konsumenten-/Produzentensystem
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
6
Diplom-verteidigung
Konsumenten-/Produzentensystem
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
6
Diplom-verteidigung
Konsumenten-/Produzentensystem
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
6
Diplom-verteidigung
Konsumenten-/Produzentensystem
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
7
Diplom-verteidigung
Einführung in TLDA
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
7
Diplom-verteidigung
Einführung in TLDA
Das semantische Modell ist ein Ablauf.
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
7
Diplom-verteidigung
Einführung in TLDA
Das semantische Modell ist ein Ablauf.
! ein Schnitt kann als lokaler Zustand aufgefasst werden
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
7
Diplom-verteidigung
Einführung in TLDA
Das semantische Modell ist ein Ablauf.
! ein Schnitt kann als lokaler Zustand aufgefasst werden
! jeder Ablauf hat einen Anfangsschnitt
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C0 C
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
8
Diplom-verteidigung
Einführung in TLDA
rp
0
rr
rd
§
rp t1 rd rp
t2 rc rr
1 0 1
…
…
…
C
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
8
Diplom-verteidigung
Einführung in TLDA
rp
0
rr
rd
§
rp t1 rd rp
t2 rc rr
1 0 1
…
…
…
C!C
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
8
Diplom-verteidigung
! wenn alle möglichen Transitionen schalten, wird der Nachfolgeschnitt C' erreicht
Einführung in TLDA
rp
0
rr
rd
§
rp t1 rd rp
t2 rc rr
1 0 1
…
…
…
C!C
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
8
Diplom-verteidigung
! wenn alle möglichen Transitionen schalten, wird der Nachfolgeschnitt C' erreicht
! die Schnitte C, C' und die Transitionen bilden einen Schritt
Einführung in TLDA
rp
0
rr
rd
§
rp t1 rd rp
t2 rc rr
1 0 1
…
…
…
C!C
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
8
Diplom-verteidigung
! wenn alle möglichen Transitionen schalten, wird der Nachfolgeschnitt C' erreicht
! die Schnitte C, C' und die Transitionen bilden einen Schritt
Einführung in TLDA
rp
0
rr
rd
§
rp t1 rd rp
t2 rc rr
1 0 1
…
…
…
C!C
Dieser Schnitt kann nichtdurch Schritte erreicht werden
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
9
Diplom-verteidigung
! Halbordnungssemantik
Semantiken
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
s rp t rd rp
u rc rr
1 0 1
…
…
…
9
Diplom-verteidigung
! Halbordnungssemantik! Transitionen sind halbgeordnet:
Semantiken
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
s rp t rd rp
u rc rr
1 0 1
…
…
…
9
Diplom-verteidigung
! Halbordnungssemantik! Transitionen sind halbgeordnet:
! Transition s schaltet vor t
Semantiken
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
s rp t rd rp
u rc rr
1 0 1
…
…
…
9
Diplom-verteidigung
! Halbordnungssemantik! Transitionen sind halbgeordnet:
! Transition s schaltet vor t
! Transitionen t und u sind nebenläufig:es gibt keine Reihenfolge
Semantiken
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
s rp t rd rp
u rc rr
1 0 1
…
…
…
10
Diplom-verteidigung
Semantiken
Erst t, dann u!
rp1rr
t u
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rd1rr
rd0rc
10
Diplom-verteidigung
Semantiken
Erst t, dann u!
rp1rr
t u
u tErst u, dann t!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rd1rr
rd0rc
rp1rr
rp0rc
rd0rc
10
Diplom-verteidigung
Semantiken
Erst t, dann u!
rp1rr
t u
u t
{t, u}
Erst u, dann t!
t und u schalten gleichzeitig!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rd1rr
rd0rc
rp1rr
rp0rc
rd0rc
rp1rr
rd0rc
10
Diplom-verteidigung
! Interleavingsemantik
Semantiken
Erst t, dann u!
rp1rr
t u
u t
{t, u}
Erst u, dann t!
t und u schalten gleichzeitig!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rd1rr
rd0rc
rp1rr
rp0rc
rd0rc
rp1rr
rd0rc
10
Diplom-verteidigung
! Interleavingsemantik! betrachtet alle möglichen Reihenfolgen:
Semantiken
Erst t, dann u!
rp1rr
t u
u t
{t, u}
Erst u, dann t!
t und u schalten gleichzeitig!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rd1rr
rd0rc
rp1rr
rp0rc
rd0rc
rp1rr
rd0rc
10
Diplom-verteidigung
! Interleavingsemantik! betrachtet alle möglichen Reihenfolgen:
! total geordnet
Semantiken
Erst t, dann u!
rp1rr
t u
u t
{t, u}
Erst u, dann t!
t und u schalten gleichzeitig!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rd1rr
rd0rc
rp1rr
rp0rc
rd0rc
rp1rr
rd0rc
10
Diplom-verteidigung
! Interleavingsemantik! betrachtet alle möglichen Reihenfolgen:
! total geordnet! exponentielle Anzahl von Interleavings und
Zwischenzuständen
Semantiken
Erst t, dann u!
rp1rr
t u
u t
{t, u}
Erst u, dann t!
t und u schalten gleichzeitig!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rd1rr
rd0rc
rp1rr
rp0rc
rd0rc
rp1rr
rd0rc
11
Diplom-verteidigung
Semantiken
! Halbordnungssemantiken:+ sehr ausdrucksstark! kaum Erfahrungen bei der
computergestützten Verifikation
! Interleavingsemantiken:! Zustandsexplosion+ sehr einfach+ können leicht durch Graphen
(Transitionssysteme) repräsentiert werden+ explizites Modelchecking weit verbreitet
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
12
Diplom-verteidigung
Transitionssystem
Definition: TS = (S, S0, Act, R, L)
buff h 0 buff h 1 buff h 0
s0 s1 s2
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
12
Diplom-verteidigung
Transitionssystem
Definition: TS = (S, S0, Act, R, L)! S: Zustandsmenge
buff h 0 buff h 1 buff h 0
s0 s1 s2
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
12
Diplom-verteidigung
Transitionssystem
Definition: TS = (S, S0, Act, R, L)! S: Zustandsmenge
! S0 ! S: Menge der Anfangszustände
buff h 0 buff h 1 buff h 0
s0 s1 s2
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
12
Diplom-verteidigung
Transitionssystem
Definition: TS = (S, S0, Act, R, L)! S: Zustandsmenge
! S0 ! S: Menge der Anfangszustände
! Act: Aktionsmenge
buff h 0 buff h 1 buff h 0a0 a1
a3
s0 s1 s2
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
a2
12
Diplom-verteidigung
Transitionssystem
Definition: TS = (S, S0, Act, R, L)! S: Zustandsmenge
! S0 ! S: Menge der Anfangszustände
! Act: Aktionsmenge
! R ! S " Act " S: Übergangsrelation
buff h 0 buff h 1 buff h 0a0 a1
a3
s0 s1 s2
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
a2
12
Diplom-verteidigung
Transitionssystem
Definition: TS = (S, S0, Act, R, L)! S: Zustandsmenge
! S0 ! S: Menge der Anfangszustände
! Act: Aktionsmenge
! R ! S " Act " S: Übergangsrelation
! L: S ! (Var ! Val): Zustandsbeschriftung
buff h 0 buff h 1 buff h 0a0 a1
a3
s0 s1 s2
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
a2
13
Diplom-verteidigung
Transitionssystem
Wir können ein Transitionssystem TS! für
TLDA-Spezifikationen ! in Normalform bilden:
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
13
Diplom-verteidigung
Transitionssystem
Wir können ein Transitionssystem TS! für
TLDA-Spezifikationen ! in Normalform bilden:
! Definition: Normalform:! , Init # □ Next
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
13
Diplom-verteidigung
Transitionssystem
Wir können ein Transitionssystem TS! für
TLDA-Spezifikationen ! in Normalform bilden:
! Definition: Normalform:! , Init # □ Next
! Aktionsmenge:Act ist die Menge der Klauseln der disjunktiven Normalform von Next.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
14
Diplom-verteidigung
Transitionssystem
! Zustände, Anfangszustände, Beschriftung
Für alle von C0 durch Schritte erreichbaren Schnitte füge einen neuen Zustand hinzu und beschrifte ihn.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
14
Diplom-verteidigung
Transitionssystem
! Zustände, Anfangszustände, Beschriftung
Für alle von C0 durch Schritte erreichbaren Schnitte füge einen neuen Zustand hinzu und beschrifte ihn.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C0
14
Diplom-verteidigung
Transitionssystem
sC0
! Zustände, Anfangszustände, Beschriftung
Für alle von C0 durch Schritte erreichbaren Schnitte füge einen neuen Zustand hinzu und beschrifte ihn.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C0
14
Diplom-verteidigung
Transitionssystem
sC0
! Zustände, Anfangszustände, Beschriftung
Für alle von C0 durch Schritte erreichbaren Schnitte füge einen neuen Zustand hinzu und beschrifte ihn.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C0 C1
14
Diplom-verteidigung
Transitionssystem
sC0sC1
! Zustände, Anfangszustände, Beschriftung
Für alle von C0 durch Schritte erreichbaren Schnitte füge einen neuen Zustand hinzu und beschrifte ihn.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C0 C1
14
Diplom-verteidigung
Transitionssystem
sC0sC1
sC2
! Zustände, Anfangszustände, Beschriftung
Für alle von C0 durch Schritte erreichbaren Schnitte füge einen neuen Zustand hinzu und beschrifte ihn.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C0 C1 C2
14
Diplom-verteidigung
Transitionssystem
sC0sC1
sC2
! Zustände, Anfangszustände, Beschriftung
Wiederhole dies für alle Abläufe von !.
Für alle von C0 durch Schritte erreichbaren Schnitte füge einen neuen Zustand hinzu und beschrifte ihn.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C0 C1 C2
15
Diplom-verteidigung
Transitionssystem
! Zustandsübergänge:
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
sC0sC1
sC2
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C0 C1 C2
15
Diplom-verteidigung
Transitionssystem
! Zustandsübergänge:
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
sC0sC1
sC2
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C0 C1 C2
15
Diplom-verteidigung
Transitionssystem
! Zustandsübergänge:
Jeder Schritt erfüllt Klauselmenge A von Next.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
sC0sC1
sC2
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C0 C1 C2
15
Diplom-verteidigung
Transitionssystem
! Zustandsübergänge:
Jeder Schritt erfüllt Klauselmenge A von Next.Beschrifte Zustandsübergänge mit "i ("i $ A).
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
sC0sC1
sC2
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C0 C1 C2
15
Diplom-verteidigung
Transitionssystem
! Zustandsübergänge:
Jeder Schritt erfüllt Klauselmenge A von Next.Beschrifte Zustandsübergänge mit "i ("i $ A).
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
sC0sC1
sC2
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C0 C1 C2
15
Diplom-verteidigung
Transitionssystem
! Zustandsübergänge:
Jeder Schritt erfüllt Klauselmenge A von Next.Beschrifte Zustandsübergänge mit "i ("i $ A).
Wiederhole dies für alle Abläufe von !.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
sC0sC1
sC2
rp
0
rr
rd
§
rp rd rp
rc rr
1 0 1
…
…
…
C0 C1 C2
16
Diplom-verteidigung
Formale Fundierung
Eigenschaften von TS!:
! Für alle Abläufe von !, für alle Schnitte C, die mit Schritten erreichbar sind, existiert ein erreichbarer entsprechender Zustand sC in TS!.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
16
Diplom-verteidigung
Formale Fundierung
Eigenschaften von TS!:
! Für alle Abläufe von !, für alle Schnitte C, die mit Schritten erreichbar sind, existiert ein erreichbarer entsprechender Zustand sC in TS!.
! Für alle erreichbaren Zustände sC in TS!
existiert ein Ablauf von ! mit einem entsprechenden Schnitt C, der mit Schritten erreichbar ist.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
17
Diplom-verteidigung
Formale Fundierung
Können wir alle Schnitte mit Schrittenvon C0 aus erreichen?
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd rp t rd rp
u rc rr
1 0 1
…
…
…
! u1 ! u2 ! u3 ! !
§
C0 C1 C2 C3"*
17
Diplom-verteidigung
Formale Fundierung
Können wir alle Schnitte mit Schrittenvon C0 aus erreichen?
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd rp t rd rp
u rc rr
1 0 1
…
…
…
! u1 ! u2 ! u3 ! !
§
C0 C1 C2 C* C3"*
17
Diplom-verteidigung
Formale Fundierung
Können wir alle Schnitte mit Schrittenvon C0 aus erreichen?
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd rp t rd rp
u rc rr
1 0 1
…
…
…
! u1 ! u2 ! u3 ! !
§
C0 C1 C2 C* C3"*
17
Diplom-verteidigung
Formale Fundierung
Können wir alle Schnitte mit Schrittenvon C0 aus erreichen?
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd rp t rd rp
u rc rr
1 0 1
…
…
…
! u1 ! u2 ! u3 ! !§
C0 C1 C2 C* C3"*
17
Diplom-verteidigung
Formale Fundierung
Können wir alle Schnitte mit Schrittenvon C0 aus erreichen? "
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd rp t rd rp
u rc rr
1 0 1
…
…
…
! u1 ! u2 ! u3 ! !§
C0 C1 C2 C* C3"*
18
Diplom-verteidigung
Formale Fundierung
Gilt #$ !? Nicht notwendigerweise!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
18
Diplom-verteidigung
Formale Fundierung
Gilt #$ !?
Es gilt jedoch stets für umgebungs-invariante Formeln.
Nicht notwendigerweise!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
18
Diplom-verteidigung
Formale Fundierung
Gilt #$ !?
Es gilt jedoch stets für umgebungs-invariante Formeln.
Nicht notwendigerweise!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
18
Diplom-verteidigung
Formale Fundierung
Gilt #$ !?
Es gilt jedoch stets für umgebungs-invariante Formeln.
Kann wörtlich verstanden werden:
Nicht notwendigerweise!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
18
Diplom-verteidigung
Formale Fundierung
Gilt #$ !?
Es gilt jedoch stets für umgebungs-invariante Formeln.
Kann wörtlich verstanden werden:
Eine Formel ! ist umgebungsinvariant gdw. für alle Abläufe # mit # ! gilt:Wenn #$ auf den Systemvariablen mit # übereinstimmt, dann gilt #$ !.
Nicht notwendigerweise!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
19
Diplom-verteidigung
Formale Fundierung
Eigenschaften von TS! (! umgebungs-invariant):
! Für alle Abläufe von !, für jeden Schnitt C, der mit Schritten erreichbar ist, existiert ein erreichbarer entsprechender Zustand sC in TS!.
! Für alle erreichbaren Zustände sC in TS!
existiert ein Ablauf von ! mit einem entsprechenden Schnitt C, der mit Schritten erreichbar ist.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
19
Diplom-verteidigung
Formale Fundierung
Eigenschaften von TS! (! umgebungs-invariant):
! Für alle Abläufe von !, für jeden Schnitt C, der mit Schritten erreichbar ist, existiert ein erreichbarer entsprechender Zustand sC in TS!.
! Für alle erreichbaren Zustände sC in TS!
existiert ein Ablauf von ! mit einem entsprechenden Schnitt C, der mit Schritten erreichbar ist.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
19
Diplom-verteidigung
Formale Fundierung
Eigenschaften von TS! (! umgebungs-invariant):
! Für alle Abläufe von !, für jeden Schnitt C, der mit Schritten erreichbar ist, existiert ein erreichbarer entsprechender Zustand sC in TS!.
! Für alle erreichbaren Zustände sC in TS!
existiert ein Ablauf von ! mit einem entsprechenden Schnitt C, der mit Schritten erreichbar ist.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
20
Diplom-verteidigung
Formale Fundierung
Eigenschaften von TS! (! umgebungs-invariant):
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
20
Diplom-verteidigung
Formale Fundierung
Eigenschaften von TS! (! umgebungs-invariant):
1. Jeder Schnitt entspricht einem Zustand.
2. Jeder Ablauf entspricht Interleavings.
3. Jeder Zustand entspricht einem Schnitt.
4. Jedes Interleaving entspricht einem Ablauf.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
20
Diplom-verteidigung
Formale Fundierung
Eigenschaften von TS! (! umgebungs-invariant):
1. Jeder Schnitt entspricht einem Zustand.
2. Jeder Ablauf entspricht Interleavings.
3. Jeder Zustand entspricht einem Schnitt.
4. Jedes Interleaving entspricht einem Ablauf.
Die Interleavings von ! sind Pfade in TS!.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
20
Diplom-verteidigung
Formale Fundierung
Eigenschaften von TS! (! umgebungs-invariant):
1. Jeder Schnitt entspricht einem Zustand.
2. Jeder Ablauf entspricht Interleavings.
3. Jeder Zustand entspricht einem Schnitt.
4. Jedes Interleaving entspricht einem Ablauf.
Die Interleavings von ! sind Pfade in TS!.
% TS! ist eine TLDA-Interleavingsemantik.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
21
Diplom-verteidigung
Formale Fundierung
! Zusammenhangzwischen Abläufenund Interleavings
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
rp rd
rc
1 0
…
…
…
21
Diplom-verteidigung
Formale Fundierung
! Zusammenhangzwischen Abläufenund Interleavings
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
rp rd
rc
1 0
…
…
…
C0
21
Diplom-verteidigung
Formale Fundierung
! Zusammenhangzwischen Abläufenund Interleavings
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
rp rd
rc
1 0
…
…
…
C0
21
Diplom-verteidigung
Formale Fundierung
! Zusammenhangzwischen Abläufenund Interleavings
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
rp rd
rc
1 0
…
…
…
C0 C1
21
Diplom-verteidigung
Formale Fundierung
! Zusammenhangzwischen Abläufenund Interleavings
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
rp rd
rc
1 0
…
…
…
C0 C1 C2
21
Diplom-verteidigung
Formale Fundierung
! Zusammenhangzwischen Abläufenund Interleavings
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
rp rd
rc
1 0
…
…
…
C0 C1 C2 C3
21
Diplom-verteidigung
Formale Fundierung
! Zusammenhangzwischen Abläufenund Interleavings
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
rp
0
rr
rd
§
rp rd
rc
1 0
…
…
…
C0 C1 C2 C3
Produce
Deliver&Filling
Remove&Emptying
22
Diplom-verteidigung
Formale Fundierung
! Transitionssystemerlaubt explizitesModelchecking.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
22
Diplom-verteidigung
Formale Fundierung
! Transitionssystemerlaubt explizitesModelchecking.
! Ziel weiterer Arbeit:Entwicklung vonModelchecking-Algorithmen
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
22
Diplom-verteidigung
Formale Fundierung
! Transitionssystemerlaubt explizitesModelchecking.
! Ziel weiterer Arbeit:Entwicklung vonModelchecking-Algorithmen
! Beispiel: Gilt die Formel ?
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
23
Diplom-verteidigung
E!zientere Algorithmen
! Problem: Klauselanzahl der DNF kann exponentiell steigen!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
23
Diplom-verteidigung
E!zientere Algorithmen
! Problem: Klauselanzahl der DNF kann exponentiell steigen!
! Meist sind mehr als 99 % der Klauseln widersprüchlich!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
23
Diplom-verteidigung
E!zientere Algorithmen
! Problem: Klauselanzahl der DNF kann exponentiell steigen!
! Meist sind mehr als 99 % der Klauseln widersprüchlich!
! Beispiel: Die DNF des Produzenten-/Konsumentensystemes besteht aus 16875 Klauseln, von denen jedoch nur 26 für das Transitionssystem wesentlich sind.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
24
Diplom-verteidigung
E!zientere Algorithmen
! Die disjunktive Normalform muss nicht vollständig gebildet werden!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
24
Diplom-verteidigung
E!zientere Algorithmen
! Die disjunktive Normalform muss nicht vollständig gebildet werden!
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
24
Diplom-verteidigung
E!zientere Algorithmen
! Die disjunktive Normalform muss nicht vollständig gebildet werden!
! kompositionaler Aufbau von Spezifikationen:
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
24
Diplom-verteidigung
E!zientere Algorithmen
! Die disjunktive Normalform muss nicht vollständig gebildet werden!
! kompositionaler Aufbau von Spezifikationen:
! Idee: nur DNF der Komponenten bilden
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
25
Diplom-verteidigung
E!zientere Implementierung
25
Diplom-verteidigung
E!zientere Implementierung
Klausel
25
Diplom-verteidigung
E!zientere Implementierung
Klausel Komponente
25
Diplom-verteidigung
E!zientere Implementierung
Klausel KomponenteStartknoten Endknoten
25
Diplom-verteidigung
E!zientere Implementierung
! DNF-Graph
! Pfade entsprechen Klauseln der Gesamtspezifikation
25
Diplom-verteidigung
E!zientere Implementierung
! DNF-Graph
! Pfade entsprechen Klauseln der Gesamtspezifikation
26
Diplom-verteidigung
E!zientere Algorithmen
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
……
Klauseln der Komponente i Klauseln der Komponente i+1
26
Diplom-verteidigung
E!zientere Algorithmen
! Beschriebener Pfad ist widersprüchlich
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
……
Klauseln der Komponente i Klauseln der Komponente i+1
26
Diplom-verteidigung
E!zientere Algorithmen
! Beschriebener Pfad ist widersprüchlich
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
……
Klauseln der Komponente i Klauseln der Komponente i+1
26
Diplom-verteidigung
E!zientere Algorithmen
! Beschriebener Pfad ist widersprüchlich
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
……
Klauseln der Komponente i Klauseln der Komponente i+1
27
Diplom-verteidigung
E!zientere Algorithmen
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
27
Diplom-verteidigung
E!zientere Algorithmen
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
! On-the-fly-Verfahren:
1. Widerspruch erkannt
2. Klausel austauschen
3. Pfad fortsetzen
28
Diplom-verteidigung
E!zientere Algorithmen
! On-the-fly-Verfahren:! Berechnung kann früher abgebrochen
werden! nicht alle Klauseln müssen betrachtet
werden! weniger Speicherplatz notwendig
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
28
Diplom-verteidigung
E!zientere Algorithmen
! On-the-fly-Verfahren:! Berechnung kann früher abgebrochen
werden! nicht alle Klauseln müssen betrachtet
werden! weniger Speicherplatz notwendig
! Beispiel:! Nur 1407 von 16875 Klauseln müssen
analysiert werden.! DNF-Graph hat nur 30 Knoten.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
29
Diplom-verteidigung
E!zientere Algorithmen
! ~-Variablen sind oft Grund für Widersprüchlichkeit
! kann oft nicht rein syntaktisch erkannt werden:
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
29
Diplom-verteidigung
E!zientere Algorithmen
! ~-Variablen sind oft Grund für Widersprüchlichkeit
! kann oft nicht rein syntaktisch erkannt werden:
! Regeln, um Informationen zu gewinnen:1. Zerlegung:
2. Transitivität:3. Erweiterung:
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
29
Diplom-verteidigung
E!zientere Algorithmen
! ~-Variablen sind oft Grund für Widersprüchlichkeit
! kann oft nicht rein syntaktisch erkannt werden:
! Regeln, um Informationen zu gewinnen:1. Zerlegung:
2. Transitivität:3. Erweiterung:
! Regeln basieren auf Mengenbeziehungen
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
30
Diplom-verteidigung
E!zientere Algorithmen
w x y z
wx wy wz xy xz
wxy wxz wyz xyz
wxyz
yz
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
30
Diplom-verteidigung
E!zientere Algorithmen
! ~-Graph
w x y z
wx wy wz xy xz
wxy wxz wyz xyz
wxyz
yz
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
30
Diplom-verteidigung
E!zientere Algorithmen
! ~-Graph
! jeder Knoten entspricht einer ~-Variable
w x y z
wx wy wz xy xz
wxy wxz wyz xyz
wxyz
yz
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
30
Diplom-verteidigung
E!zientere Algorithmen
! ~-Graph
! jeder Knoten entspricht einer ~-Variable
! Kanten entsprechen Mengenbeziehungen
w x y z
wx wy wz xy xz
wxy wxz wyz xyz
wxyz
yz
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
31
Diplom-verteidigung
E!zientere Algorithmen
! Informationsgewinnung:! Gegeben:
w x y z
wx wy wz xy xz
wxy wxz wyz xyz
wxyz
yzKonsumenten-/
Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
31
Diplom-verteidigung
E!zientere Algorithmen
! Informationsgewinnung:! Gegeben:
! Berechnet:
w x y z
wx wy wz xy xz
wxy wxz wyz xyz
wxyz
yzKonsumenten-/
Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
32
Diplom-verteidigung
E!zientere Algorithmen
! Erkennung von Widersprüchen:! Gegeben:
w x y z
wx wy wz xy xz
wxy wxz wyz xyz
wxyz
yzKonsumenten-/
Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
32
Diplom-verteidigung
E!zientere Algorithmen
! Erkennung von Widersprüchen:! Gegeben:
! Berechnet:
w x y z
wx wy wz xy xz
wxy wxz wyz xyz
wxyz
yzKonsumenten-/
Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
32
Diplom-verteidigung
E!zientere Algorithmen
! Erkennung von Widersprüchen:! Gegeben:
! Berechnet:
w x y z
wx wy wz xy xz
wxy wxz wyz xyz
wxyz
yz
wyz
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
32
Diplom-verteidigung
E!zientere Algorithmen
! Erkennung von Widersprüchen:! Gegeben:
! Berechnet:
w x y z
wx wy wz xy xz
wxy wxz wyz xyz
wxyz
yz
wyz
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
Widerspruch!
33
Diplom-verteidigung
E!zientere Algorithmen
! Minimale Repräsentation
! Repräsentanten:
w x y z
wx wy wz xy xz
wxy wxz wyz xyz
wxyz
yzKonsumenten-/
Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
34
Diplom-verteidigung
E!zientere Algorithmen
! ~-Graph:! e!zientes Verfahren zur Erkennung von
Widersprüchen! Datenstruktur zur minimalen
Repräsentation von Informationen Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
34
Diplom-verteidigung
E!zientere Algorithmen
! ~-Graph:! e!zientes Verfahren zur Erkennung von
Widersprüchen! Datenstruktur zur minimalen
Repräsentation von Informationen
! Beispiel:! Beim Konsumenten-/Produzentensystem
konnten so alleine 577 widersprüchliche Klauseln entdeckt werden.
! Minimale Repräsentation spart 57 % Speicherplatz.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
35
Diplom-verteidigung
Ausblick
! Für kleine Beispiele sind die entwickelten Algorithmen sehr e!zient.
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
35
Diplom-verteidigung
Ausblick
! Für kleine Beispiele sind die entwickelten Algorithmen sehr e!zient.
! Komplexität der DNF wurde nicht verringert Konsumenten-/
Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
35
Diplom-verteidigung
Ausblick
! Für kleine Beispiele sind die entwickelten Algorithmen sehr e!zient.
! Komplexität der DNF wurde nicht verringert
! Anzahl der ~-Variablen steigt ebenfalls exponentiell
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
35
Diplom-verteidigung
Ausblick
! Für kleine Beispiele sind die entwickelten Algorithmen sehr e!zient.
! Komplexität der DNF wurde nicht verringert
! Anzahl der ~-Variablen steigt ebenfalls exponentiell
! Analyse der Aktionen (Preprocessing!) kann Stunden dauern
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
36
Diplom-verteidigung
Ausblick
! alternative Spezifikationsmöglichkeiten! Aktionen direkt angeben
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
36
Diplom-verteidigung
Ausblick
! alternative Spezifikationsmöglichkeiten! Aktionen direkt angeben
! alternativen Verifikationsmöglichkeiten:! symbolisches Modelchecking (SAT)! Theorembeweiser
Konsumenten-/Produzentensystem
Einführungin TLDA
Semantiken
Transitionssystem
FormaleFundierung
Effizientere Implementierung
Ausblick
01/04/11
Formale Fundierung und e!zientere Implementierung der schrittbasierten TLDA-
Interleavingsemantik
Vielen Dank!
Niels Lohmann
nlohmann@informatik.hu-berlin.dehttp://www.informatik.hu-berlin.de/~nlohmann/studium