source: papers/FDL2012/exp_results.tex @ 71

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.


\begin{table*} [ht]
\hspace*{10mm}
\begin{tabular}{clccccc}

\toprule 
\multicolumn{2}{c}{\textbf{VCI-PI}}   & \emph{Number of}      & \emph{FSM}    & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\ 
\multicolumn{2}{c}{\textbf{Platform}} &\emph{BDD Variables}  & \emph{Depth}  & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
\midrule
\midrule
               & 1 Master-1 Slave   & 308 & 599 & 33 442   & 3.64116e+06 & 41.49 \\
 Concrete      & 2 Masters-1 Slave  & 439 & 186 & 75 210   & 73282       & 14.36 \\
  Model        & 4 Masters-1 Slave  & 709 & 408 & 156 657  & 2.15076e+07 & 414.38 \\
               & 4 Masters-2 Slaves & 883 & 597 & 217 797  & 3.22215e+10 & 4064.09 \\
 \midrule 
 \midrule
 Final         & 1 Master-1 Slave   & 197 & 2   &  76   &  5.03316e+07  & 0.01 \\
 Abstract      & 2 Masters-1 Slave  & 301 & 2   &  99   &  4.12317e+11  & 0.02 \\
 Model         & 4 Masters-1 Slave  & 501 & 2   & 147   &  3.45876e+18  & 0.03\\
 for $\phi_1$  & 4 Masters-2 Slaves & xx  & 2   & xxx   &  xxx          & xxxx \\
\midrule 
 Final         & 1 Master-1 Slave   & 194 & 1   & 50    &  2.62144e+07  & 0 \\
 Abstract      & 2 Masters-1 Slave  & 298 & 1   & 73    &  2.14748e+11  & 0.01 \\
 Model         & 4 Masters-1 Slave  & 498 & 1   & 121   &  1.80144e+18  & 0.02 \\
 for $\phi_2$  & 4 Masters-2 Slaves & xxx & x   & xxx   &  xxx          & xxx \\ 
\bottomrule  
\bottomrule
\end{tabular}
 
\caption{\label{StatsVCI_PI} Statistics on the VCI-PI platform}
\end{table*}
%\medskip


\begin{table*} [ht]
\hspace*{12mm}
\begin{tabular}{cccccc}

\toprule 
\textbf{CAN Bus}      & \emph{Number of}      & \emph{FSM}    & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\ 
\textbf{Platform}     &\emph{BDD Variables}  & \emph{Depth}  & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
\midrule
\midrule
 Concrete Model   & 838     & 182     & 212550    & 2.87296e+08      & 167.9 \\      
 \midrule 
 \midrule
 Final Abstract Model for $\phi_1$  & xx  & 2   & xxx   &  xxx       & xxxx \\
\midrule 
 Final Abstract Model for $\phi_2$  & xx  & 2   & xxx   &  xxx       & xxxx \\
\bottomrule  
\bottomrule
\end{tabular}
 
\caption{\label{StatsCAN_Bus} Statistics on the CAN Bus platform}
\end{table*}


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

\toprule 
\emph{Global}   &\emph{Verification} & \emph{Refinement}  & \emph{Verif.}  \\
\emph{Property} & \emph{Technique}  & \emph{Iteration}  & \emph{Time (s)}      \\ 
\midrule
\midrule
\multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\
                 & Prop. Selection   & 1    &    2.2     \\
 $\phi_1$   & Incremental       & 0    &   18.1        \\
            & Standard MC       & -    &   14.9     \\
\midrule
                 & Prop. Selection   & 0    &     1.0     \\
 $\phi_2$   & Incremental       & 467  &   168.0         \\
                 & Standard MC       & -    &    14.9      \\
\midrule   
\midrule
\multicolumn{4}{l}{\textbf{\underline{2 Masters - 1 Slave :}}}   \\   
                 & Prop. Selection   & 1    &    2.0     \\
 $\phi_1$   & Incremental       & 0    &    1.3        \\
            & Standard MC       & -    &    1.5     \\
\midrule
                 & Prop. Selection   & 0    &    1.0    \\
 $\phi_2$   & Incremental       & 0    &   15.3       \\
                 & Standard MC       & -    &   14.6    \\
\midrule
\midrule  
\multicolumn{4}{l}{\textbf{\underline{4 Masters - 1 Slave :}}}   \\ 
                 & Prop. Selection   & 1    &    2.1     \\
 $\phi_1$   & Incremental       & 0    &    6.8        \\
            & Standard MC       & -    &  175.5     \\
\midrule
                 & Prop. Selection   &  0    &   1.0 \\
 $\phi_2$   & Incremental       &  0    &   7.5    \\
                 & Standard MC       &  -    & 195.1 \\
\midrule 
\midrule
\multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}}  \\ 
                                & Prop. Selection   & 1   &  xxx     \\
 $\phi_1$   & Incremental       & xxx &  xxx         \\
            & Standard MC       & -   &  2231.3    \\
\midrule
            & Prop. Selection   & 0   &  xxx\\
 $\phi_2$   & Incremental       & N/A &  >1 day    \\
            & Standard MC       & -   &  12814.1 \\
\bottomrule       
\bottomrule

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

%\medskip

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

\toprule 
\emph{Global}  & \emph{Verification} & \emph{Refinement} & \emph{Verif.}   \\ 
\emph{Property}  & \emph{Technique}  & \emph{Iteration}  & \emph{Time (s)}       \\
\midrule
\midrule
                 & Prop. Selection  &  xxx        &  xxx     \\
 $\phi_3$   & Incremental      & N/A            &  >1 day \\
                 & Standard MC      & -                         &  51.9    \\
\midrule
                 & Prop. Selection   &  xxx       &  xxx \\
 $\phi_4$   & Incremental       & 0          &   57.3     \\
                 & Standard MC       & -          &    2.2    \\
\bottomrule

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

\medskip

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