Changeset 74 for papers/FDL2012/exp_results.tex

Timestamp:

Mar 26, 2012, 3:46:26 PM (13 years ago)

Author:

syed

Message:

/papers/FDL2012/

File:

• papers/FDL2012/exp_results.tex (modified) (1 diff)

papers/FDL2012/exp_results.tex

@@ -117 +117 @@
 
 
-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. 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.
+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.