Changeset 75 for papers


Ignore:
Timestamp:
Mar 27, 2012, 5:24:35 PM (13 years ago)
Author:
syed
Message:

/papers/FDL2012/

Location:
papers/FDL2012
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • papers/FDL2012/FDL2012.tex

    r66 r75  
    4747
    4848\begin{abstract}
    49 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.
     49Embedded 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.
    5050\end{abstract}
    5151
  • papers/FDL2012/exp_results.tex

    r74 r75  
    2121 Abstract      & 2 Masters-1 Slave  & 301 & 2   &  99   &  4.12317e+11  & 0.02 \\
    2222 Model         & 4 Masters-1 Slave  & 501 & 2   & 147   &  3.45876e+18  & 0.03\\
    23  for $\phi_1$  & 4 Masters-2 Slaves & xx  & 2   & xxx   &  xxx          & xxxx \\
     23 for $\phi_1$  & 4 Masters-2 Slaves & 589 & 2   & 167   &  7.08355e+21  & 0.04 \\
    2424\midrule
    2525 Final         & 1 Master-1 Slave   & 194 & 1   & 50    &  2.62144e+07  & 0 \\
    2626 Abstract      & 2 Masters-1 Slave  & 298 & 1   & 73    &  2.14748e+11  & 0.01 \\
    2727 Model         & 4 Masters-1 Slave  & 498 & 1   & 121   &  1.80144e+18  & 0.02 \\
    28  for $\phi_2$  & 4 Masters-2 Slaves & xxx & x   & xxx   &  xxx          & xxx \\
     28 for $\phi_2$  & 4 Masters-2 Slaves & 586 & 1   & 141   &  3.68935e+21  & 0.02 \\
    2929\bottomrule 
    3030\bottomrule
     
    9999\midrule
    100100\multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}}  \\
    101                                 & Prop. Selection   & 1   &  xxx     \\
    102  $\phi_1$   & Incremental       & xxx &  xxx         \\
     101                                & Prop. Selection   & 1   &  2.2     \\
     102 $\phi_1$   & Incremental       & N/A &  >1 day    \\
    103103            & Standard MC       & -   &  2231.3    \\
    104104\midrule
    105             & Prop. Selection   & 0   &  xxx\\
     105            & Prop. Selection   & 0   &  1.1\\
    106106 $\phi_2$   & Incremental       & N/A &  >1 day    \\
    107107            & Standard MC       & -   &  12814.1 \\
     
    115115
    116116%\medskip
    117 
    118 
    119 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.
    120117
    121118
     
    143140\end{table}
    144141
    145 \medskip
    146142
    147143
     144In 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.
     145
     146
     147
     148%\medskip
     149
     150
  • papers/FDL2012/introduction.tex

    r74 r75  
    88
    99
    10 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.
     10In 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.
    1111
    1212
    13 \subsection{Related Works}
    14 
     13%\subsection{Related Works}
     14\emph{Related Works:}
    1515We 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.
    1616
     
    4141
    4242
    43 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.
     43%\subsection{Contribution}
     44\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.
    4445
     46In 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.
     47
Note: See TracChangeset for help on using the changeset viewer.