source: papers/FDL2012/exp_results.tex @ 74

We have conducted preliminary experiments to tests and compare the performance of our strategy with existing abstraction-refinement technique available in VIS. As our test platforms 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}. It is an automatic abstraction refinement algorithm which generates an initial conservative abstraction principally by reducing the size of the latches by a constant factor. If the initial abstraction is not conclusive, a \emph{goal set} will then be computed in order to guide the refinement process.

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 on a CAN bus. Table \ref{StatsVCI_PI} and Table \ref{StatsCAN_Bus} give the size and the statistics concerning the VCI-PI platform and CAN bus platform respectively. All the values are obtained using the \emph{compute\_reach} command with option \emph{-v 1} in VIS except the number of BDD variables, computed using the \emph{print\_bdd\_stats} command. The experiments have been executed 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   & 7.3282e+04  & 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


In the following tables: Table \ref{TabVCI_PI} and Table \ref{TabCANBus}, we compare the execution time between our technique (Prop. Selection), incremental\_ctl\_verification (Incremental) and the standard model checking (Standard MC) computed using the \emph{model\_check} command in VIS (Note: Dynamic variable ordering has been enabled with sift method). For the VCI-PI platform, the global property $\phi_1$ is the type $AF(p=1)*AF(q=1)$ and $\phi_2$ is actually a stronger version of the same formula with $AG(AF(p=1)*AF(q=1))$ whereas for the CAN bus platform, the global property $\phi_3$ is the type $AG(((p'=1)*(q'=1)) -> AF((s = 1)*(r = 1))$ and $\phi_4 = AG(((p'=1)*(q'=1)) -> AG(r' = 0))$. We can see that our technique systematically computes faster than the other two methods and interestingly in the case where the size of the platform increases by adding the more connected components, in contrary to the other two methods, our computation time remains stable.


\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