![(please configure the [header_logo] section in trac.ini)](/trac/verif_tools/chrome/site/your_project_logo.png){kind=logo}
Changeset 71 for papers/FDL2012/exp_results.tex
- Timestamp:
- Mar 22, 2012, 7:15:07 PM (13 years ago)
- File:
-
- 1 edited
-
papers/FDL2012/exp_results.tex (modified) (3 diffs)
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/exp_results.tex
r66 r71 1 1 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}. 2 3 2 4 3 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. 5 4 6 5 7 \medskip 6 \begin{table*} [ht] 7 \hspace*{10mm} 8 \begin{tabular}{clccccc} 9 10 \toprule 11 \multicolumn{2}{c}{\textbf{VCI-PI}} & \emph{Number of} & \emph{FSM} & \emph{BDD} & \emph{Number of } & \emph{Analysis}\\ 12 \multicolumn{2}{c}{\textbf{Platform}} &\emph{BDD Variables} & \emph{Depth} & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\ 13 \midrule 14 \midrule 15 & 1 Master-1 Slave & 308 & 599 & 33 442 & 3.64116e+06 & 41.49 \\ 16 Concrete & 2 Masters-1 Slave & 439 & 186 & 75 210 & 73282 & 14.36 \\ 17 Model & 4 Masters-1 Slave & 709 & 408 & 156 657 & 2.15076e+07 & 414.38 \\ 18 & 4 Masters-2 Slaves & 883 & 597 & 217 797 & 3.22215e+10 & 4064.09 \\ 19 \midrule 20 \midrule 21 Final & 1 Master-1 Slave & 197 & 2 & 76 & 5.03316e+07 & 0.01 \\ 22 Abstract & 2 Masters-1 Slave & 301 & 2 & 99 & 4.12317e+11 & 0.02 \\ 23 Model & 4 Masters-1 Slave & 501 & 2 & 147 & 3.45876e+18 & 0.03\\ 24 for $\phi_1$ & 4 Masters-2 Slaves & xx & 2 & xxx & xxx & xxxx \\ 25 \midrule 26 Final & 1 Master-1 Slave & 194 & 1 & 50 & 2.62144e+07 & 0 \\ 27 Abstract & 2 Masters-1 Slave & 298 & 1 & 73 & 2.14748e+11 & 0.01 \\ 28 Model & 4 Masters-1 Slave & 498 & 1 & 121 & 1.80144e+18 & 0.02 \\ 29 for $\phi_2$ & 4 Masters-2 Slaves & xxx & x & xxx & xxx & xxx \\ 30 \bottomrule 31 \bottomrule 32 \end{tabular} 33 34 \caption{\label{StatsVCI_PI} Statistics on the VCI-PI platform} 35 \end{table*} 36 %\medskip 37 38 39 \begin{table*} [ht] 40 \hspace*{12mm} 41 \begin{tabular}{cccccc} 42 43 \toprule 44 \textbf{CAN Bus} & \emph{Number of} & \emph{FSM} & \emph{BDD} & \emph{Number of } & \emph{Analysis}\\ 45 \textbf{Platform} &\emph{BDD Variables} & \emph{Depth} & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\ 46 \midrule 47 \midrule 48 Concrete Model & 838 & 182 & 212550 & 2.87296e+08 & 167.9 \\ 49 \midrule 50 \midrule 51 Final Abstract Model for $\phi_1$ & xx & 2 & xxx & xxx & xxxx \\ 52 \midrule 53 Final Abstract Model for $\phi_2$ & xx & 2 & xxx & xxx & xxxx \\ 54 \bottomrule 55 \bottomrule 56 \end{tabular} 57 58 \caption{\label{StatsCAN_Bus} Statistics on the CAN Bus platform} 59 \end{table*} 60 8 61 9 62 \begin{table} [h] … … 12 65 13 66 \toprule 14 \ textbf{VCI} & \emph{Verification} & \emph{Verification} & \emph{Refinement} \\15 \textbf{-PI}& \emph{Technique} & \emph{Time (s)} & \emph{Iteration} \\ 67 \emph{Global} &\emph{Verification} & \emph{Refinement} & \emph{Verif.} \\ 68 \emph{Property} & \emph{Technique} & \emph{Iteration} & \emph{Time (s)} \\ 16 69 \midrule 17 70 \midrule 18 & Prop. Selection & 2.2 & 1 \\ 19 $\phi_1$ & Incremental & 18.1 & 0 \\ 20 & Standard MC & 14.9 & - \\ 71 \multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\ 72 & Prop. Selection & 1 & 2.2 \\ 73 $\phi_1$ & Incremental & 0 & 18.1 \\ 74 & Standard MC & - & 14.9 \\ 21 75 \midrule 22 & Prop\_Selection & 1.0 & 0 \\ 23 $\phi_2$ & Incremental & 168.0 & 467 \\ 24 & Standard MC & 14.9 & - \\ 76 & Prop. Selection & 0 & 1.0 \\ 77 $\phi_2$ & Incremental & 467 & 168.0 \\ 78 & Standard MC & - & 14.9 \\ 79 \midrule 80 \midrule 81 \multicolumn{4}{l}{\textbf{\underline{2 Masters - 1 Slave :}}} \\ 82 & Prop. Selection & 1 & 2.0 \\ 83 $\phi_1$ & Incremental & 0 & 1.3 \\ 84 & Standard MC & - & 1.5 \\ 85 \midrule 86 & Prop. Selection & 0 & 1.0 \\ 87 $\phi_2$ & Incremental & 0 & 15.3 \\ 88 & Standard MC & - & 14.6 \\ 89 \midrule 90 \midrule 91 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 1 Slave :}}} \\ 92 & Prop. Selection & 1 & 2.1 \\ 93 $\phi_1$ & Incremental & 0 & 6.8 \\ 94 & Standard MC & - & 175.5 \\ 95 \midrule 96 & Prop. Selection & 0 & 1.0 \\ 97 $\phi_2$ & Incremental & 0 & 7.5 \\ 98 & Standard MC & - & 195.1 \\ 99 \midrule 100 \midrule 101 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}} \\ 102 & Prop. Selection & 1 & xxx \\ 103 $\phi_1$ & Incremental & xxx & xxx \\ 104 & Standard MC & - & 2231.3 \\ 105 \midrule 106 & Prop. Selection & 0 & xxx\\ 107 $\phi_2$ & Incremental & N/A & >1 day \\ 108 & Standard MC & - & 12814.1 \\ 109 \bottomrule 25 110 \bottomrule 26 111 27 112 \end{tabular} 28 113 29 \caption{\label{TabVCI_PI} Results on VCI-PI platform }114 \caption{\label{TabVCI_PI} Results on the VCI-PI platform } 30 115 \end{table} 31 116 … … 34 119 \begin{table} [h] 35 120 %\hspace*{-8mm} 36 \begin{tabular}{ cccc}121 \begin{tabular}{lcccc} 37 122 38 123 \toprule 39 \ textbf{CAN} & \emph{Verification} & \emph{Verification} & \emph{Refinement}\\40 \ textbf{Bus} & \emph{Technique} & \emph{Time (s)} & \emph{Iteration}\\124 \emph{Global} & \emph{Verification} & \emph{Refinement} & \emph{Verif.} \\ 125 \emph{Property} & \emph{Technique} & \emph{Iteration} & \emph{Time (s)} \\ 41 126 \midrule 42 127 \midrule 43 & Prop. Selection & &\\44 $\phi_ 1$ & Incremental & >1 day & 0\\45 & Standard MC & 51.9 & -\\128 & Prop. Selection & xxx & xxx \\ 129 $\phi_3$ & Incremental & N/A & >1 day \\ 130 & Standard MC & - & 51.9 \\ 46 131 \midrule 47 & Prop\_Selection & &\\48 $\phi_ 2$ & Incremental & 57.3 & 0\\49 & Standard MC & 2.2 & -\\132 & Prop. Selection & xxx & xxx \\ 133 $\phi_4$ & Incremental & 0 & 57.3 \\ 134 & Standard MC & - & 2.2 \\ 50 135 \bottomrule 51 136 52 137 \end{tabular} 53 138 54 \caption{\label{TabCANBus} Results on CAN Bus platform }139 \caption{\label{TabCANBus} Results on the CAN Bus platform } 55 140 \end{table} 56 141
Note: See TracChangeset
for help on using the changeset viewer.
