Changeset 80 for papers/FDL2012


Ignore:
Timestamp:
Apr 4, 2012, 2:01:08 PM (13 years ago)
Author:
syed
Message:

/papers/FDL2012

Location:
papers/FDL2012
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • papers/FDL2012/FDL2012.tex

    r75 r80  
    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 conducted several preliminary experimentations which shows that our approach is promising in comparison to other abstraction-refinement techniques implemented in VIS.
     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 \cite{ucberkeley96vis}.
    5050\end{abstract}
    5151

  • papers/FDL2012/exp_results.tex

    r75 r80  
    1 We have conducted preliminary experiments to tests and compare the performance of our strategy with existing abstraction-refinement technique available in VIS. As our test platforms requires fairness constraints, we have chosen the \emph{incremental\_ctl\_verification} abstraction refinement technique as it supports CTL formulas and fairness constraints \cite{PardoHachtel98incremCTLMC} \cite{PardoHachtel97autoAbsMC}. It is an automatic abstraction refinement algorithm which generates an initial conservative abstraction principally by reducing the size of the latches by a constant factor. If the initial abstraction is not conclusive, a \emph{goal set} will then be computed in order to guide the refinement process.
     1We have conducted preliminary experiments to tests and compare the performance of our strategy with existing abstraction-refinement technique available in VIS. There several abstraction-refinement techniques implemented in VIS accessible via \emph{approximate\_model\_check}, \emph{iterative\_model\_check}, \emph{check\_invariant} and \emph{incremental\_ctl\_model\_check} commands. However, among the techniques available, \emph{incremental\_ctl\_model\_check} is the only abstraction-refinement technique that supports CTL formulas and fairness constraints which are necessary in our test platforms. It is an automatic abstraction refinement algorithm which generates an initial conservative abstraction principally by reducing the size of the latches by a constant factor. If the initial abstraction is not conclusive, a \emph{goal set} will then be computed in order to guide the refinement process \cite{PardoHachtel98incremCTLMC} \cite{PardoHachtel97autoAbsMC}.
     2
    23
    34We have executed and compared the execution time and the number of refinement iterations for two examples: VCI-PI platform consisting of Virtual Component Interface (VCI), a PI-Bus and VCI-PI protocol converter and a simplified version of a CAN bus platform consisting of 3 nodes on a CAN bus. Table \ref{StatsVCI_PI} and Table \ref{StatsCAN_Bus} give the size and the statistics concerning the VCI-PI platform and CAN bus platform respectively. All the values are obtained using the \emph{compute\_reach} command with option \emph{-v 1} in VIS except the number of BDD variables, computed using the \emph{print\_bdd\_stats} command. The experiments have been executed on a PC with an AMD Athlon dual-core processor 4450e and 1.8GB of RAM memory.
    45
     6
    57\begin{table*} [ht]
    6 \hspace*{10mm}
    7 \begin{tabular}{clccccc}
     8\hspace*{17mm}
     9\begin{tabular}{clcccc}
    810
    911\toprule
    10 \multicolumn{2}{c}{\textbf{VCI-PI}}   & \emph{Number of}      & \emph{FSM}    & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\
    11 \multicolumn{2}{c}{\textbf{Platform}} &\emph{BDD Variables}  & \emph{Depth} & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
     12\multicolumn{2}{c}{\textbf{VCI-PI}}   & \emph{Number of}      & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\
     13\multicolumn{2}{c}{\textbf{Platform}} &\emph{BDD Variables}  & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
    1214\midrule
    1315\midrule
    14                & 1 Master-1 Slave   & 308 & 599 & 33 442   & 3.64116e+06 & 41.49 \\
    15  Concrete      & 2 Masters-1 Slave  & 439 & 186 & 75 210   & 7.3282e+04  & 14.36 \\
    16   Model        & 4 Masters-1 Slave  & 709 & 408 & 156 657  & 2.15076e+07 & 414.38 \\
    17                & 4 Masters-2 Slaves & 883 & 597 & 217 797  & 3.22215e+10 & 4064.09 \\
     16               & 1 Master-1 Slave   & 308 & 33 442   & 3.64116e+06 & 41.49 \\
     17 Concrete      & 2 Masters-1 Slave  & 453  & 140297   & 2.42518e+11 & 1922.75 \\
     18  Model        & 4 Masters-1 Slave  & 737  & N/A      & N/A         & >3days \\
     19               & 4 Masters-2 Slaves & 911  & N/A      & N/A         & >3days \\
    1820 \midrule
    1921 \midrule
    20  Final         & 1 Master-1 Slave   & 197 & 2  &  76   &  5.03316e+07  & 0.01 \\
    21  Abstract      & 2 Masters-1 Slave  & 301 & 2  &  99   &  4.12317e+11  & 0.02 \\
    22  Model         & 4 Masters-1 Slave  & 501 & 2  & 147   &  3.45876e+18  & 0.03\\
    23  for $\phi_1$  & 4 Masters-2 Slaves & 589 & 2  & 167   &  7.08355e+21  & 0.04 \\
     22 Final         & 1 Master-1 Slave   & 197 &  76   &  5.03316e+07  & 0.01 \\
     23 Abstract      & 2 Masters-1 Slave  & 301 &  99   &  4.12317e+11  & 0.02 \\
     24 Model         & 4 Masters-1 Slave  & 501 & 147   &  3.45876e+18  & 0.03\\
     25 for $\phi_1$  & 4 Masters-2 Slaves & 589 & 167   &  7.08355e+21  & 0.04 \\
    2426\midrule
    25  Final         & 1 Master-1 Slave   & 194 & 1  & 50    &  2.62144e+07  & 0 \\
    26  Abstract      & 2 Masters-1 Slave  & 298 & 1  & 73    &  2.14748e+11  & 0.01 \\
    27  Model         & 4 Masters-1 Slave  & 498 & 1  & 121   &  1.80144e+18  & 0.02 \\
    28  for $\phi_2$  & 4 Masters-2 Slaves & 586 & 1  & 141   &  3.68935e+21  & 0.02 \\
     27 Final         & 1 Master-1 Slave   & 194 & 50    &  2.62144e+07  & 0 \\
     28 Abstract      & 2 Masters-1 Slave  & 298 & 73    &  2.14748e+11  & 0.01 \\
     29 Model         & 4 Masters-1 Slave  & 498 & 121   &  1.80144e+18  & 0.02 \\
     30 for $\phi_2$  & 4 Masters-2 Slaves & 586 & 141   &  3.68935e+21  & 0.02 \\
    2931\bottomrule 
    3032\bottomrule
    … …  
    3638
    3739
     40
    3841\begin{table*} [ht]
    39 \hspace*{12mm}
    40 \begin{tabular}{cccccc}
     42\hspace*{15mm}
     43\begin{tabular}{ccccc}
    4144
    4245\toprule
    43 \textbf{CAN Bus}      & \emph{Number of}      & \emph{FSM}    & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\
    44 \textbf{Platform}     &\emph{BDD Variables}  & \emph{Depth}  & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
     46\textbf{CAN Bus}      & \emph{Number of}      & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\
     47\textbf{Platform}     &\emph{BDD Variables}    & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
    4548\midrule
    4649\midrule
    47  Concrete Model   & 838     & 182     & 212550    & 2.87296e+08      & 167.9 \\     
     50 Concrete Model                     & 822     & 140586      & 3.7354e+07     & 294.6 \\     
    4851 \midrule
    4952 \midrule
    50  Final Abstract Model for $\phi_1$  & xx  & 2   & xxx   &  xxx       & xxxx \\
     53 Final Abstract Model for $\phi_1$  & 425   & 187   &  1.66005e+12       & 0.03 \\
    5154\midrule
    52  Final Abstract Model for $\phi_2$  & xx  & 2   & xxx   &  xxx       & xxxx \\
     55 Final Abstract Model for $\phi_2$  & 425   & 187   &  1.66005e+12       & 0.04 \\
    5356\bottomrule 
    5457\bottomrule
    … …  
    5760\caption{\label{StatsCAN_Bus} Statistics on the CAN Bus platform}
    5861\end{table*}
     62
     63
    5964
    6065
    … …  
    8085\multicolumn{4}{l}{\textbf{\underline{2 Masters - 1 Slave :}}}   \\   
    8186                 & Prop. Selection   & 1    &    2.0     \\
    82  $\phi_1$   & Incremental       & 0    &    1.3        \\
    83             & Standard MC       & -    &    1.5     \\
     87 $\phi_1$   & Incremental       & 0    &  107.7        \\
     88            & Standard MC       & -    & 1181.8     \\
    8489\midrule
    8590                 & Prop. Selection   & 0    &    1.0    \\
    86  $\phi_2$   & Incremental       & 0    &   15.3       \\
    87                  & Standard MC       & -    &   14.6    \\
     91 $\phi_2$   & Incremental       & 0    &  108.5       \\
     92                 & Standard MC       & -    & 1103.3   \\
    8893\midrule
    8994\midrule 
    9095\multicolumn{4}{l}{\textbf{\underline{4 Masters - 1 Slave :}}}   \\
    9196                 & Prop. Selection   & 1    &    2.1     \\
    92  $\phi_1$   & Incremental       & 0    &    6.8        \\
    93             & Standard MC       & -    &  175.5     \\
     97 $\phi_1$   & Incremental       & N/A  & >3 days        \\
     98            & Standard MC       & -    & >3 days     \\
    9499\midrule
    95100                 & Prop. Selection   &  0    &   1.0 \\
    96  $\phi_2$   & Incremental       &  0    &   7.5    \\
    97                  & Standard MC       &  -    & 195.1 \\
     101 $\phi_2$   & Incremental       &  N/A  &  >3 days   \\
     102                 & Standard MC       &  -    & >3 days \\
    98103\midrule
    99104\midrule
    100105\multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}}  \\
    101106                                & Prop. Selection   & 1   &  2.2     \\
    102  $\phi_1$   & Incremental       & N/A &  >1 day    \\
    103             & Standard MC       & -   &  2231.3    \\
     107 $\phi_1$   & Incremental       & N/A &  >3 days    \\
     108            & Standard MC       & -   &  >3 days   \\
    104109\midrule
    105110            & Prop. Selection   & 0   &  1.1\\
    106  $\phi_2$   & Incremental       & N/A &  >1 day    \\
    107             & Standard MC       & -   &  12814.1 \\
     111 $\phi_2$   & Incremental       & N/A &  >3 days    \\
     112            & Standard MC       & -   &  >3 days\\
    108113\bottomrule       
    109114\bottomrule
    … …  
    126131\midrule
    127132\midrule
    128                  & Prop. Selection  &  xxx        &  xxx     \\
    129  $\phi_3$   & Incremental      & N/A            &  >1 day \\
    130                  & Standard MC      & -                         &  51.9    \\
     133                 & Prop. Selection  &  0          &  1.02     \\
     134 $\phi_3$   & Incremental      & N/A            &  N/A \\
     135                 & Standard MC      & -                         &  N/A    \\
    131136\midrule
    132                  & Prop. Selection   &  xxx       &  xxx \\
    133  $\phi_4$   & Incremental       & 0          &   57.3     \\
    134                  & Standard MC       & -          &    2.2    \\
     137                 & Prop. Selection   &  0         &   1.01\\
     138 $\phi_4$   & Incremental       & N/A        &   N/A     \\
     139                 & Standard MC       & -          &   N/A    \\
    135140\bottomrule
    136141
    … …  
    142147
    143148
    144 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.
     149In 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. 
     150
     151
     152In 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.
     153
     154Globally, 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.
    145155
    146156

  • papers/FDL2012/introduction.tex

    r78 r80  
    1 The embedded systems correspond to the integration into the same electronic circuit, a huge number of complex functionalities performed by several heterogenous components. Current SoC (System on Chips) contain multiple processors executing numerous cooperating tasks, specialized co-processors (for particular data treatment or communication purposes), Radio-Frequency components, etc. These systems are usually submitted to safety and robustness requirements.  Depending on their application domains, their failure may induce serious damages. Generally failures on these systems are unacceptable and have to be avoided.
     1The embedded systems correspond to the integration into the same electronic circuit, a huge number of complex functionalities performed by several heterogenous components. Current SoC (System on Chips) contain multiple processors executing numerous cooperating tasks, specialized co-processors (for particular data treatment or communication purposes), Radio-Frequency components, etc. These systems are usually submitted to safety and robustness requirements. Depending on their application domains, their failure may induce serious damages and catastrophic consequences.
    22
    33
    … …  
    1010
    1111%\subsection{Related Works}
    12 \emph{Related Works:} A strategy to overcome the state explosion problem is by abstraction. A method for the construction of  an abstract state graph of an arbitrary system automatically was proposed by Graf and Saidi \cite{GrafSaidi97abstract_construct} using Pvs theorem prover. Here, the abstract states are generated from the valuations of a set of predicates on the concrete variables. The construction approach is automatic and incremental.
     12A strategy to overcome the state explosion problem is by performing abstraction. A method for the construction of an abstract state graph of an arbitrary system automatically was first proposed by Graf and Saidi \cite{GrafSaidi97abstract_construct} using Pvs theorem prover. Here, the abstract states are generated from the valuations of a set of predicates on the concrete variables. The construction approach is automatic and incremental.
    1313
    1414
    15 A few years later, an interesting abstraction-refinement methodology called counterexample-guided abstraction refinement (CEGAR) was proposed by Clarke and al. \cite{clarke00cegar}. The abstraction was done by generating an abstract model of the system by considering only the variables that possibly have a role in verifying a particular property. In this technique, the counterexample provided by the model-checker in case of failure is used to refine the system.
     15In 2000, an interesting abstraction-refinement methodology called counterexample-guided abstraction refinement (CEGAR) was proposed by Clarke and al. \cite{clarke00cegar}. The abstraction was done by generating an abstract model of the system by considering only the variables that possibly have a role in verifying a particular property. In this technique, the counterexample provided by the model-checker in case of failure is used to refine the system.
    1616
    1717
    18 Several tools using counterexample-guided abstraction refinement technique have been developed such as SLAM, a software model-checker by Microsoft Research \cite{microsoft04SLAM}, BLAST (Berkeley Lazy Abstraction Software Verification Tool), a software model-checker for C programs \cite{berkeley07BLAST} and VCEGAR (Verilog Counterexample Guided Abstraction Refinement), a hardware model-checker which performs verification at the RTL (Register Transfer Language) level \cite{Kroening_al07vcegar}.
     18Several tools using counterexample-guided abstraction refinement technique have been developed such as SLAM, a software model-checker by Microsoft Research \cite{microsoft04SLAM}, BLAST (Berkeley Lazy Abstraction Software Verification Tool), a software model-checker for C programs \cite{berkeley07BLAST} and VCEGAR (Verilog Counterexample Guided Abstraction Refinement), a hardware model-checker which performs verification at the RTL (Register Transfer Language) level \cite{Kroening_al07vcegar}. However, relying on counterexamples generated by the model checker as the only source for refinement may not be conclusive.
    1919
    2020
    21 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, it is shown 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 this is 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.
     21An alternative method to get over the state explosion problem is the compositional strategy. The 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, it is shown 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 this is 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.
    2222
    2323
    24 
    25 Xie and Browne have proposed a method for software verification based on composition of several components \cite{XieBrowne03composition_soft}. Their main objective is developing components that could be reused with certitude that their behaviors will always respect their specification when associated in a proper composition. Therefore, temporal properties of the software are specified, verified and packaged with the component for possible reuse. The implementation of this approach on software have been succesful and the application of the assume-guarantee reasoning has considerably reduced the model checking complexity.
     24\textbf{\emph{Related Works:}} Xie and Browne have proposed a method for software verification based on composition of several components \cite{XieBrowne03composition_soft}. Their main objective is developing components that could be reused with certitude that their behaviors will always respect their specification when associated in a proper composition. Therefore, temporal properties of the software are specified, verified and packaged with the component for possible reuse. The implementation of this approach on software have been succesful and the application of the assume-guarantee reasoning has considerably reduced the model checking complexity.
    2625
    2726
    … …  
    4140
    4241%\subsection{Contribution}
    43 \emph{Contribution :} 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.
     42\textbf{\emph{Contribution :}} 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.
    4443
    4544In 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.
Note: See TracChangeset for help on using the changeset viewer.