\chapter{Le problème de l'ingénierie des protocoles}

\section{Intention}
Établir une communication {\em fiable} entre deux processus. L'un est généralement appelé le producteur, et l'autre le consommateur. Une solution consiste à contruire une couche de communication comprenant un processus émetteur (dans lequel le producteur dépose ses messages) et un processus récepteur (duquel le consommateur reçoit les messages) reliés par un réseau.

\section{Le code du protocole}
L'emetteur exécute le programme suivant~:
\begin{verbatim}
Emetteur {
  tant que vrai faire {
    recevoir(Producteur, message)
    transmettreSurement(Recepteur, message);
  }
}
\end{verbatim}

Le récepteur exécute le programme suivant~:
\begin{verbatim}
Recepteur {
  tant que vrai faire {
    recevoirSurement(Emetteur, message);
    emettre(Consommateur, message)
  }
}
\end{verbatim}

\section{Les spécifications}\label{spec}
Toute solution doit satisfaire les propriétés suivantes~:
\begin{list}{P\theenumi}{\usecounter{enumi}}
\item Le protocole ne doit pas perdre de message.
\item Le protocole ne doit pas abimer de message.
\item Le protocole ne doit pas dupliquer de message.
\item Le protocole doit conserver l'ordonnancement des messages.
\end{list}

Afin de répondre à ces questions, il est généralement nécessaire de faire des hypothèses sur le type de communication et sur les qualités du réseau.

\begin{list}{H\theenumi}{\usecounter{enumi}}
\item Communications synchrones.
\item Communications asynchrones.
\item Réseau parfait.
\item Réseau avec pertes unidirectionnelle.
\item Réseau avec pertes bidirectionnelle.
\item Réseau avec duplication unidirectionnelle.
\item Réseau avec duplication bidirectionnelle.
\item \dots
\end{list}

\section{L'étude réalisée}

Nous allons vérifier si plusieurs protocoles de la littérature satisfont les propriétés enoncées en~\ref{spec}.

Pour cela, les algorithmes seront modélisés avec \altarica\ et les propriétés seront vérifiées avec \acheck.
