Changeset 74

Timestamp:

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

Author:

syed

Message:

/papers/FDL2012/

Location:

papers/FDL2012

Files:

• exp_results.tex (modified) (1 diff)
• introduction.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.
 
 

papers/FDL2012/introduction.tex

@@ -41 +41 @@
 
 
+In the next section, we will give an overview of our framework and introduce the notations that will be used later. The rest of the paper is organized as follows: section 3 details our strategy of refinement. Section 4 presents the experimentation results and finally, section 5 draws the conclusions.
+