\chapter{Le protocole du bit alterné}

\section{Le code de l'algorithme}

L'émetteur dans le protocole du bit alterné.
\begin{verbatim}
parite := true
while true do begin
              recevoir(message);             /* du producteur */
              repeter emettre(message,parite);
                      recevoir(ack,pariteAck);
              jusqu'a parite = pariteAck;
              parite := not parite;
              end;
\end{verbatim}

Le récepteur dans le protocole du bit alterné.
\begin{verbatim}
pariteAck := true
while true do begin
              repeter recevoir(message,parite);
                      emettre(ack,parite);
              jusqu'a parite = pariteAck;
              emettre(message);               /* vers le consommateur */
              pariteAck := not pariteAck;
              end;
\end{verbatim}

\section{Le modèle \altarica\ des composants pour ABP}

\renewcommand{\nodename}{EmetteurABP}
\renewcommand{\nodefilename}{EmetteurABP}
\subsection{Le n\oe ud \nodename}
\subsection{Le source AltaRica}
\verbatiminput{Alt/\nodefilename.alt}
\subsection{La sémantique}
La sémantique en terme de système de transition est donnée par la figure~\ref{\nodename}
\begin{figure}
\centering{\epsfig{file=\nodefilename.eps, width=\textwidth}}
\caption{Le n\oe ud \nodename}\label{\nodename}
\end{figure}

\renewcommand{\nodename}{RecepteurABP}
\renewcommand{\nodefilename}{RecepteurABP}
\subsection{Le n\oe ud \nodename}
\subsection{Le source AltaRica}
\verbatiminput{Alt/\nodefilename.alt}
\subsection{La sémantique}
La sémantique en terme de système de transition est donnée par la figure~\ref{\nodename}
\begin{figure}
\centering{\epsfig{file=\nodefilename.eps, width=\textwidth}}
\caption{Le n\oe ud \nodename}\label{\nodename}
\end{figure}

\section{L'étude}

\renewcommand{\nodename}{ABPparfait}
\renewcommand{\nodefilename}{ABPparfait}
\subsection{Le n\oe ud \nodename}
\subsection{Le source AltaRica}
\verbatiminput{Alt/\nodefilename.alt}
\subsection{La sémantique}
La sémantique en terme de système de transition est donnée par la figure~\ref{\nodename}
\begin{figure}
\centering{\epsfig{file=\nodefilename.eps, height=\textheight}}
\caption{Le n\oe ud \nodename}\label{\nodename}
\end{figure}
\subsection{Les propriétés}
\subsubsection{Les spécifications}
\verbatiminput{\nodefilename.spe}
\subsubsection{Les résultats}
\verbatiminput{\nodefilename.prop}
\subsubsection{Interprétations}
\verbatiminput{\nodefilename.res}

\renewcommand{\nodename}{ABPperteUnidirectionnelle}
\renewcommand{\nodefilename}{ABPperteUnidirectionnelle}
\subsection{Le n\oe ud \nodename}
\subsection{Le source AltaRica}
\verbatiminput{Alt/\nodefilename.alt}
\subsection{La sémantique}
La sémantique en terme de système de transition est donnée par la figure~\ref{\nodename}
\begin{figure}
\centering{\epsfig{file=\nodefilename.eps, width=\textwidth}}
\caption{Le n\oe ud \nodename}\label{\nodename}
\end{figure}
\subsection{Les propriétés}
\subsubsection{Les spécifications}
\verbatiminput{\nodefilename.spe}
\subsubsection{Les résultats}
\verbatiminput{\nodefilename.prop}
\subsubsection{Interprétations}
\verbatiminput{\nodefilename.res}
\begin{figure}
\centering{\epsfig{file=\nodefilename_bug.eps}}
\caption{Un blocage dans le n\oe ud \nodename}
\end{figure}

\renewcommand{\nodename}{ABPerreurUnidirectionnelle}
\renewcommand{\nodefilename}{ABPerreurUnidirectionnelle}
\subsection{Le n\oe ud \nodename}
\subsection{Le source AltaRica}
\verbatiminput{Alt/\nodefilename.alt}
\subsection{La sémantique}
La sémantique en terme de système de transition est donnée par la figure~\ref{\nodename}
\begin{figure}
\centering{\epsfig{file=\nodefilename.eps, width=\textwidth}}
\caption{Le n\oe ud \nodename}\label{\nodename}
\end{figure}
\subsection{Les propriétés}
\subsubsection{Les spécifications}
\verbatiminput{\nodefilename.spe}
\subsubsection{Les résultats}
\verbatiminput{\nodefilename.prop}
\subsubsection{Interprétations}
\verbatiminput{\nodefilename.res}

\section{Conclusion}

Dans cette étude, nous avons montré que~:
Sous l'hypothèse de communications synchrones ({\bf H1}), le protocole du bit alterné vérifie les propriétés suivantes~:
\begin{enumerate}
\item {\bf P1, P2, P3, sans blocage} si le réseau est parfait.
\item {\bf P1, P2, P3, sans blocage} si un seul sens du réseau abime les messages.
\item {\bf P1, P2, P3 avec risque de blocage} si un seul sens du réseau perd les messages.
\end{enumerate}
