source: papers/FDL2012/exp_results.tex @ 69

We have conducted preliminary experiments to tests and compare the performance of our strategy with existing abstraction-refinement technique available in VIS. As our abstraction representation requires fairness constraints, we have chosen the \emph{incremental\_ctl\_verification} abstraction refinement technique as it supports CTL formulas and fairness constraints \cite{PardoHachtel98incremCTLMC} \cite{PardoHachtel97autoAbsMC}. 


We have executed and compared the execution time and the number of refinement iterations for two examples: VCI-PI platform consisting of Virtual Component Interface (VCI), a PI-Bus and VCI-PI protocol converter and a simplified version of a CAN bus platform consisting of 3 nodes and a CAN bus. The results have been obtained on a PC with an AMD Athlon dual-core processor 4450e and 1.8GB of RAM memory.


\medskip

\begin{table} [h]
%\hspace*{-8mm}
\begin{tabular}{cccc}

\toprule 
\textbf{VCI} & \emph{Verification} & \emph{Verification}  & \emph{Refinement} \\ 
 \textbf{-PI}& \emph{Technique}  & \emph{Time (s)}       & \emph{Iteration} \\
\midrule
\midrule
             & Prop. Selection &    2.2    & 1 \\
 $\phi_1$   & Incremental      &  18.1    & 0    \\
             & Standard MC    &  14.9    & - \\
\midrule
             & Prop\_Selection &     1.0    & 0 \\
 $\phi_2$   & Incremental      & 168.0    & 467    \\
             & Standard MC    &   14.9    & - \\
\bottomrule

\end{tabular}
 
\caption{\label{TabVCI_PI} Results on VCI-PI platform }
\end{table}

%\medskip

\begin{table} [h]
%\hspace*{-8mm}
\begin{tabular}{cccc}

\toprule 
\textbf{CAN} & \emph{Verification} & \emph{Verification}  & \emph{Refinement} \\ 
\textbf{Bus}  & \emph{Technique}  & \emph{Time (s)}       & \emph{Iteration} \\
\midrule
\midrule
              & Prop. Selection  &             &       \\
 $\phi_1$   & Incremental       &  >1 day  & 0    \\
              & Standard MC     &  51.9    & - \\
\midrule
             & Prop\_Selection &              &   \\
 $\phi_2$   & Incremental      &   57.3    & 0   \\
             & Standard MC     &     2.2    & - \\
\bottomrule

\end{tabular}
 
\caption{\label{TabCANBus} Results on CAN Bus platform }
\end{table}

\medskip

Table 1 shows the... 
\TODO{Comments about Table 1, Table 2 and conclusion of Experimental Results}