Index: /papers/FDL2012/exp_results.tex =================================================================== --- /papers/FDL2012/exp_results.tex (revision 87) +++ /papers/FDL2012/exp_results.tex (revision 88) @@ -2,63 +2,46 @@ -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*{17mm} -\begin{tabular}{clcccc} - -\toprule -\multicolumn{2}{c}{\textbf{VCI-PI}} & \emph{Number of} & \emph{BDD} & \emph{Number of } & \emph{Analysis}\\ -\multicolumn{2}{c}{\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 & 911 & N/A & N/A & >1 day \\ - \midrule - \midrule - Final & 1 Master-1 Slave & 197 & 76 & 5.03316e+07 & 0.01 \\ - 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 \\ -\midrule - 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 \\ -\bottomrule -\bottomrule -\end{tabular} - -\caption{\label{StatsVCI_PI} Statistics on the VCI-PI platform} -\end{table*} -%\medskip - +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} -\begin{tabular}{ccccc} +\small +\begin{tabular}{cclcccc} \toprule -\textbf{CAN Bus} & \emph{Number of} & \emph{BDD} & \emph{Number of } & \emph{Analysis}\\ -\textbf{Platform} &\emph{BDD Variables} & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\ +\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 - Concrete Model & 822 & 161730 & 3.7354e+07 & 300.12 \\ + & & 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 & 911 & N/A & N/A & >1 day \\ +\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 - Final Abstract Model for $\phi_1$ & 425 & 187 & 1.66005e+12 & 0.03 \\ -\midrule - Final Abstract Model for $\phi_2$ & 425 & 187 & 1.66005e+12 & 0.04 \\ + &\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{StatsCAN_Bus} Statistics on the CAN Bus platform} + +\caption{\label{StatsPlatform} Statistics on the VCI-PI and CAN Bus platform} \end{table*} - @@ -66,86 +49,71 @@ \begin{table} [h] %\hspace*{-8mm} -\begin{tabular}{cccc} - +\small +\addtolength{\tabcolsep}{-1pt} +\begin{tabular}{ccccc} \toprule -\emph{Global} &\emph{Verification} & \emph{Refinement} & \emph{Verif.} \\ -\emph{Property} & \emph{Technique} & \emph{Iteration} & \emph{Time (s)} \\ +\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. Selection & 1 & 2.2 \\ - $\phi_1$ & Incremental & 0 & 6.3 \\ - & Standard MC & - & 6.06 \\ -\midrule - & Prop. Selection & 0 & 1.0 \\ - $\phi_2$ & Incremental & 562 & 200.9 \\ - & Standard MC & - & 6.13 \\ +%\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 -\multicolumn{4}{l}{\textbf{\underline{2 Masters - 1 Slave :}}} \\ - & Prop. Selection & 1 & 2.0 \\ - $\phi_1$ & Incremental & 0 & 20.4 \\ - & Standard MC & - & 37.9 \\ -\midrule - & Prop. Selection & 0 & 1.0 \\ - $\phi_2$ & Incremental & 74 & 786.3 \\ - & Standard MC & - & 39.4 \\ + & & 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 -\multicolumn{4}{l}{\textbf{\underline{4 Masters - 1 Slave :}}} \\ - & Prop. Selection & 1 & 2.1 \\ - $\phi_1$ & Incremental & 0 & 261.6 \\ - & Standard MC & - & >1 day \\ -\midrule - & Prop. Selection & 0 & 1.0 \\ - $\phi_2$ & Incremental & 0 & 263.5 \\ - & Standard MC & - & >1 day \\ + + & & 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 -\multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}} \\ - & Prop. Selection & 1 & 2.2 \\ - $\phi_1$ & Incremental & N/A & >1 day \\ - & Standard MC & - & >1 day \\ + + & & 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. Selection & 0 & 1.1\\ - $\phi_2$ & Incremental & N/A & >1 day \\ - & Standard MC & - & >1 day\\ + & & 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{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 & 0 & 1.02 \\ - $\phi_3$ & Incremental & N/A & >1 day \\ - & Standard MC & - & 2645.4 \\ -\midrule - & Prop. Selection & 0 & 1.01 \\ - $\phi_4$ & Incremental & N/A & >1 day \\ - & Standard MC & - & 1678.1 \\ -\bottomrule - -\end{tabular} - -\caption{\label{TabCANBus} Results on the CAN Bus platform } +\caption{\label{TabVerif} Verification Results } \end{table} -In the following tables: Table \ref{TabVCI_PI} and Table \ref{TabCANBus}, we compare the execution time between our technique (Prop. Selection), \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 42 verifed components properties to be selected in VCI-PI plateform and for the verification of $\phi_1$ we have restrained the selectable properties only to those without AG prefix. 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 Table \ref{TabVerif}, we compare the execution time 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 42 verifed components properties to be selected in VCI-PI plateform and for the verification of $\phi_1$ we have restrained the selectable properties only to those without AG prefix. 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.