Semantik von UML Sequenzdiagrammen

Christopher Lie (227249)

Betreuer: Dr. Erika Abraham

Gliederung

Einleitung Grundlagen Semantik von UML Sequenzdiagrammen Refinement Zusammenfassung

Einleitung

Wir formulieren die Semantik von UML Sequenzdiagrammen mit Hilfe von Büchi Automaten.

Wir zeigen die Kompositionalität der Verfeinerung.

Gliederung

Einleitung Grundlagen Semantik von UML Sequenzdiagrammen Refinement Zusammenfassung

Grundlagen

NFA Hi-level NFA Büchi Automat Safety Eigenschaft Liveness Eigenschaft

NFA

NFA = Nichtdeterministischer endlicher Automat

‹Σ,S,δ,S0,F› - 5 Tupel Σ : Eingabealphabet S : Zustandsmenge δ : S × Σ × S : Übergangsrelation S0 ⊆ S : Startzustände F ⊆ S : EndzuständeAkzeptiert endliche Wörter.

High-level NFA

Ein Hi-Level NFA ist ein NFA, dessen Zustände Basic-NFAs oder andere nicht rekursive Hi-Level NFAs sind.

Transitionen von Hi-Level NFAs werden mit ℇ beschriftet.

Büchi Automat

Ein Büchi Automat ist ein endlicher Automat der unendliche Wörter akzeptiert.

Akzeptanzbedingung:Unendlich viele Endzustände besuchen

Safety Eigenschaft P P ist eine Eigenschaft, die besagt, dass etwas

Schlechtes nicht passiert.

∀α∈Σωτ.α⊨P ↔ ∀i >0. ∃β∈ Σω

τ. α[1..i]β ⊨P

Liveness Eigenschaft PP ist eine Eigenschaft, die besagt, dass

irgendwann etwas Gutes passiert.

∀α∈Σ*τ. ∃β ∈ Σω

τ. αβ ⊨P

Gliederung

Einleitung Grundlagen Semantik von UML Sequenzdiagrammen Refinement Zusammenfassung

Semantik v. UML Sequenzdiagrammen

High SD

High NFA

Positive NFA Negative NFA

„Liveness“ Büchi „Safety“ Büchi

xSemantik

Sequenzdiagramme

Partielle Ordnung →NFA

Partielle Ordnung →NFA

Sei P := Potenzmenge der Aktionen A, Dann definiert man

P' := {p ∈ P|∀i, j. i ∈ P ∧ j < i ⇒ j ∈ P}. Schließlich definieren wir die Transitionen:

T := {t ∈ P' × A × P' |

b = a ∪ {e} ∧ t = (a, l(e), b) }. Endzustand ist A.

High SD zu High NFA

Negativer & positiver NFA

Negativer NFA Positiver NFA

Flattening vom negativen NFA

Flattening vom positiven NFA

Negativer NFA → Safety Büchi

N = Negativer Büchi Automat Sei B = ¬N Reduziere B Mache alle Zustände akzeptierend→Safe(B)

Negativer NFA → Safety Büchi

Positiver NFA → Liveness Büchi

P = Positiver Automat NFA P → Büchi Automat A Reduziere A Live(A) = A ∪ ¬Safe(A)

Positiver NFA → Liveness Büchi

Semantik von SD

Definition:

Sei S SD, Sl = Live(pos(S)), Ss = Safe(¬neg(S)) dann

L(S) = L(Sl × Ss).

Theorem: L(S) = L(Sl) ∩ L(Ss)

Gliederung

Einleitung Grundlagen Semantik von Sequenzdiagrammen Refinement Zusammenfassung

Refinement Definition :

Seien S1 und S2 Sequenzdiagramme.

S1 verfeinert S2 wenn L(S1) ⊆ L(S2) Satz :

Seien S1 und S2 Sequenzdiagramme. Für i = 1,2 seien Pi = pos(Si) und Ni = neg(Si).

Dann S1≼S2 wenn gilt:L(N2) ⊆ L(N1) undRej(L(P2)) ⊆ Rej(L(P1)), wobei

Rej(L(A)) = Safe(L(A)) – L(A)

Refinement

SD1SD2 SD≼ 1

SD2SD3 SD≼ 2 ⇒ SD1(SD2SD3) SD≼ 1(SD2)

Refinement Korollar :

Sei S,T,U Sequenzdiagramm, L(pos(S)) ∩ Rej(L(pos(T))) = L(pos(T)) ∩ Rej(L(pos(S))) = Ø, dannSU S≼ ; S+ S; S+T S und S≼ ≼ +T T; ≼

S||T S und S||T T.≼ ≼T U ST SU≼ ⇒ ≼ ; S T (S)* (T)*;≼ ⇒ ≼

T U S+T S+U und T+S U+S;≼ ⇒ ≼ ≼T U S||T S||U und T||S U||S. ≼ ⇒ ≼ ≼

Gliederung

Einleitung Grundlagen Semantik von Sequenzdiagrammen Refinement Zusammenfassung

Zusammenfassung

Wir haben die Semantik von SDs mit Hilfe von Safety und Lifeness Eigenschaften bestimmt.

Wenn man ein SD verfeinert, dann verfeinert man auch dessen Semantik.

Refinement

NFA → Büchi Automat