source: papers/FDL2012/exp_results.tex

We have conducted preliminary experiments to test and compare the performance
of our strategy with existing techniques available in
VIS. There are several abstraction-refinement techniques implemented in VIS
accessible via \emph{approximate\_model\_check},
\emph{iterative\_model\_check}, \emph{check\_invariant} and
\emph{incremental\_ctl\_verification} commands. However, among the available
techniques, \emph{incremental\_ctl\_verification} is the only one that supports CTL formulas and fairness constraints which are necessary in our test platforms. 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 \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 on a CAN bus. Table \ref{StatsPlatform} gives the size and the statistics concerning the VCI-PI platform and CAN bus platform verified. 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*{15mm}
%\small
\footnotesize
\begin{tabular}{cclcccc}

\toprule 
\multicolumn{3}{l}{\textbf{Experiment}}   & \emph{Number of}      & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\ 
\multicolumn{3}{l}{\textbf{Platform}}     &\emph{BDD Variables}   & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
\midrule
\midrule
                        &               & 1 Master-1 Slave   & 304  & 7207     & 4.711e+3    & 6.36 \\
                        & Concrete      & 2 Masters-1 Slave  & 445  & 24406    & 7.71723e+06 & 35.2 \\
                        &  Model        & 4 Masters-1 Slave  & 721  & 84118    & 3.17332e+12 & 2818.3 \\
                        &               & 4 Masters-2 Slaves & 895  & 238990   & 5.708e+15   & 68882.3\footnotemark[1] \\
\cline{2-7} 
\cline{2-7}
                        & Final         & 1 Master-1 Slave   & 197  &  76   &  5.03316e+07  & 0.01 \\
VCI-PI  & Abstract      & 2 Masters-1 Slave  & 301  &  99   &  4.12317e+11  & 0.02 \\
                        & Model         & 4 Masters-1 Slave  & 501  & 147   &  3.45876e+18  & 0.03\\
                        & for $\phi_1$  & 4 Masters-2 Slaves & 589  & 167   &  7.08355e+21  & 0.04 \\
\cline{2-7}
                        & Final         & 1 Master-1 Slave   & 194  & 50    &  2.62144e+07  & 0 \\
                        & Abstract      & 2 Masters-1 Slave  & 298  & 73    &  2.14748e+11  & 0.01 \\
                        & Model         & 4 Masters-1 Slave  & 498  & 121   &  1.80144e+18  & 0.02 \\
                        & for $\phi_2$  & 4 Masters-2 Slaves & 586  & 141   &  3.68935e+21  & 0.02 \\ 
% \midrule 
 \midrule
                        &\multicolumn{2}{c}{Concrete Model}                                          & 822     & 161730      & 3.7354e+07     & 300.12 \\      
\cline{2-7}
\cline{2-7}
CAN Bus  &\multicolumn{2}{c}{Final Abstract Model for $\phi_3$}  & 425   & 187   &  1.66005e+12       & 0.03 \\
\cline{2-7}
                        &\multicolumn{2}{c}{Final Abstract Model for $\phi_4$}  & 425   & 187   &  1.66005e+12       & 0.04 \\
\bottomrule  
%\bottomrule
\end{tabular}
\caption{\label{StatsPlatform} Statistics on the VCI-PI and CAN Bus platform}
\end{table*}

%\footnotetext[1]{Computed on a calculation server.}


\begin{table} [h]
%\hspace*{-8mm}
\small
\addtolength{\tabcolsep}{-1pt}
\begin{tabular}{ccccc}
\toprule 
\emph{Experim.}     &\emph{Global}   &\emph{Verification} & \emph{Refine.}  & \emph{Verif.}  \\
\emph{Platform}         &\emph{Property} & \emph{Technique}  & \emph{Iter.}  & \emph{Time (s)}      \\ 
\midrule
\midrule
%\multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\
                                &                 & Prop. Select.   & 1    &    2.2     \\
VCI-PI:         & $\phi_1$   & Incremental       & 0    &    6.3        \\
1 Master                &            & Standard MC       & -    &    6.06     \\
\cline{2-5}
-                               &                 & Prop. Select.   & 0    &     1.0     \\
1 Slave         & $\phi_2$   & Incremental       & 562  &   200.9         \\
                                &                 & Standard MC       & -    &    6.13      \\
\midrule   
%\midrule
                                &                 & Prop. Select.   & 1    &    2.0     \\
VCI-PI:                 & $\phi_1$   & Incremental       & 0    &   20.4        \\
2 Masters       &            & Standard MC       & -    &   37.9     \\
\cline{2-5}
-                               &                 & Prop. Select.   & 0    &    1.0    \\
1 Slave         & $\phi_2$   & Incremental       & 74   &  786.3        \\
                                &                 & Standard MC       & -    &   39.4    \\
\midrule
%\midrule  

                                &                 & Prop. Select.   &  1   &    2.1     \\
VCI-PI:         & $\phi_1$   & Incremental       &  0   &  261.6      \\
4 Masters       &            & Standard MC       &  -   &  >1 day     \\
\cline{2-5}
-                  &              & Prop. Select.   &  0   &   1.0    \\
1 Slave         & $\phi_2$   & Incremental       &  0   &   263.5     \\
                                &                 & Standard MC       &  -   &   >1 day   \\
\midrule 
%\midrule

                                &                                & Prop. Select.   & 1          &  2.2     \\
VCI-PI:     & $\phi_1$   & Incremental       & N/A      &  >1 day    \\
4 Masters       &            & Standard MC       & -    &  >1 day   \\
\cline{2-5}
  -                &            & Prop. Select.   & 0           &  1.1\\
2 Slaves                & $\phi_2$   & Incremental       & N/A  &  >1 day    \\
                                &            & Standard MC       & -    &  >1 day\\
\midrule 
%\midrule
                &                 & Prop. Select.   &  0     &  1.02     \\
                                &$\phi_3$    & Incremental       & N/A    &  >1 day   \\
CAN                     &                 & Standard MC       & -       &  2645.4    \\
\cline{2-5}
Bus                     &                 & Prop. Select.   &  0     &   1.01     \\
                                &$\phi_4$    & Incremental       & N/A    &  >1 day    \\
                                &                 & Standard MC       & -      &   1678.1    \\    

\bottomrule       
%\bottomrule

\end{tabular}

\caption{\label{TabVerif} Verification Results  }
\end{table}


In Table \ref{TabVerif}, we compare the execution time and the number of refinement
between our technique (Prop. Select.), \emph{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)))$. We have a total of
26 verified components properties to be selected in the VCI-PI platform.
In comparison to $\phi_2$, we can see that, a better set of properties available will result in a better abstraction and less refinement iterations.  


In the case of the CAN bus platform, the global property $\phi_3$ is the type
$AG(((p'=1)*(q'=1)*AF(r_1=1)) \rightarrow AF((s_1=1)*AF(t_1=1)))$ and $\phi_4
= AG(((p'=1)*(q'=1)*AG(r_2=0)) \rightarrow AG((s_2=0)*(t_2=0)))$. We have at
our disposal 103 verified component properties and after the selection process
for the initial abstraction, 3 selected component properties were sufficient
to verify both global properties without refinement.

Globally, we can see that our technique, for these examples, systematically computes faster than the other two methods and interestingly in the case where the size of the platform increases by adding  more connected components, in contrary to the other two methods, our computation time remains stable. This is mainly due to the fact that for small number of properties, our abstraction is generated almost instantly and as only pertinent properties are selected, not many refinement iterations are required in order to complete the verification process. It is also important to note that the properties tested are simple and we have in our property selection list the local properties required to satisfy the global property. 



%\medskip