![(please configure the [header_logo] section in trac.ini)](/trac/verif_tools/chrome/site/your_project_logo.png){kind=logo}
Changeset 83 for papers/FDL2012/exp_results.tex
- Timestamp:
- Apr 5, 2012, 1:59:16 PM (13 years ago)
- File:
-
- 1 edited
-
papers/FDL2012/exp_results.tex (modified) (5 diffs)
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/exp_results.tex
r80 r83 14 14 \midrule 15 15 \midrule 16 & 1 Master-1 Slave & 30 8 & 33 442 & 3.64116e+06 & 41.49\\17 Concrete & 2 Masters-1 Slave & 4 53 & 140297 & 2.42518e+11 & 1922.75\\18 Model & 4 Masters-1 Slave & 7 37 & N/A & N/A & >3days\\19 & 4 Masters-2 Slaves & 911 & N/A & N/A & > 3days\\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 20 \midrule 21 21 \midrule … … 48 48 \midrule 49 49 \midrule 50 Concrete Model & 822 & 1 40586 & 3.7354e+07 & 294.6\\50 Concrete Model & 822 & 161730 & 3.7354e+07 & 300.12 \\ 51 51 \midrule 52 52 \midrule … … 75 75 \multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\ 76 76 & Prop. Selection & 1 & 2.2 \\ 77 $\phi_1$ & Incremental & 0 & 18.1\\78 & Standard MC & - & 14.9\\77 $\phi_1$ & Incremental & 0 & 6.3 \\ 78 & Standard MC & - & 6.06 \\ 79 79 \midrule 80 80 & Prop. Selection & 0 & 1.0 \\ 81 $\phi_2$ & Incremental & 467 & 168.0\\82 & Standard MC & - & 14.9\\81 $\phi_2$ & Incremental & 562 & 200.9 \\ 82 & Standard MC & - & 6.13 \\ 83 83 \midrule 84 84 \midrule 85 85 \multicolumn{4}{l}{\textbf{\underline{2 Masters - 1 Slave :}}} \\ 86 86 & Prop. Selection & 1 & 2.0 \\ 87 $\phi_1$ & Incremental & 0 & 107.7\\88 & Standard MC & - & 1181.8\\87 $\phi_1$ & Incremental & 0 & 20.4 \\ 88 & Standard MC & - & 37.9 \\ 89 89 \midrule 90 90 & Prop. Selection & 0 & 1.0 \\ 91 $\phi_2$ & Incremental & 0 & 108.5\\92 & Standard MC & - & 1103.3\\91 $\phi_2$ & Incremental & 74 & 786.3 \\ 92 & Standard MC & - & 39.4 \\ 93 93 \midrule 94 94 \midrule 95 95 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 1 Slave :}}} \\ 96 & Prop. Selection & 1& 2.1 \\97 $\phi_1$ & Incremental & N/A & >3 days\\98 & Standard MC & - & >3 days\\96 & Prop. Selection & 1 & 2.1 \\ 97 $\phi_1$ & Incremental & 0 & 261.6 \\ 98 & Standard MC & - & >1 day \\ 99 99 \midrule 100 & Prop. Selection & 0 & 1.0\\101 $\phi_2$ & Incremental & N/A & >3 days\\102 & Standard MC & - & >3 days\\100 & Prop. Selection & 0 & 1.0 \\ 101 $\phi_2$ & Incremental & 0 & 263.5 \\ 102 & Standard MC & - & >1 day \\ 103 103 \midrule 104 104 \midrule 105 105 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}} \\ 106 106 & Prop. Selection & 1 & 2.2 \\ 107 $\phi_1$ & Incremental & N/A & > 3 days\\108 & Standard MC & - & > 3 days\\107 $\phi_1$ & Incremental & N/A & >1 day \\ 108 & Standard MC & - & >1 day \\ 109 109 \midrule 110 110 & Prop. Selection & 0 & 1.1\\ 111 $\phi_2$ & Incremental & N/A & > 3 days\\112 & Standard MC & - & > 3 days\\111 $\phi_2$ & Incremental & N/A & >1 day \\ 112 & Standard MC & - & >1 day\\ 113 113 \bottomrule 114 114 \bottomrule … … 132 132 \midrule 133 133 & Prop. Selection & 0 & 1.02 \\ 134 $\phi_3$ & Incremental & N/A & N/A\\135 & Standard MC & - & N/A\\134 $\phi_3$ & Incremental & N/A & >1 day \\ 135 & Standard MC & - & 2645.4 \\ 136 136 \midrule 137 & Prop. Selection & 0 & 1.01 \\138 $\phi_4$ & Incremental & N/A & N/A\\139 & Standard MC & - & N/A\\137 & Prop. Selection & 0 & 1.01 \\ 138 $\phi_4$ & Incremental & N/A & >1 day \\ 139 & Standard MC & - & 1678.1 \\ 140 140 \bottomrule 141 141 … … 147 147 148 148 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.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. 150 150 151 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.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)) \rightarrow AF((s_1=1)*AF(t_1=1)))$ and $\phi_4 = AG(((p'=1)*(q'=1)*AG(r_2=0)) \rightarrow 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 153 154 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.
Note: See TracChangeset
for help on using the changeset viewer.
