%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% LaTeX poster template
% Created by Nathaniel Johnston
% August 2009
% http://www.nathanieljohnston.com/2009/08/latex-poster-template/
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\documentclass[final]{beamer}
\usepackage[orientation=landscape, size=custom, height=60.96, width=91.44, scale=0.85]{beamerposter} % size=a0

% \usepackage[orientation=landscape, scale=1]{beamerposter} % size=a0
\usepackage{graphicx}			% allows us to import images
\usepackage{tikz}
\usetikzlibrary{circuits,shapes,arrows,fit,calc,positioning,automata}
\usepackage{lipsum}
\usepackage{wrapfig}
\usepackage{epsfig}

%\usepackage{libertine}
% \usepackage[margin=1in, paperwidth=36in, paperheight=24in]{geometry}
%TODO set size to 24"x36"
%-----------------------------------------------------------
% Define the column width and poster size
% To set effective sepwid, onecolwid and twocolwid values, first choose how many columns you want and how much separation you want between columns
% The separation I chose is 0.024 and I want 4 columns
% Then set onecolwid to be (1-(4+1)*0.024)/4 = 0.22
% Set twocolwid to be 2*onecolwid + sepwid = 0.464
%-----------------------------------------------------------

\newlength{\sepwid}
\newlength{\onecolwid}
\newlength{\twocolwid}
\newlength{\threecolwid}
% \setlength{\paperwidth}{36in}
% \setlength{\paperheight}{24in}
\setlength{\sepwid}{0.024\paperwidth}
\setlength{\onecolwid}{0.22\paperwidth}
\setlength{\twocolwid}{0.272\paperwidth}
\setlength{\threecolwid}{0.708\paperwidth}
% \setlength{\topmargin}{-0.5in}
\usetheme{CSA}
\usepackage{exscale}
\usepackage{wrapfig}

%-----------------------------------------------------------
% The next part fixes a problem with figure numbering. Thanks Nishan!
% When including a figure in your poster, be sure that the commands are typed in the following order:
% \begin{figure}
% \includegraphics[...]{...}
% \caption{...}
% \end{figure}
% That is, put the \caption after the \includegraphics
%-----------------------------------------------------------

\usecaptiontemplate{
\small
\structure{\insertcaptionname~\insertcaptionnumber:}
\insertcaption}

%-----------------------------------------------------------
% Define colours (see beamerthemeconfposter.sty to change these colour definitions)
%-----------------------------------------------------------

% \setbeamercolor{block title}{fg=ngreen,bg=white}
\setbeamercolor{block body}{fg=black,bg=white}
\setbeamercolor{block alerted title}{fg=white,bg=dblue!70}
\setbeamercolor{block alerted body}{fg=black,bg=dblue!10}

%-----------------------------------------------------------
% Name and authors of poster/paper/research
%-----------------------------------------------------------

\title{Transducer Models of Retransmission Protocols for Noisy Channels}
\author{Jay Thakkar and Aditya Kanade}
\institute{Indian Institute of Science, Bangalore\\
Work submitted to Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}
\footer{footer text}

%-----------------------------------------------------------
% Start the poster itself
%-----------------------------------------------------------

\begin{document}
\setbeamertemplate{background}
 {\includegraphics[width=\paperwidth,height=\paperheight]{slide_bg}}
\begin{frame}[t]
  \vspace{-1cm}
  \begin{columns}[t]		
										% the [t] option aligns the column's content at the top
    		% empty spacer column
    \begin{column}{\onecolwid}
      \setbeamercolor{block alerted title}{fg=white,bg=norange}	% frame color
      \setbeamercolor{block alerted body}{fg=black,bg=norange!10}
      \begin{alertblock}{Introduction}
      \begin{block}{Communication System}


      
        
      

	\begin{minipage}{0.4\linewidth}
\boldmath
      \input{comm}
      \vspace{-1.5cm}
      \input{comm1}
      \unboldmath\end{minipage}%
\begin{minipage}{0.6\linewidth}
\begin{itemize}
  \item Communication channel between sender and receiver can be unreliable.
 \item {\color{Blue}Aim}: To transfer the message successfully from sender to receiver, without any error.

 
\end{itemize}

\end{minipage}

        
      \end{block}
      \vskip1ex
      \begin{block}{Retransmission Protocols}

	\begin{minipage}{0.35\linewidth}
	  \boldmath
	  \input{swd}
	  \unboldmath
	\end{minipage}%
	\begin{minipage}{0.65\linewidth}
	  \begin{itemize}
	    \item They are used to ensure that a sequence of frames is delivered in order and without errors despite of transmission errors.

	    \item Reliable delivery is achieved using acknowledgements with re-transmission paradigm.

	  \end{itemize}
	\end{minipage}
      \vspace{0.25cm}  
      \end{block}
      \vskip1ex
      \begin{block}{Cyclic Redundancy Check}
	\begin{itemize}
	 \item The \emph{cyclic redundancy check (CRC)} is a common technique for detecting errors in data transmission. 
	 \item Given a fixed generator polynomial, we build an SST to encode a message string into a cyclic redundancy check (CRC) codeword.
	\end{itemize}

	
        
      \end{block}
      \vskip1ex
      \begin{block}{Streaming String Transducer}
      
	  \begin{itemize}
	   \item An SST reads an input string in a single left-to-right pass and produces the output string using a finite set of states. 
	   \item It also uses a finite set of string variables to store strings over the output alphabet. 
	   \item On each input symbol, it may transition to another state and update string variables.
 	  \end{itemize}
	  \begin{minipage}{0.5\linewidth}
	  \boldmath
	  \input{sst}
	  \unboldmath
	\end{minipage}%
	\begin{minipage}{0.5\linewidth}
	  \begin{itemize}
	   \item A string variable can be used at most once across the right-hand side of the parallel assignment.
	  \end{itemize}
	\end{minipage}
	  

        
      \end{block}
    \end{alertblock}
    \end{column}


%  \begin{column}
%    {\sepwid}
%   \end{column}	
%\hspace{-17mm}
  \begin{column}{\twocolwid}
      
      \begin{alertblock}{Protocol Models}
      \begin{block}{Sender SST for SWP}

	\begin{itemize}
          \item The sender receives a message and encodes it into a frame with sequence number, message content and checksum.
	  \item The sender outputs a correct frame upon receiving a positive ACK and a corrupt frame upon receiving a negative ACK.
          \item String variable $x$ plays the role of the sender's buffer.
        \end{itemize}




\input{sender}
\vspace{0.5mm}
\end{block}
\vskip1ex
\begin{block}{Receiver SST for SWP}

	\begin{itemize}
          \item It distinguishes between the correct and corrupt frames.
          \item For the correctly received frame, it removes sequence number and checksum and passes the message to its client. 
	\end{itemize}


      \input{receiver}


\end{block}


\end{alertblock}
\end{column}

%\begin{column}
%    {\sepwid}
%   \end{column}
%\hspace{-30mm}

  \begin{column}{\twocolwid}
   \setbeamercolor{block alerted title}{fg=white,bg=norange1}	% frame color
      \setbeamercolor{block alerted body}{fg=black,bg=norange1!10}
  \begin{alertblock}{Verification Approach}

      \begin{block}{Specification SST for SWP}

	\begin{itemize}
          \item {\color{Blue}Key Property}:  Messages acknowledged by the receiver are delivered to the receiver's client correctly and in the same order in which the client of the sender handed them to the sender.
          \item  The \emph{specification SST} does not encode checksum computation, noisy outputs and repeated retransmissions. 
	  \item  The input to the specification transducer is a sequence of messages and acknowledgements (similar to the sender) and the output is a sequence of correctly delivered messages (similar to
the receiver).
	\end{itemize}
 

\input{specification}
\vspace{1.4cm}
\end{block}
\vskip1ex
\begin{block}{The Verification Layout}

      
\begin{minipage}{0.45\linewidth}
 \centering
 \includegraphics[height=0.6\onecolwid]{fig1} % The mechanism space
\end{minipage}%
\begin{minipage}{0.55\linewidth}
\begin{itemize}
 \item {\color{Blue}Verification Problem}: To check \emph{functional equivalence} between the specification and the protocol model.
 \item The output of the sender is the input of the receiver. 
 \item The model for the entire protocol is obtained by sequentially composing the two.
 
\end{itemize}

\end{minipage}
\vspace{1.85cm}

% \begin{wrapfigure}{l}{8.5cm}
%  \centering
%  \includegraphics[height=0.6\onecolwid]{fig1} % The mechanism space
% \end{wrapfigure}
% 
% 
%            Verification Problem: to check \emph{functional equivalence} between the specification and the protocol model.
%            The output of the sender is the input of the receiver. The model for the entire protocol is obtained by sequentially composing the two.
% 
% {\color{jblue}Verification Problem}: to check \emph{functional equivalence} between the specification and the protocol model.
%            The output of the sender is the input of the receiver. The model for the entire protocol is obtained by sequentially composing the two.
	
\end{block}

\vspace{0.005mm}
\end{alertblock}
\end{column} 

%   \begin{column}
%    {\sepwid}
%   \end{column}	
%\hspace{-30mm}

  \begin{column}{\onecolwid}
  \begin{alertblock}{Wrapping Up\ldots}

      \begin{block}{Case studies}


\begin{enumerate}

\item \textbf{\color{Fuchsia}TinyOS} : The SerialP~\cite{website:tinyos-serial} software module of
TinyOS computes the checksum and uses the stop-and-wait protocol in the host-to-mote direction. 

\item \textbf{\color{Fuchsia}HDLC} : HDLC~\cite{hdlc} is a bit-oriented protocol, that operates at data link layer. Its software implementations compute checksum and use go-back-n 
protocol.
\end{enumerate}
	
            \vspace{0.4cm}
  
      \end{block}
      \vskip1ex
      \begin{block}{Conclusions and Future Work}
      
	\begin{itemize}
	  \item Our work allows explicit modeling of message contents yet enables algorithmic verification of the resulting protocol models.
	  \item In the future, we will try to permit arbitrary bit corruption using non-deterministic version of SSTs.
	  \item Bounding the number of retransmission rounds can also be useful to extend the protocol models.
	\end{itemize}
	
      \end{block}
      \vskip1ex
      \begin{block}{Related Work}
       \begin{itemize}
        \item Several automated techniques abstract messages to model and verify these protocols~\cite{DBLP:journals/comsur/BabichD02}, whereas we model a message as a bit stream. Hence, we use SSTs to model these protocols.
	\item SSTs are closed under sequential composition~\cite{DBLP:conf/fsttcs/AlurC10} and the equivalence problem for SSTs is decidable~\cite{DBLP:conf/popl/AlurC11}.    
       \end{itemize}
      \vspace{0.5cm}
      \end{block}

      \vskip1ex
      \begin{block}{References}
       \scriptsize \justifying
\bibliographystyle{ieeetr}
\bibliography{poster}
      \end{block}


\end{alertblock}



  \end{column}

%  \begin{column}
%    {\sepwid}
%  \end{column}
%\section{References}

 \end{columns}
\end{frame}
\end{document}
