Communicating Sequential Processes

CSP ist eine von Prof. Sir Tony Hoare an der Universität Oxford entwickelte Prozessalgebra zur mathematischen Beschreibung kommunizierender Automaten. Die zentrale Idee ist eine Entwurfsmethodik, die es erlaubt, systematisch komplexe Systeme aus kleineren zu konstruieren.

Syntax und Semantik:

• In CSP werden Zustände mit Großbuchstaben, Ereignisse mit Kleinbuchstaben ausgedrückt.

• Transitionen werden durch einen Pfeil -> gekennzeichnet. So bedeutet (x -> B), gesprochen "x, dann B", dass der Automat nach dem Ereignis x im Zustand B ankommt. Gleichermaßen meint (x -> y -> B) den Übergang in den Zustand B, nachdem die Ereignisse x und dann y eingetreten sind.

• Einfache sequentielle Komposition ist durch das Einführen von Zwischenzuständen möglich: P = (x -> A), A = (y -> B) akzeptiert also die gleiche Ereignisfolge wie P = (x -> y -> B)

• Der Auswahloperator | erlaubt das Schalten in verschiedene Zustände, abhängig vom aufgetretenen Ereignis: P = (x -> A | y -> B) schaltet z.B. bei x in den Zustand A, bei y in den Zustand B.

• Auch Rekursionen sind möglich: P = (x -> y -> P) lässt z.B. eine unendliche Abfolge xyxyxy... von Ereignissen zu.

• Jedem Prozess P ist ein Alphabet αP zugeordnet, das angibt, auf welche Signale der Prozess P reagiert.

• Ein Sonderzustand ist der Zustand STOP/αP, aus dem der Automat mit Alphabet αP nicht wieder herauswechseln kann.

Automaten können mittels des Zeichens || parallel geschaltet werden, wobei zu beachten ist, dass der Produktautomat nur dann auf Ereignisse aus dem gemeinsamen Alphabet reagieren kann, wenn sich beide Teilautomaten in einem Zustand befinden, aus dem dieses Ereignis führt.

Ein Beispiel:

• P = (a -> (b -> P | x -> P) | (b -> P)) mit αP = {a, b, x}

• Q = (a -> b -> Q | y -> b -> Q) mit αQ = {a, b, y}

• Dann akzeptiert P || Q die Zeichenfolgen {ab, axb, yb} sowie alle Kombinationen (abab..., ababx...) daraus.