Spezifikation nebenläufiger Programme

• Prozeßkalküle oder Prozeßalgebren: CSP, CCS, π-Kalkül

• Primäre Operation: Kommunikation

• Beschreibt ablauffähige Prozesse (vgl. Modallogik, temporale Logik, TLA: Spezifikation)

C. Lüth  Korrekte Software durch Formale Methoden  55

CSP: Syntax Gegeben Prozeßalphabet Σ, besondere Ereignisse ✓, τ

P ::= Stop | a → P | μ P.F(P) fundamentale Operationen | ?x : A → P(x)  Präfixauswahl (A ⊆ Σ) | P □Q | P ⊓ Q  externe und interne Auswahl | P ∥ Q | P ∥_{X} Q | P _{X}∥_{Y} Q synchronisiert parallel | P ||| Q  unsynchronisiert parallel | P \ X | f [P]  hiding, Umbenennung (f injektiv) | Skip | P; Q  sequentielle Komposition, Iteration

CSP: Beispiele

• Einfacher Schokoladenautomat: μ P.1p → choc → P

• Schokoladenautomat mit Auswahl: P = 1p → choc → P | 2p → toffee → P

• Pufferprozess:

COPY = left ?x → right !x → COPY

NB. Eingabe (c?x) und Ausgabe (c!x) sind reine Konvention.

C. Lüth  Korrekte Software durch Formale Methoden  57

CSP: Beispiele II

• Bankautomat:

ATM = in?c : CARD → pin.f_{pin}(c) → req ?n : WA → ((dispense .n → out .cATM ) ⊓ (refuse → (ATM ⊓ out .c → ATM )))

• Pantomimenpferd (fehlerhaft):

HORSE = Front _{F}∥_{B} back
F = {forward , backward , nod , neigh }
B = {forward , backward , wag , kick }
Front = forward → Front ′ □ nod → Front
Back = backward → Back ′ □ wag → Back
C. Lüth  Korrekte Software durch Formale Methoden  58

Operationale Semantik für CSP (I)

Defn: Ein labelled transition system (LTS) ist L = (N, A, →) mit Menge N der Knoten (Zustände), Menge A von Labels und Relation {→^{a} ⊆ N × N}_{a∈A} von Kanten (Zustandsübergänge).

Hier N = P,A = Σ ∪ {✓, τ}, → definiert wie folgt (NB. Keine Regel für Stop ):

e → P →^{a} P[a/e] a ∈ comms(e)
P ⊓ Q →^{τ} P  P ⊓ Q →^{τ} Q

Skip →^{✓} Ω

C. Lüth  Korrekte Software durch Formale Methoden  59

Operationale Semantik für CSP (II)

{P →^{τ} P′ \atop P □ Q →^{τ} P′ □ Q}  {Q →^{τ} Q′ \atop P □ Q →^{τ} P □ Q′}

{P →^{a} P′ \atop P □ Q →^{a} P′} a ≠ τ  {Q →^{a} Q′ \atop P □ Q →^{a} Q′} a ≠ τ

P →^{x} P′ P; Q →^{x} P′; Q x ≠ ✓ {∃ P′. P →^{✓} P′ \atop P; Q →^{τ} Q}

{P →^{✓} P′ \atop P \ B →^{✓} Ω}  {P →^{x} P′ \atop P \ B →^{τ} P′} x ∈ B P →^{x} P′ P \ B →^{x} P′ \ B x ∉ B ∪ \{✓\}

C. Lüth  Korrekte Software durch Formale Methoden  60

Operationale Semantik für CSP (III)

P →^{τ} P′

P ∥_{X} Q →^{τ} P′ ∥_{X} Q

Q →^{τ} Q′

P ∥_{X} Q →^{τ} P ∥_{X} Q′

P →^{a} P′ P ∥_{X} Q →^{a} P′ ∥_{X} Q a ∉ X Q →^{a} Q′ P ∥_{X} Q →^{a} P ∥_{X} Q′ a ∉ X

P →^{a} P′ Q →^{a} Q′

P ∥_{X} Q →^{a} P′ ∥_{X} Q′

a ∈ X

P →^{✓} P′

P ∥_{X} Q →^{τ} Ω ∥_{X} Q

Q →^{✓} Q′

P ∥_{X} Q →^{τ} P ∥_{X} Ω

Ω ∥_{X} Ω →^{✓} Ω

C. Lüth  Korrekte Software durch Formale Methoden  61

Ziele der Semantik von Prozesskalkülen

• Reasoning about processes by their external behaviour

• Untersuchung von – Verfeinerung (Implementation)

– deadlock: Keine Transition möglich

– livelock: Divergenz

• Grundlegender Begriff: Äquivalenz (Gleichheit) von Prozessen

C. Lüth  Korrekte Software durch Formale Methoden  62

Äquivalenz für LTS: Bisimulation Defn: Für LTS L = (N, A, →), eine Bisimulation ist eine Relation R ⊆ N × N auf den Knoten so daß

(i) wenn n_{1} R n_{2} und n_{1} →^{x} m_{1} (x ∈ Σ^{τ,✓}), dann gibt es m_{2} so daß n_{2} →^{x} m_{2} und m_{1} R m_{2}

(ii) wenn n_{1} R n_{2} und n_{2} →^{x} m_{2} (x ∈ Σ^{τ,✓}),

dann gibt es m_{1} so daß n_{1} →^{x} m_{1} und m_{1} R m_{2} Bisimularität: externe Ununterscheidbarkeit Allerdings: CSP primär über denotationelle Semantik definiert

C. Lüth  Korrekte Software durch Formale Methoden  63

Denotationelle Semantik für CSP I: Das Pfad-Modell Pfade: Σ^{∗✓} =^{def} Σ^{∗} ∪ {s ˆ ⟨✓⟩ | s ∈ Σ^{∗}}

traces (Stop ) = ⟨⟩
traces (a → P) = {⟨⟩} ∪ {⟨a⟩ˆ s | s ∈ traces (P)}
traces (P □ Q) = traces (P) ∪ traces (Q)
traces (P ⊓ Q) = traces (P) ∪ traces (Q)
traces (P \ B) = {s ↾ Σ \ B | s ∈ traces (P)}
traces (Skip ) = {⟨⟩, ⟨✓⟩}
traces (P; Q) = (traces (P) ∩ Σ^{∗})∪

{s ˆ t | s ˆ ⟨✓⟩ ∈ traces (P), t ∈ traces (Q) }

traces (P ∥_{X} Q) = ⋃{s ∥_{X} t | s ∈ traces (P), t ∈ traces (Q) }
C. Lüth  Korrekte Software durch Formale Methoden  64

Denotationelle Semantik für CSP I: Das Pfad-Modell Für x ∈ X, y ∈ Σ \ X:

⟨⟩ ∥_{X} ⟨⟩ = ⟨⟩ ⟨⟩ ∥_{X} ⟨x⟩ = ⟨⟩ ⟨⟩ ∥_{X} ⟨y⟩ = ⟨y⟩
⟨x⟩ˆ s ∥_{X} ⟨y⟩ˆ t = {⟨y⟩ˆ u | u ∈ ⟨x⟩ˆ s ∥_{X} t }
⟨x⟩ˆ s ∥_{X} ⟨x⟩ˆ t = {⟨x⟩ˆ u | u ∈ s ∥_{X} t }
⟨x⟩ˆ s ∥_{X} ⟨x′⟩ˆ t = ∅ x ≠ x′
⟨y⟩ˆ s ∥_{X} ⟨y′⟩ˆ t = {⟨y⟩ˆ u | u ∈ s ∥_{X} ⟨y′⟩ˆ t } ∪ {⟨y′⟩ˆ u | u ∈ ⟨y⟩ˆ s ∥_{X} t }
s ∥_{X} tˆ ⟨✓⟩ = ∅
s ˆ ⟨✓⟩ ∥_{X} tˆ ⟨✓⟩ = {uˆ ⟨✓⟩ | u ∈ s ∥_{X} t }
C. Lüth  Korrekte Software durch Formale Methoden  65

Denotationelle Semantik für CSP I: Das Pfad-Modell

• Für Rekursion: vollständige Ordnung auf Pfaden

P ⊑ Q =^{def} P ⊆ Q, ⊥ =^{def} {⟨⟩}

traces (μ P.F(P)) = fix(F) = ⋃_{i<ω} F^{i}({⟨⟩})

Operatoren stetig und monoton. (Nicht der Fall für Präfixordnung ⊑_{T} .)

• Probleme des Pfad-Modells:

– Keine Unterscheidung von interner und externer Auswahl.

– Keine Unterscheidung von deadlocks.

C. Lüth  Korrekte Software durch Formale Methoden  66

Denotationelle Semantik für CSP II: Failure/Divergence

• Pfade beschreiben mögliche Aktionen, F/D beschreiben auch erzwungene Aktionen.

• Divergenz: Menge von Pfaden, ab denen der Prozess divergieren kann (unendliche Sequenz von τ).

• Failures: (s, X) wobei s ein Pfad des Prozesses ist und X eine Menge von verweigerten Aktionen (refusals) in einem stabilen Zustand nach s oder nach s kann ✓ auftreten (dann X ⊆ Σ) oder Prozess divergiert nach s.

• Stabiler Zustand: kein τ oder ✓ möglich.

Denotationelle Semantik für CSP II: Failure/Divergence Modell N N gegeben durch P = (F, D) mit F ⊆ Σ^{∗✓} × ℙ(Σ^{✓}), D ⊆ Σ^{∗✓} so daß

F1 traces (P) = {t | (t, X) ∈ F } ist nichtleer und präfixgeschlossen.
F2 (s, X) ∈ F ∧ Y ⊆ X ⇒ (s, Y ) ∈ F
F3 (s, X) ∈ F ∧ ∀ a ∈ Y . s ˆ ⟨a⟩ ∉ traces (P) ⇒ (s, X ∪ Y ) ∈ F
F4 s ˆ ⟨✓⟩ ∈ traces (P) ⇒ (s, Σ) ∈ F
D1 s ∈ D ∩ Σ^{∗} ∧ t ∈ Σ^{∗✓} ⇒ s ˆ t ∈ D
D2 s ∈ D ⇒ (s, X) ∈ F
D3 s ˆ ⟨✓⟩ ∈ D ⇒ s ∈ D
C. Lüth  Korrekte Software durch Formale Methoden  68

Denotationelle Semantik für CSP II: Eigenschaften von N Verfeinerung: (F, D) ⊑_{FD} (F′, D′) gdw F ⊇ F′, D ⊇ D′ Theorem: Für endliches Σ, N ist cpo mit ⊑_{FD} und

⊥_{N} = (Σ^{∗✓} × ℙ(Σ^{∗✓}), Σ^{∗✓})

⨆_{i}(F_{i}, D_{i}) = (⋂_{i}F_{i}, ⋂ D_{i})

Deadlockfreiheit: ∀ s. (s, Σ) ∉ failures (P) (P kann nie alles verweigern)

C. Lüth  Korrekte Software durch Formale Methoden  69

failures (Stop ) = {(⟨⟩, X) | X ⊆ Σ^{✓}} divergences (Stop ) = ∅ failures (a → P) = {(⟨⟩, X) | a ∉ X } ∪ {(⟨a⟩ˆ s, X) | (s, X) ∈ failures (s) } divergences (a → P) = {(⟨a⟩ˆ s, X) | s ∈ divergences (P)} failures (P ⊓ Q) = failures (P) ∪ failures (Q) divergences (P ⊓ Q) = divergences (P) ∪ divergences (Q) failures (P □ Q) = {(⟨⟩, X) | (⟨⟩, X) ∈ failures (P) ∩ failures (Q) } ∪{(s, X) | (s, X) ∈ failures (P) ∪ failures (Q) ∧ s ≠ ⟨⟩ } ∪{(⟨⟩, X) | ⟨⟩ ∈ divergences (P) ∪ divergences (Q) } ∪{(⟨⟩, X) | X ⊆ Σ ∧ ⟨✓⟩ ∈ traces (P) ∪ traces (Q) }

divergences (P □ Q) = divergences (P) ∪ divergences (Q)

failures (P ∥_{X} Q) = \{ \begin{matrix}(u, Y ∪ Z) | Y \ (X ∪ \{✓\}) = Z \ (X ∪ \{✓\}) \\ ∧ ∃ s, t.(s, Y ) ∈ failures (P) ∧ (t, Z) ∈ failures (Q) \\ ∧u ∈ s ∥_{X} t\} \end{matrix}

∪{(u, Y ) | u ∈ divergences (P ∥_{X} Q) }
divergences (P ∥_{X} Q) = \{ \begin{matrix}uˆ v | ∃ s ∈ traces (P), t ∈ traces (Q). \\ u ∈ (s ∥_{X} t) ∩ Σ^{∗} \\ ∧(s ∈ divergences (P) ∨ t ∈ divergences (Q))\} \end{matrix}

failures (P \ X) = {(s \ X, Y ) | (s, Y ∪ X) ∈ failures (Y ) }

∪{(s, X) | s ∈ divergences (P \ X) }

divergences (P \ X) = {(s \ X)ˆ t | s ∈ divergences (P)}

∪\{(u \ X)ˆ t | \begin{matrix}u ∈ Σ^{ω} ∧ (u \ X)finite \\ ∧ ∀ s < u.s ∈ traces (P)\} \end{matrix}

failures (P; Q) = {(s, X) | s ∈ Σ^{∗} ∧ (s, X ∪ {✓}) ∈ failures (P) }

∪{(s ˆ t, X) | s ˆ ⟨✓⟩ ∈ traces (P) ∧ (t, X) ∈ failures (Q) } ∪{(s, X) | s ∈ divergences (P; Q) }

divergences (P; Q) = divergences (P)∪

{s ˆ t | s ˆ ⟨✓⟩ ∈ traces (P) ∧ t ∈ divergences (Q) } Lemma: Für endliches Σ, alle Operatoren sind stetig. ⇒ Existenz von Fixpunkten. Nachteile: Endlichkeit des Alphabets, Divergenzmengen kostspielig zu berechnen aber meistens nicht nötig. Nachteile können behoben werden durch stable failures model F.

C. Lüth  Korrekte Software durch Formale Methoden  73

Tools für CSP

• FDR2 (Formal Systems Europe Ltd.): – model-checker: für Prozesse mit endlich vielen Zuständen;

– automatische Prüfung auf refinement (T, F, FD), deadlock, livelock; Debugging, Auswertung.

• HOL-CSP (Uni Bremen):

– Kodierung von FD-Semantik in Isabelle

– Interaktives Beweis beliebiger Aussagen über Prozesse mit un-

endlichen Zuständen, beliebigen Alphabeten etc.

C. Lüth  Korrekte Software durch Formale Methoden  74

Arbeiten mit FDR2