Ignore:
Timestamp:
Apr 6, 2012, 10:37:41 PM (13 years ago)
Author:
syed
Message:

/papers/FDL2012/

File:
1 edited

Legend:

Unmodified
Added
Removed

  • papers/FDL2012/exp_results.tex

    r89 r92  
    11We have conducted preliminary experiments to test and compare the performance
    2 of our strategy with existing abstraction-refinement techniques available in
     2of our strategy with existing techniques available in
    33VIS. There are several abstraction-refinement techniques implemented in VIS
    44accessible via \emph{approximate\_model\_check},
    55\emph{iterative\_model\_check}, \emph{check\_invariant} and
    6 \emph{incremental\_ctl\_model\_check} commands. However, among the available
    7 techniques, \emph{incremental\_ctl\_model\_check} is the only one 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}.
     6\emph{incremental\_ctl\_verification} commands. However, among the available
     7techniques, \emph{incremental\_ctl\_verification} is the only one 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}.
    88
    99
    … …  
    1818\toprule
    1919\multicolumn{3}{l}{\textbf{Experiment}}   & \emph{Number of}      & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\
    20 \multicolumn{3}{l}{\textbf{Platform}} &\emph{BDD Variables}   & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
     20\multicolumn{3}{l}{\textbf{Platform}}     &\emph{BDD Variables}   & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
    2121\midrule
    2222\midrule
    … …  
    2424                        & Concrete      & 2 Masters-1 Slave  & 445  & 24406    & 7.71723e+06 & 35.2 \\
    2525                        &  Model        & 4 Masters-1 Slave  & 721  & 84118    & 3.17332e+12 & 2818.3 \\
    26                         &                & 4 Masters-2 Slaves & 911  & N/A      & N/A         & >1 day \\
     26                        &               & 4 Masters-2 Slaves & 895  & 238990   & 5.708e+15   & 68882.3\footnotemark[1] \\
    2727\cline{2-7}
    2828\cline{2-7}
    … …  
    3636                        & Model         & 4 Masters-1 Slave  & 498  & 121   &  1.80144e+18  & 0.02 \\
    3737                        & for $\phi_2$  & 4 Masters-2 Slaves & 586  & 141   &  3.68935e+21  & 0.02 \\
    38  \midrule
     38% \midrule
    3939 \midrule
    40                         &\multicolumn{2}{c}{Concrete Model}                                      & 822     & 161730      & 3.7354e+07     & 300.12 \\     
     40                        &\multicolumn{2}{c}{Concrete Model}                                          & 822     & 161730      & 3.7354e+07     & 300.12 \\     
    4141\cline{2-7}
    4242\cline{2-7}
    … …  
    4545                        &\multicolumn{2}{c}{Final Abstract Model for $\phi_4$}  & 425   & 187   &  1.66005e+12       & 0.04 \\
    4646\bottomrule 
    47 \bottomrule
     47%\bottomrule
     48
    4849\end{tabular}
    4950
    … …  
    5152\end{table*}
    5253
     54%\footnotetext[1]{Computed on a calculation server.}
    5355
    5456
    … …  
    7274                                &                 & Standard MC       & -    &    6.13      \\
    7375\midrule   
    74 \midrule
     76%\midrule
    7577                                &                 & Prop. Select.   & 1    &    2.0     \\
    7678VCI-PI:                 & $\phi_1$   & Incremental       & 0    &   20.4        \\
    … …  
    8183                                &                 & Standard MC       & -    &   39.4    \\
    8284\midrule
    83 \midrule 
     85%\midrule 
    8486
    8587                                &                 & Prop. Select.   &  1   &    2.1     \\
    … …  
    9193                                &                 & Standard MC       &  -   &   >1 day   \\
    9294\midrule
    93 \midrule
     95%\midrule
    9496
    9597                                &                                & Prop. Select.   & 1          &  2.2     \\
    … …  
    101103                                &            & Standard MC       & -    &  >1 day\\
    102104\midrule
    103 \midrule
     105%\midrule
    104106                &                 & Prop. Select.   &  0     &  1.02     \\
    105107                                &$\phi_3$    & Incremental       & N/A    &  >1 day   \\
    … …  
    111113
    112114\bottomrule       
    113 \bottomrule
     115%\bottomrule
    114116
    115117\end{tabular}
    … …  
    117119\caption{\label{TabVerif} Verification Results  }
    118120\end{table}
    119 
    120 
    121121
    122122
    … …  
    128128$\phi_1$ is the type $AF((p=1)*AF(q=1))$ and $\phi_2$ is actually a stronger
    129129version of the same formula with $AG(AF((p=1)*AF(q=1)))$. We have a total of
    130 27 verifed components properties to be selected in VCI-PI plateform.
     13026 verifed components properties to be selected in VCI-PI plateform.
    131131In comparison to $\phi_2$, we can see that, a better set of properties available will result in a better abstraction and less refinement iterations. 
    132132
Note: See TracChangeset for help on using the changeset viewer.