\begin{frame}[allowframebreaks]{causal}

\begin{enumerate}

    \item Use Alloy to verify model consistency during every stage of model creation.
    
    \item Do a user study to verify the usability of the system interface and utilities. 
	
	\item Use Spin to verify that the concurrent aspects of the simulation cannot deadlock and that critical area consistency is preserved.

	\item (from Whyness) Use alloy to model the correctness of final outcome.

  \item (from Quadforce) Perform validation of interaction simulations based on
case studies of real world or well studied academic situations.
	
\end{enumerate}

\end{frame}
