![(please configure the [header_logo] section in trac.ini)](/trac/verif_tools/chrome/site/your_project_logo.png){kind=logo}
Changeset 80 for papers/FDL2012/exp_results.tex
- Timestamp:
- Apr 4, 2012, 2:01:08 PM (13 years ago)
- File:
-
- 1 edited
-
papers/FDL2012/exp_results.tex (modified) (6 diffs)
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/exp_results.tex
r75 r80 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 test platforms 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}. 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. 1 We have conducted preliminary experiments to tests and compare the performance of our strategy with existing abstraction-refinement technique available in VIS. There several abstraction-refinement techniques implemented in VIS accessible via \emph{approximate\_model\_check}, \emph{iterative\_model\_check}, \emph{check\_invariant} and \emph{incremental\_ctl\_model\_check} commands. However, among the techniques available, \emph{incremental\_ctl\_model\_check} is the only abstraction-refinement technique 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}. 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. 4 5 6 5 7 \begin{table*} [ht] 6 \hspace*{1 0mm}7 \begin{tabular}{clcccc c}8 \hspace*{17mm} 9 \begin{tabular}{clcccc} 8 10 9 11 \toprule 10 \multicolumn{2}{c}{\textbf{VCI-PI}} & \emph{Number of} & \emph{ FSM} & \emph{BDD} & \emph{Number of } & \emph{Analysis}\\11 \multicolumn{2}{c}{\textbf{Platform}} &\emph{BDD Variables} & \emph{Depth}& \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\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)} \\ 12 14 \midrule 13 15 \midrule 14 & 1 Master-1 Slave & 308 & 599& 33 442 & 3.64116e+06 & 41.49 \\15 Concrete & 2 Masters-1 Slave & 4 39 & 186 & 75 210 & 7.3282e+04 & 14.36\\16 Model & 4 Masters-1 Slave & 7 09 & 408 & 156 657 & 2.15076e+07 & 414.38\\17 & 4 Masters-2 Slaves & 883 & 597 & 217 797 & 3.22215e+10 & 4064.09\\16 & 1 Master-1 Slave & 308 & 33 442 & 3.64116e+06 & 41.49 \\ 17 Concrete & 2 Masters-1 Slave & 453 & 140297 & 2.42518e+11 & 1922.75 \\ 18 Model & 4 Masters-1 Slave & 737 & N/A & N/A & >3days \\ 19 & 4 Masters-2 Slaves & 911 & N/A & N/A & >3days \\ 18 20 \midrule 19 21 \midrule 20 Final & 1 Master-1 Slave & 197 & 2& 76 & 5.03316e+07 & 0.01 \\21 Abstract & 2 Masters-1 Slave & 301 & 2& 99 & 4.12317e+11 & 0.02 \\22 Model & 4 Masters-1 Slave & 501 & 2& 147 & 3.45876e+18 & 0.03\\23 for $\phi_1$ & 4 Masters-2 Slaves & 589 & 2& 167 & 7.08355e+21 & 0.04 \\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 \\ 24 26 \midrule 25 Final & 1 Master-1 Slave & 194 & 1& 50 & 2.62144e+07 & 0 \\26 Abstract & 2 Masters-1 Slave & 298 & 1& 73 & 2.14748e+11 & 0.01 \\27 Model & 4 Masters-1 Slave & 498 & 1& 121 & 1.80144e+18 & 0.02 \\28 for $\phi_2$ & 4 Masters-2 Slaves & 586 & 1& 141 & 3.68935e+21 & 0.02 \\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 \\ 29 31 \bottomrule 30 32 \bottomrule … … 36 38 37 39 40 38 41 \begin{table*} [ht] 39 \hspace*{1 2mm}40 \begin{tabular}{ccccc c}42 \hspace*{15mm} 43 \begin{tabular}{ccccc} 41 44 42 45 \toprule 43 \textbf{CAN Bus} & \emph{Number of} & \emph{FSM}& \emph{BDD} & \emph{Number of } & \emph{Analysis}\\44 \textbf{Platform} &\emph{BDD Variables} & \emph{Depth}& \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\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)} \\ 45 48 \midrule 46 49 \midrule 47 Concrete Model & 838 & 182 & 212550 & 2.87296e+08 & 167.9\\50 Concrete Model & 822 & 140586 & 3.7354e+07 & 294.6 \\ 48 51 \midrule 49 52 \midrule 50 Final Abstract Model for $\phi_1$ & xx & 2 & xxx & xxx & xxxx\\53 Final Abstract Model for $\phi_1$ & 425 & 187 & 1.66005e+12 & 0.03 \\ 51 54 \midrule 52 Final Abstract Model for $\phi_2$ & xx & 2 & xxx & xxx & xxxx\\55 Final Abstract Model for $\phi_2$ & 425 & 187 & 1.66005e+12 & 0.04 \\ 53 56 \bottomrule 54 57 \bottomrule … … 57 60 \caption{\label{StatsCAN_Bus} Statistics on the CAN Bus platform} 58 61 \end{table*} 62 63 59 64 60 65 … … 80 85 \multicolumn{4}{l}{\textbf{\underline{2 Masters - 1 Slave :}}} \\ 81 86 & Prop. Selection & 1 & 2.0 \\ 82 $\phi_1$ & Incremental & 0 & 1.3\\83 & Standard MC & - & 1.5\\87 $\phi_1$ & Incremental & 0 & 107.7 \\ 88 & Standard MC & - & 1181.8 \\ 84 89 \midrule 85 90 & Prop. Selection & 0 & 1.0 \\ 86 $\phi_2$ & Incremental & 0 & 15.3\\87 & Standard MC & - & 14.6\\91 $\phi_2$ & Incremental & 0 & 108.5 \\ 92 & Standard MC & - & 1103.3 \\ 88 93 \midrule 89 94 \midrule 90 95 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 1 Slave :}}} \\ 91 96 & Prop. Selection & 1 & 2.1 \\ 92 $\phi_1$ & Incremental & 0 & 6.8\\93 & Standard MC & - & 175.5\\97 $\phi_1$ & Incremental & N/A & >3 days \\ 98 & Standard MC & - & >3 days \\ 94 99 \midrule 95 100 & Prop. Selection & 0 & 1.0 \\ 96 $\phi_2$ & Incremental & 0 & 7.5\\97 & Standard MC & - & 195.1\\101 $\phi_2$ & Incremental & N/A & >3 days \\ 102 & Standard MC & - & >3 days \\ 98 103 \midrule 99 104 \midrule 100 105 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}} \\ 101 106 & Prop. Selection & 1 & 2.2 \\ 102 $\phi_1$ & Incremental & N/A & > 1 day\\103 & Standard MC & - & 2231.3\\107 $\phi_1$ & Incremental & N/A & >3 days \\ 108 & Standard MC & - & >3 days \\ 104 109 \midrule 105 110 & Prop. Selection & 0 & 1.1\\ 106 $\phi_2$ & Incremental & N/A & > 1 day\\107 & Standard MC & - & 12814.1\\111 $\phi_2$ & Incremental & N/A & >3 days \\ 112 & Standard MC & - & >3 days\\ 108 113 \bottomrule 109 114 \bottomrule … … 126 131 \midrule 127 132 \midrule 128 & Prop. Selection & xxx & xxx\\129 $\phi_3$ & Incremental & N/A & >1 day\\130 & Standard MC & - & 51.9\\133 & Prop. Selection & 0 & 1.02 \\ 134 $\phi_3$ & Incremental & N/A & N/A \\ 135 & Standard MC & - & N/A \\ 131 136 \midrule 132 & Prop. Selection & xxx & xxx\\133 $\phi_4$ & Incremental & 0 & 57.3\\134 & Standard MC & - & 2.2\\137 & Prop. Selection & 0 & 1.01\\ 138 $\phi_4$ & Incremental & N/A & N/A \\ 139 & Standard MC & - & N/A \\ 135 140 \bottomrule 136 141 … … 142 147 143 148 144 In the following tables: Table \ref{TabVCI_PI} and Table \ref{TabCANBus}, we compare the execution time between our technique (Prop. Selection), 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)))$ whereas for the CAN bus platform, the global property $\phi_3$ is the type $AG(((p'=1)*(q'=1)) -> AF((s = 1)*(r = 1))$ and $\phi_4 = AG(((p'=1)*(q'=1)) -> AG(r' = 0))$. We can see that our technique systematically computes faster than the other two methods and interestingly in the case where the size of the platform increases by adding the more connected components, in contrary to the other two methods, our computation time remains stable. 149 In the following tables: Table \ref{TabVCI_PI} and Table \ref{TabCANBus}, we compare the execution time between our technique (Prop. Selection), 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 151 152 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)) -> AF((s_1=1)*AF(t_1=1)))$ and $\phi_4 = AG(((p'=1)*(q'=1)*AG(r_2=0)) -> AG((s_2=0)*(t_2=0)))$. We have at our disposal 103 verified component properties and after the selection process, 3 selected component properties were sufficient to verify both global properties. 153 154 Globally, we can see that our technique systematically computes faster than the other two methods and interestingly in the case where the size of the platform increases by adding the more connected components, in contrary to the other two methods, our computation time remains stable. 145 155 146 156
Note: See TracChangeset
for help on using the changeset viewer.
