\section{Spin Analysis of UML Diagrams via Promela Specifications}
%
% Give a brief description of the three types of analysis that
% you will be performing:
% 1. asserts
% 2. reachability
% 3. never claims (liveness or safety checks)
%
% For each type of check below, please explain the impact
% on your modeling that the check had (e.g., you had
% to revise one or more models, you gained a better
% understanding of the requirements, you were able
% to clarify the textual descriptions, etc. 
%************************************************************
% If you give more than one example of a given type of
% analysis, please use either enumerate, itemize, or
% separate paragraphs with \paragraph{Assertion Check 2}
% to break them up. 
%
% You will receive extra credit
% for additional checks of any of the above types.


\subsection{Assertion Check}

%
% Give the English version of the property, and then
% the Promela version.
% Include the Promela proctype that you are
% using for the check. 
% Include excerpts from the Spin output that illustrate
% your results. 
%
\subsection{Reachability Analysis}
%
% Do the same thing for reachability analysis
%
%
\subsection{Model Checking}
%
% Do the same thing for reachability analysis
%
%