Changeset 75

Timestamp:

Mar 27, 2012, 5:24:35 PM (13 years ago)

Author:

syed

Message:

/papers/FDL2012/

Location:

papers/FDL2012

Files:

• FDL2012.tex (modified) (1 diff)
• exp_results.tex (modified) (4 diffs)
• introduction.tex (modified) (2 diffs)

papers/FDL2012/FDL2012.tex

@@ -47 +47 @@
 
 \begin{abstract}
-Embedded systems are usually composed of several components and in practice, these components generally have been independently verified to ensure that they respect their specifications before being integrated into a larger system. Therefore, we would like to exploit the specification (i.e. verified CTL properties) of the components in the objective of verifying a global property of the system. A complete concrete system may not be directly verifiable due to the state explosion problem, thus abstraction and eventually refinement process are required. In this paper, we propose a technique to select properties in order to generate a good abstraction and reduce refinement iterations. We have tested this technique on a set of benchmarks which shows that our approach is promising in comparison to other abstraction-refinement techniques.
+Embedded systems are usually composed of several components and in practice, these components generally have been independently verified to ensure that they respect their specifications before being integrated into a larger system. Therefore, we would like to exploit the specification (i.e. verified CTL properties) of the components in the objective of verifying a global property of the system. A complete concrete system may not be directly verifiable due to the state explosion problem, thus abstraction and eventually refinement process are required. In this paper, we propose a technique to select properties in order to generate a good abstraction and reduce refinement iterations. We have conducted several preliminary experimentations which shows that our approach is promising in comparison to other abstraction-refinement techniques implemented in VIS.
 \end{abstract}
 

papers/FDL2012/exp_results.tex

@@ -21 +21 @@
  Abstract      & 2 Masters-1 Slave  & 301 & 2   &  99   &  4.12317e+11  & 0.02 \\
  Model         & 4 Masters-1 Slave  & 501 & 2   & 147   &  3.45876e+18  & 0.03\\
- for $\phi_1$  & 4 Masters-2 Slaves & xx  & 2   & xxx   &  xxx          & xxxx \\
+ for $\phi_1$  & 4 Masters-2 Slaves & 589 & 2   & 167   &  7.08355e+21  & 0.04 \\
 \midrule 
  Final         & 1 Master-1 Slave   & 194 & 1   & 50    &  2.62144e+07  & 0 \\
  Abstract      & 2 Masters-1 Slave  & 298 & 1   & 73    &  2.14748e+11  & 0.01 \\
  Model         & 4 Masters-1 Slave  & 498 & 1   & 121   &  1.80144e+18  & 0.02 \\
- for $\phi_2$  & 4 Masters-2 Slaves & xxx & x   & xxx   &  xxx          & xxx \\ 
+ for $\phi_2$  & 4 Masters-2 Slaves & 586 & 1   & 141   &  3.68935e+21  & 0.02 \\ 
 \bottomrule  
 \bottomrule
@@ -99 +99 @@
 \midrule
 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}}  \\ 
-                                & Prop. Selection   & 1   &  xxx     \\
- $\phi_1$   & Incremental       & xxx &  xxx         \\
+                                & Prop. Selection   & 1   &  2.2     \\
+ $\phi_1$   & Incremental       & N/A &  >1 day    \\
             & Standard MC       & -   &  2231.3    \\
 \midrule
-            & Prop. Selection   & 0   &  xxx\\
+            & Prop. Selection   & 0   &  1.1\\
  $\phi_2$   & Incremental       & N/A &  >1 day    \\
             & Standard MC       & -   &  12814.1 \\
@@ -115 +115 @@
 
 %\medskip
-
-
-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.
 
 
@@ -143 +140 @@
 \end{table}
 
-\medskip
 
 
+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.
+
+
+
+%\medskip
+
+

papers/FDL2012/introduction.tex

@@ -8 +8 @@
 
 
-In this research we would like to contribute in the improvement of the model-checking technique through the combination of the compositional method and the abstraction-refinement procedure which would allow the verification of complex structured systems and cope with the state space explosion phenomenon. Till now, compositional analysis and abstraction-refinement procedure have been essentially explored seperately, hence the desire to investigate the potential of the combination of these two techniques. The research will lead to a proposal of a development and verification process based on association of several components.
+In this research we would like to contribute to the improvement of the model-checking technique through the combination of the compositional method and the abstraction-refinement procedure which would allow the verification of complex structured systems and cope with the state space explosion phenomenon. Till now, compositional analysis and abstraction-refinement procedure have been essentially explored seperately, hence the desire to investigate the potential of the combination of these two techniques. The research will lead to a proposal of a development and verification process based on association of several components. In this paper we present a strategy to exploit the properties of verified component in the goal of verifying complex systems with a good initial abstraction and eventually being conclusive in minimal refinement iterations. 
 
 
-\subsection{Related Works}
-
+%\subsection{Related Works}
+\emph{Related Works:} 
 We are inspired by the compositional strategy is based on the assume-guarantee reasoning where assumptions are made on other components of the systems when verifying one component. In other words, we show that a component $C_1$ guarantees certain properties $P_1$ on the hypothesis that component $C_2$ provides certain properties $P_2$ and vice-versa for $C_2$. If that's the case, then we can claim that the composition of $C_1$ and $C_2$, both executed in parallel and may interact with each other, guarantees the properties $P_1$ and $P_2$ unconditionally. Several works have manipulated this technique notably in \cite{GrumbergLong91assume_guarantee} where Grumberg and Long described the methodology using a subset of CTL in their framework and later in \cite{HQR98assume_guarantee} where Herzinger and al. presented their successful implementations and case study regarding this approach.
 
@@ -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.
+%\subsection{Contribution}
+\emph{Contribution :} In this paper we present a strategy to exploit the properties of verified component in the goal of verifying complex systems with a good initial abstraction and eventually being conclusive in minimal refinement iterations. 
 
+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 and summarize our possible future works.
+