Index: /papers/FDL2012/exp_results.tex =================================================================== --- /papers/FDL2012/exp_results.tex (revision 70) +++ /papers/FDL2012/exp_results.tex (revision 71) @@ -1,9 +1,62 @@ 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*} [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] @@ -12,20 +65,52 @@ \toprule -\textbf{VCI} & \emph{Verification} & \emph{Verification} & \emph{Refinement} \\ - \textbf{-PI}& \emph{Technique} & \emph{Time (s)} & \emph{Iteration} \\ +\emph{Global} &\emph{Verification} & \emph{Refinement} & \emph{Verif.} \\ +\emph{Property} & \emph{Technique} & \emph{Iteration} & \emph{Time (s)} \\ \midrule \midrule - & Prop. Selection & 2.2 & 1 \\ - $\phi_1$ & Incremental & 18.1 & 0 \\ - & Standard MC & 14.9 & - \\ +\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 & 1.0 & 0 \\ - $\phi_2$ & Incremental & 168.0 & 467 \\ - & Standard MC & 14.9 & - \\ + & 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 VCI-PI platform } +\caption{\label{TabVCI_PI} Results on the VCI-PI platform } \end{table} @@ -34,23 +119,23 @@ \begin{table} [h] %\hspace*{-8mm} -\begin{tabular}{cccc} +\begin{tabular}{lcccc} \toprule -\textbf{CAN} & \emph{Verification} & \emph{Verification} & \emph{Refinement} \\ -\textbf{Bus} & \emph{Technique} & \emph{Time (s)} & \emph{Iteration} \\ +\emph{Global} & \emph{Verification} & \emph{Refinement} & \emph{Verif.} \\ +\emph{Property} & \emph{Technique} & \emph{Iteration} & \emph{Time (s)} \\ \midrule \midrule - & Prop. Selection & & \\ - $\phi_1$ & Incremental & >1 day & 0 \\ - & Standard MC & 51.9 & - \\ + & Prop. Selection & xxx & xxx \\ + $\phi_3$ & Incremental & N/A & >1 day \\ + & Standard MC & - & 51.9 \\ \midrule - & Prop\_Selection & & \\ - $\phi_2$ & Incremental & 57.3 & 0 \\ - & Standard MC & 2.2 & - \\ + & Prop. Selection & xxx & xxx \\ + $\phi_4$ & Incremental & 0 & 57.3 \\ + & Standard MC & - & 2.2 \\ \bottomrule \end{tabular} -\caption{\label{TabCANBus} Results on CAN Bus platform } +\caption{\label{TabCANBus} Results on the CAN Bus platform } \end{table}