\begin{slide}{Communicating Sequential Processes}

abstraktes Modell für Kommunikation von Prozessen

C. A. R. Hoare 1978, Grundlage für
Prozeßmodell in Occam, Ada, Go, \ldots

\end{slide}

\begin{slide}{CSP-Definition}
Syntax (Beispiel):
\begin{itemize}\itemsep 0pt
\item $\text{STOP}$,  \quad $e \to P$ mit $e$ Ereignis, $P$ Prozeß
\item Nacheinander: $P_1 ; P_2$, \quad Auswahl: $P_1 \Box P_2$
\item unabhängig, verschränkt $P_1 \|| P_2$ (shuffle)
\item parallel, synchronisiert $P_1 \|_E P_2$ 
  mit $E$ Menge von Ereignissen
\end{itemize}
Semantik: Beschreibung der möglichen Transitionen:
\begin{itemize} \itemsep 0pt
\item $(a \to P) \stackrel{a}{\to} P$
\item wenn $P  \stackrel{a}{\to} P'$, dann $(P \Box Q)   \stackrel{a}{\to} P'$
\item wenn $Q  \stackrel{b}{\to} Q'$, dann $(P \Box Q)   \stackrel{b}{\to} Q'$
\end{itemize}


\end{slide}
