Communicating Sequential Processes
Communicating Sequential Processes (CSP) ist eine von Tony Hoare an der Universität Oxford entwickelte Sprache zur Beschreibung von Interaktion zwischen kommunizierenden Prozessen. Die Idee wurde 1978 von Tony Hoare erstmals beschrieben, 1985 mit der Veröffentlichung des Buchs mit dem gleichnamigen Titel Communicating Sequential Processes berühmt und war 2003 nach CiteSeer bereits das dritthäufigst zitierte Buch der Informatik.
Anwendungen
Die Programmiersprache Occam ist eine praktische Implementierung der CSP. JCSP ist die Verbindung von CSP und Occam-Konzepten in einer Java-API. Weitere Anwendungen sind das Message Passing Interface sowie die Parallel Virtual Machine.
- CSP verwendet Großbuchstaben für Zustände des Automaten sowie Kleinbuchstaben für Ereignisse. Die durch Ereignisse ausgelösten Zustandsübergänge werden durch einen Pfeil (->) gekennzeichnet.
(x -> B) Auf das Ereignis x folgt der Zustand B (x -> y -> B) Auf die Ereignisfolge x und dann y folgt Zustand B
- In CSP werden bedingte Ereignisse durch Angabe des Auswahloperators | definiert.
(x -> A | y -> B) Wenn Ereignis x, dann Zustand A. Wenn Ereignis y, dann Zustand B
- Die Menge der Zustände und Ereignisse, die ein über CSP definierter Automat akzeptiert wird durch das Alphabet αP angegeben. Jeder Automat beinhaltet einen zusätzlichen Zustand STOP in αP, aus dem ein weiterer Zustandsübergang per Definition nicht mehr erlaubt ist.
- Sequentielle Komposition wird durch das Einführen von Zwischenzuständen ermöglicht
P = (x -> A), A = (y -> B) ist äquivalent zu P = (x -> y -> B)
- Die Parallelschaltung von Prozessen, die dieser Prozessalgebra den Namen gab, wird durch die Angabe des Symbols || erreicht.
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}
P || Q akzeptiert alle Zeichenfolgen {ab, axb, yb} sowie beliebige sequentielle Kombinationen
- Rekursionen sind möglich
P = (x -> y -> P) generiert die unendliche Abfolge der Ereignisse xyxyxy...