![(please configure the [header_logo] section in trac.ini)](/trac/verif_tools/chrome/site/your_project_logo.png){kind=logo}
- Timestamp:
- Apr 6, 2012, 1:50:44 PM (13 years ago)
- File:
-
- 1 edited
-
papers/FDL2012/exp_results.tex (modified) (2 diffs)
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/exp_results.tex
r83 r88 2 2 3 3 4 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. 5 6 7 \begin{table*} [ht] 8 \hspace*{17mm} 9 \begin{tabular}{clcccc} 10 11 \toprule 12 \multicolumn{2}{c}{\textbf{VCI-PI}} & \emph{Number of} & \emph{BDD} & \emph{Number of } & \emph{Analysis}\\ 13 \multicolumn{2}{c}{\textbf{Platform}} &\emph{BDD Variables} & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\ 14 \midrule 15 \midrule 16 & 1 Master-1 Slave & 304 & 7207 & 4.711e+3 & 6.36 \\ 17 Concrete & 2 Masters-1 Slave & 445 & 24406 & 7.71723e+06 & 35.2 \\ 18 Model & 4 Masters-1 Slave & 721 & 84118 & 3.17332e+12 & 2818.3 \\ 19 & 4 Masters-2 Slaves & 911 & N/A & N/A & >1 day \\ 20 \midrule 21 \midrule 22 Final & 1 Master-1 Slave & 197 & 76 & 5.03316e+07 & 0.01 \\ 23 Abstract & 2 Masters-1 Slave & 301 & 99 & 4.12317e+11 & 0.02 \\ 24 Model & 4 Masters-1 Slave & 501 & 147 & 3.45876e+18 & 0.03\\ 25 for $\phi_1$ & 4 Masters-2 Slaves & 589 & 167 & 7.08355e+21 & 0.04 \\ 26 \midrule 27 Final & 1 Master-1 Slave & 194 & 50 & 2.62144e+07 & 0 \\ 28 Abstract & 2 Masters-1 Slave & 298 & 73 & 2.14748e+11 & 0.01 \\ 29 Model & 4 Masters-1 Slave & 498 & 121 & 1.80144e+18 & 0.02 \\ 30 for $\phi_2$ & 4 Masters-2 Slaves & 586 & 141 & 3.68935e+21 & 0.02 \\ 31 \bottomrule 32 \bottomrule 33 \end{tabular} 34 35 \caption{\label{StatsVCI_PI} Statistics on the VCI-PI platform} 36 \end{table*} 37 %\medskip 38 4 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. 39 5 40 6 41 7 \begin{table*} [ht] 42 8 \hspace*{15mm} 43 \begin{tabular}{ccccc} 9 \small 10 \begin{tabular}{cclcccc} 44 11 45 12 \toprule 46 \ textbf{CAN Bus} & \emph{Number of}& \emph{BDD} & \emph{Number of } & \emph{Analysis}\\47 \ textbf{Platform} &\emph{BDD Variables}& \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\13 \multicolumn{3}{l}{\textbf{Experiment}} & \emph{Number of} & \emph{BDD} & \emph{Number of } & \emph{Analysis}\\ 14 \multicolumn{3}{l}{\textbf{Platform}} &\emph{BDD Variables} & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\ 48 15 \midrule 49 16 \midrule 50 Concrete Model & 822 & 161730 & 3.7354e+07 & 300.12 \\ 17 & & 1 Master-1 Slave & 304 & 7207 & 4.711e+3 & 6.36 \\ 18 & Concrete & 2 Masters-1 Slave & 445 & 24406 & 7.71723e+06 & 35.2 \\ 19 & Model & 4 Masters-1 Slave & 721 & 84118 & 3.17332e+12 & 2818.3 \\ 20 & & 4 Masters-2 Slaves & 911 & N/A & N/A & >1 day \\ 21 \cline{2-7} 22 \cline{2-7} 23 & Final & 1 Master-1 Slave & 197 & 76 & 5.03316e+07 & 0.01 \\ 24 VCI-PI & Abstract & 2 Masters-1 Slave & 301 & 99 & 4.12317e+11 & 0.02 \\ 25 & Model & 4 Masters-1 Slave & 501 & 147 & 3.45876e+18 & 0.03\\ 26 & for $\phi_1$ & 4 Masters-2 Slaves & 589 & 167 & 7.08355e+21 & 0.04 \\ 27 \cline{2-7} 28 & Final & 1 Master-1 Slave & 194 & 50 & 2.62144e+07 & 0 \\ 29 & Abstract & 2 Masters-1 Slave & 298 & 73 & 2.14748e+11 & 0.01 \\ 30 & Model & 4 Masters-1 Slave & 498 & 121 & 1.80144e+18 & 0.02 \\ 31 & for $\phi_2$ & 4 Masters-2 Slaves & 586 & 141 & 3.68935e+21 & 0.02 \\ 51 32 \midrule 52 33 \midrule 53 Final Abstract Model for $\phi_1$ & 425 & 187 & 1.66005e+12 & 0.03 \\ 54 \midrule 55 Final Abstract Model for $\phi_2$ & 425 & 187 & 1.66005e+12 & 0.04 \\ 34 &\multicolumn{2}{c}{Concrete Model} & 822 & 161730 & 3.7354e+07 & 300.12 \\ 35 \cline{2-7} 36 \cline{2-7} 37 CAN Bus &\multicolumn{2}{c}{Final Abstract Model for $\phi_3$} & 425 & 187 & 1.66005e+12 & 0.03 \\ 38 \cline{2-7} 39 &\multicolumn{2}{c}{Final Abstract Model for $\phi_4$} & 425 & 187 & 1.66005e+12 & 0.04 \\ 56 40 \bottomrule 57 41 \bottomrule 58 42 \end{tabular} 59 60 \caption{\label{Stats CAN_Bus} Statistics on theCAN Bus platform}43 44 \caption{\label{StatsPlatform} Statistics on the VCI-PI and CAN Bus platform} 61 45 \end{table*} 62 63 46 64 47 … … 66 49 \begin{table} [h] 67 50 %\hspace*{-8mm} 68 \begin{tabular}{cccc} 69 51 \small 52 \addtolength{\tabcolsep}{-1pt} 53 \begin{tabular}{ccccc} 70 54 \toprule 71 \emph{ Global} &\emph{Verification} & \emph{Refinement} & \emph{Verif.} \\72 \emph{P roperty} & \emph{Technique} & \emph{Iteration} & \emph{Time (s)} \\55 \emph{Experim.} &\emph{Global} &\emph{Verification} & \emph{Refine.} & \emph{Verif.} \\ 56 \emph{Platform} &\emph{Property} & \emph{Technique} & \emph{Iter.} & \emph{Time (s)} \\ 73 57 \midrule 74 58 \midrule 75 \multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\76 & Prop. Selection& 1 & 2.2 \\77 $\phi_1$ & Incremental & 0 & 6.3 \\78 & Standard MC & - & 6.06 \\79 \ midrule80 & Prop. Selection& 0 & 1.0 \\81 $\phi_2$ & Incremental & 562 & 200.9 \\82 & Standard MC & - & 6.13 \\59 %\multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\ 60 & & Prop. Select. & 1 & 2.2 \\ 61 VCI-PI: & $\phi_1$ & Incremental & 0 & 6.3 \\ 62 1 Master & & Standard MC & - & 6.06 \\ 63 \cline{2-5} 64 - & & Prop. Select. & 0 & 1.0 \\ 65 1 Slave & $\phi_2$ & Incremental & 562 & 200.9 \\ 66 & & Standard MC & - & 6.13 \\ 83 67 \midrule 84 68 \midrule 85 \multicolumn{4}{l}{\textbf{\underline{2 Masters - 1 Slave :}}} \\ 86 & Prop. Selection & 1 & 2.0 \\ 87 $\phi_1$ & Incremental & 0 & 20.4 \\ 88 & Standard MC & - & 37.9 \\ 89 \midrule 90 & Prop. Selection & 0 & 1.0 \\ 91 $\phi_2$ & Incremental & 74 & 786.3 \\ 92 & Standard MC & - & 39.4 \\ 69 & & Prop. Select. & 1 & 2.0 \\ 70 VCI-PI: & $\phi_1$ & Incremental & 0 & 20.4 \\ 71 2 Masters & & Standard MC & - & 37.9 \\ 72 \cline{2-5} 73 - & & Prop. Select. & 0 & 1.0 \\ 74 1 Slave & $\phi_2$ & Incremental & 74 & 786.3 \\ 75 & & Standard MC & - & 39.4 \\ 93 76 \midrule 94 77 \midrule 95 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 1 Slave :}}} \\ 96 & Prop. Selection& 1 & 2.1 \\97 $\phi_1$ & Incremental & 0 & 261.6 \\98 & Standard MC & - & >1 day \\99 \ midrule100 & Prop. Selection& 0 & 1.0 \\101 $\phi_2$ & Incremental & 0 & 263.5 \\102 & Standard MC & - & >1 day \\78 79 & & Prop. Select. & 1 & 2.1 \\ 80 VCI-PI: & $\phi_1$ & Incremental & 0 & 261.6 \\ 81 4 Masters & & Standard MC & - & >1 day \\ 82 \cline{2-5} 83 - & & Prop. Select. & 0 & 1.0 \\ 84 1 Slave & $\phi_2$ & Incremental & 0 & 263.5 \\ 85 & & Standard MC & - & >1 day \\ 103 86 \midrule 104 87 \midrule 105 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}} \\ 106 & Prop. Selection & 1 & 2.2 \\ 107 $\phi_1$ & Incremental & N/A & >1 day \\ 108 & Standard MC & - & >1 day \\ 88 89 & & Prop. Select. & 1 & 2.2 \\ 90 VCI-PI: & $\phi_1$ & Incremental & N/A & >1 day \\ 91 4 Masters & & Standard MC & - & >1 day \\ 92 \cline{2-5} 93 - & & Prop. Select. & 0 & 1.1\\ 94 2 Slaves & $\phi_2$ & Incremental & N/A & >1 day \\ 95 & & Standard MC & - & >1 day\\ 96 \midrule 109 97 \midrule 110 & Prop. Selection & 0 & 1.1\\ 111 $\phi_2$ & Incremental & N/A & >1 day \\ 112 & Standard MC & - & >1 day\\ 98 & & Prop. Select. & 0 & 1.02 \\ 99 &$\phi_3$ & Incremental & N/A & >1 day \\ 100 CAN & & Standard MC & - & 2645.4 \\ 101 \cline{2-5} 102 Bus & & Prop. Select. & 0 & 1.01 \\ 103 &$\phi_4$ & Incremental & N/A & >1 day \\ 104 & & Standard MC & - & 1678.1 \\ 105 113 106 \bottomrule 114 107 \bottomrule 115 108 116 109 \end{tabular} 117 118 \caption{\label{TabVCI_PI} Results on the VCI-PI platform }119 \end{table}120 110 121 %\medskip 122 123 124 \begin{table} [h] 125 %\hspace*{-8mm} 126 \begin{tabular}{lcccc} 127 128 \toprule 129 \emph{Global} & \emph{Verification} & \emph{Refinement} & \emph{Verif.} \\ 130 \emph{Property} & \emph{Technique} & \emph{Iteration} & \emph{Time (s)} \\ 131 \midrule 132 \midrule 133 & Prop. Selection & 0 & 1.02 \\ 134 $\phi_3$ & Incremental & N/A & >1 day \\ 135 & Standard MC & - & 2645.4 \\ 136 \midrule 137 & Prop. Selection & 0 & 1.01 \\ 138 $\phi_4$ & Incremental & N/A & >1 day \\ 139 & Standard MC & - & 1678.1 \\ 140 \bottomrule 141 142 \end{tabular} 143 144 \caption{\label{TabCANBus} Results on the CAN Bus platform } 111 \caption{\label{TabVerif} Verification Results } 145 112 \end{table} 146 113 147 114 148 115 149 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. 116 117 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. 150 118 151 119
Note: See TracChangeset
for help on using the changeset viewer.
