Changeset 92 for papers


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

/papers/FDL2012/

Location:
papers/FDL2012
Files:
8 edited

Legend:

Unmodified
Added
Removed

  • papers/FDL2012/FDL2012.tex

    r91 r92  
    3434
    3535 \title{ An efficient refinement strategy exploiting components' properties in a CEGAR process}
    36 % \name{Syed Hussein S. ALWI, Emmanuelle ENCRENAZ and C\'{e}cile BRAUNSTEIN}
     36% \name{Syed Hussein S. ALWI, C\'{e}cile BRAUNSTEIN and Emmanuelle ENCRENAZ}
    3737% \thanks{This work was supported by...}}
    3838% \address{Universit\'{e} Pierre et Marie Curie Paris 6, \\
    … …  
    106106Kroening \cite{pwk2009-date} could help us in this direction.
    107107
    108 
     108%footnote for Table 1
     109\footnotetext[1]{Computed on a calculation server.}
    109110
    110111%\begin{thebibliography}

  • papers/FDL2012/abstraction_refinement.tex

    r89 r92  
    88
    99\begin{definition} An efficient \emph{refinement} verifies the following properties:
     10\vspace*{-2mm}
    1011\begin{enumerate}
     12\itemsep -0.3em
    1113\item The new refinement is an over-approximation of the concrete model:
    1214$\widehat{M} \sqsubseteq \widehat{M}_{i+1}$.
    … …  
    4648\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of  length $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
    4749\rightarrow s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$.
     50%\vspace*{-2mm}
    4851\begin{itemize}
     52%\topsep 0pt
     53\itemsep -0.3em
    4954\item All its variables are concrete: $\forall s_i$ and $\forall p\in
    5055\widehat{AP}_i$, $p$ is either true or false according to $\widehat{L_i}$.
    … …  
    6671\widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}},
    6772\widehat{F}_{\overline{\sigma}} \rangle$ is such that :
     73\vspace*{-2mm}
    6874\begin{itemize}
     75%\topsep 0pt
     76\itemsep -0.3em
    6977\item $AP_{\overline{\sigma}} = {AP}_i$:
    7078The set of atomic propositions coincides with the one of $\sigma$

  • 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

  • papers/FDL2012/framework.tex

    r89 r92  
    4343%   \includegraphics[width=1.2\textwidth]{our_CEGAR_Loop_Enhanced_2S_PNG}
    4444%     \hspace*{-5mm}
    45      \includegraphics{our_framework_cegar_png}
     45     \includegraphics[scale=0.37]{our_framework_cegar_png}
    4646   \caption{\label{cegar} Verification Process }
    4747\end{figure}
    4848
     49\vspace*{-5mm}
    4950\subsection{Concrete system definition}
    5051As mentioned earlier, our concrete model consists of several components and each
    … …  
    5455\begin{definition}
    5556A \emph{Moore machine} $C$ is defined by a tuple $\langle I, O, R,$ $\delta, \lambda, \mathbf{R}_0 \rangle$, where,
    56 \begin{itemize}
     57\vspace*{-2mm}
     58\begin{itemize}
     59%\partopsep= -1.0em
     60%\topsep -0.5em
     61\itemsep -0.3em
    5762\item $I$ is a finite set of Boolean inputs signals.
    5863\item $O$ is a finite set of Boolean outputs signals.
    … …  
    104109$AP$, An \emph{Abstract Kripke Structure}, $AKS(\varphi) =(AP, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ is a 6-tuple consisting of:
    105110
    106 \begin{itemize}
     111\vspace*{-3mm}
     112\begin{itemize}
     113%\partopsep=0pt
     114%\topsep 0pt
     115\itemsep -0.3em
    107116\item { $AP$ : The finite set of atomic propositions of property $\varphi$ }   
    108117\item { $\widehat{S}$ : a finite set of states}
    … …  
    116125%\bigskip
    117126
     127\vspace*{-2mm}
    118128We denote by $\widehat{L}(s)$ the configuration of atomic propositions in state $s$ and by $\widehat{L}(s)[p]$ the projection of configuration $\widehat{L}(s)$ according to atomic proposition $p$.
    119129
    … …  
    129139let $C_j$ be a component of the concrete model $M$ and $\varphi_{j}^k$ is a CTL formula describing a satisfied property of component $C_j$. Let $AKS (\varphi_{C_j^k})$ the AKS generated from $\varphi_j^k$. We have $\forall j \in [1,n]$ and $\forall k \in [1,m]$:
    130140
    131 \begin{itemize}
     141\vspace*{-3mm}
     142\begin{itemize}
     143%\topsep 0pt
     144\itemsep -0.3em
    132145\item{$ \widehat{C}_j = AKS (\varphi_{C_j^1}) ~||~ AKS (\varphi_{C_j^2} ) ~||~...~||~ AKS (\varphi_{C_j^k}) ~||$\\ $ ...~||~ AKS (\varphi_{C_j^m}) $}
    133146\item{$ \widehat{M} = \widehat{C}_1 ~||~ \widehat{C}_2 ~||~ ... ~||~ \widehat{C}_j ~||~... ~||~ \widehat{C}_n $}
    … …  
    137150
    138151
    139 The generation of an abstract model in the form of AKS from CTL formulas is described in \cite{braunstein07ctl_abstraction} and has been implemented (\cite{bara08abs_composant}).
     152%The generation of an abstract model in the form of AKS from CTL formulas is described in \cite{braunstein07ctl_abstraction} and has been implemented (\cite{bara08abs_composant}).
    140153
    141154
    … …  
    154167\begin{definition}[]
    155168The \emph {concretization} of an abstract state $s$ with respect to the variable $p$
    156 ({\it unknown} in that state), assigns either true or false to $p$.
    157 
     169({\it unknown} in that state), assigns either true or false to $p$.\\
    158170The \emph {abstraction} of a state $s$ with respect to the variable $p$
    159171(either true or false in that state), assigns  {\it unknown} to $p$.
    … …  
    188200{\it and} to the  four-valued values of variables in $s_i$ and $s_{\varphi_j^k}$. For all $p \in
    189201AP_i \cup AP_{\varphi_j^k}$ we have the following label~:
    190 \begin{itemize}
    191 \topsep -.5em
    192 \itemsep -0.5em
     202\vspace*{-2mm}
     203\begin{itemize}
     204%\topsep 0pt
     205\itemsep -0.3em
    193206\item  $\widehat{L}_{i+1}[p] = \top$ iff  p is {\it unknown} in both states or
    194207does not belong to the set of atomic proposition.
    … …  
    197210(resp. $s_{\varphi_j^k}$).
    198211\end{itemize}
     212\vspace*{-2mm}
    199213By property \ref{prop:concrete}, $\widehat{M}_{i+1}$ is more concrete than
    200214$\widehat{M}_i$ and by
    … …  
    203217\end{proof}
    204218
     219\vspace*{-5mm}
    205220\subsection{Initial abstraction}
    206221Given a global property $\Phi$, the property to be verified by the composition of the concrete components model, an abstract model is generated by selecting some of the properties of the components which are relevant to $\Phi$.

  • papers/FDL2012/introduction.tex

    r91 r92  
    77and programmers as it may delay getting a new product to the market or cause
    88failure of some critical devices that are already in use. System verification
    9 using formal methods such as model checking guarantees a high level of quality in terms of safety and reliabilty while reducing financial risk.
     9using formal methods such as model checking guarantee a high level of quality in terms of safety and reliability while reducing financial risk.
    1010
    1111
    … …  
    1818
    1919
    20 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}. However, relying on counterexamples generated by the model checker as the only source for refinement may not be conclusive.
     20Several tools using counterexample-guided abstraction refinement technique, like those implemented in the VIS model-checker, 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.
    2121
    2222
    … …  
    2828
    2929
    30 In \cite{PMT02compositional_MC}, Peng, Mokhtari and Tahar have presented a possible implementation of assume-guarantee approach where the specification are in ACTL. Moreover, they managed to perform the synthetisation of the ACTL formulas into Verilog HDL behavior level program. The synthesized program can be used to check properties that the system's components must guarantee.
     30In \cite{PMT02compositional_MC}, Peng, Mokhtari and Tahar have presented a possible implementation of assume-guarantee approach where the specification are in ACTL. Moreover, they managed to perform the synthetisation of the ACTL formulas into Verilog HDL behavior level program. The synthesized program can be used to check properties that the system's components must guarantee. Since, there have been other works on construction of components from interval temporal logic properties which could be used to speed up verification process \cite{SNBE06property_based} \cite{Kunz_al11ipc_abs}.
    3131
    32 
    33 
    34 In 2006, Hans Eveking and al. introduced a technique of normalizing properties and transforming those normalized properties into an executable design description \cite{SNBE06property_based}. The generation of abstraction from PSL/Sugar specification language could then be used in the verification process to speed up the operation. This technique also allows the tests of specifications without having to build an implementation first.
    35 
     32%In 2006, Hans Eveking and al. introduced a technique of normalizing properties and transforming those normalized properties into an executable design description \cite{SNBE06property_based}. The generation of abstraction from PSL/Sugar specification language could then be used in the verification process to speed up the operation. This technique also allows the tests of specifications without having to build an implementation first.
     33%In \cite{Kunz_al11ipc_abs}, a method to formally verify low-level software in conjunction with the hardware by exploiting the Interval Property Checking (IPC) with abstraction technique was proposed. This method improves the robustness of interval property checking when proving long global interval properties of embedded systems.
    3634
    3735
    … …  
    3937
    4038
    41 In \cite{pwk2009-date}, an approach based on abstraction refinement technique has been proposed by Kroening and al. to strengthen properties in a finite state system specification . The method, which fundamentally relies on the notion of vacuity, generally produces shorter and stronger properties. In \cite{Kunz_al11ipc_abs}, a method to formally verify low-level software in conjunction with the hardware by exploiting the Interval Property Checking (IPC) with abstraction technique was proposed. This method improves the robustness of interval property checking when proving long global interval properties of embedded systems.
     39%In \cite{pwk2009-date}, an approach based on abstraction refinement technique has been proposed by Kroening and al. to strengthen properties in a finite state system specification . The method, which fundamentally relies on the notion of vacuity, generally produces shorter and stronger properties.
    4240
    4341

  • papers/FDL2012/myBib.bib

    r83 r92  
    7272   address = "Chicago, IL",
    7373   year = 2000,
    74    publisher = "Lecture Notes in Computer Science"
     74   publisher = "LNCS"
    7575}
    7676
    … …  
    159159   year = 2003,
    160160   month = Nov,
    161    publisher = "Lecture Notes in Computer Science"
     161   publisher = "LNCS"
    162162}
    163163
    … …  
    212212   pages = {103-122},
    213213   year = 2000,
    214    publisher = "Lecture Notes in Computer Science, Springer Verlag"
     214   publisher = "LNCS, Springer Verlag"
    215215}
    216216
    … …  
    223223   address = "Taipei, Taiwan",
    224224   year = 2005,
    225    publisher = "Lecture Notes in Computer Science, Springer"
     225   publisher = "LNCS, Springer"
    226226}
    227227
    … …  
    230230   author = "T. A. Henzinger and S. Qadeer and S. K. Rajamani",
    231231   title = "{ You Assume, We Guarantee : Methodology and Case Studies} ",
    232    booktitle = "CAV â€™98 : Proceedings of the 10th International Conference on Computer Aided Verification",
     232   booktitle = "CAV’98: Proceedings of the 10th Int. Conference on Computer Aided Verification",
    233233   volume = 1427,
    234234   pages = {440-451},
    235235   address = "Vancouver, Canada",
    236236   year = 1998,
    237    publisher = " Lecture Notes in Computer Science, Springer-Verlag"
     237   publisher = " LNCS, Springer-Verlag"
    238238}
    239239
    … …  
    246246   pages = {250-263},
    247247   year = 1991,
    248    publisher = " Lecture Notes in Computer Science, Springer-Verlag"
     248   publisher = " LNCS, Springer-Verlag"
    249249}
    250250
    … …  
    256256   volume = 1254,
    257257   year = 1997,
    258    publisher = " Lecture Notes in Computer Science, Springer"
     258   publisher = " LNCS, Springer"
    259259}
    260260
    … …  
    264264   author = "  S. Pardo and G. Hachtel",
    265265   title = "{ Automatic Abstraction Technique for Propositional mu-Calculus Model Checking} ",
    266    booktitle = " In CAV ’97: Proceedings of the 9th International Conference on Computer Aided Verification",
     266   booktitle = " In CAV ’97",
    267267   volume = 1254,
    268268   pages = {12-23},
    269269   year = 1997,
    270    publisher = " Lecture Notes in Computer Science, Springer-Verlag"
     270   publisher = " LNCS, Springer-Verlag"
    271271}
    272272
    … …  
    304304   author = " Himanshu Jain and Daniel Kroening and Natasha Sharygina and Edmund Clarke",
    305305   title = "{ VCEGAR: Verilog CounterExample Guided Abstraction Refinement} ",
    306    booktitle = " In 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)",
     306   booktitle = " In TACAS '07 ",
    307307   year = 2007,
    308308}
    … …  
    322322   author = " Thomas Ball and Byron Cook and Vladimir Levin and Sriram K. Rajamani",
    323323   title = "{ SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft} ",
    324    booktitle = " Fourth International Conference on Integrated Formal Methods (IFM 2004)",
     324   booktitle = "In 4th Int. Conference on Integrated Formal Methods (IFM 2004)",
    325325   volume = 2999,
    326326   pages = {1-20},
    327327   year = 2004,
    328    publisher = " Lecture Notes in Computer Science, Springer"
     328   publisher = " LNCS, Springer"
    329329}
    330330

  • papers/FDL2012/ordering_filter_properties.tex

    r90 r92  
    2727whereas variables which do not interfere with a primary variable are weighted 0.
    2828Here is how we proceed:
     29\vspace*{-5mm}
    2930\begin{enumerate}
     31\itemsep -0.3em
    3032\item Build the structural dependency graph for all primary variables.
    3133\item Compute the depth of all variables
    … …  
    157159In order to reach this objective, a Abstract Kripke structure of the counterexample $\sigma$, $K(\sigma)$
    158160is generated. $K(\sigma)$ is a succession of states corresponding to the counterexample path which dissatisfies
    159 the global property~$\Phi$
     161the global property~$\Phi$.
    160162%as show in figure \ref{AKSNegCex}.
    161163%In case where the spurious counter-example exhibits a bounded path, we add a last
    … …  
    181183R_{\sigma},F_{\sigma})$
    182184such that:
    183 
     185\vspace*{-2mm}
    184186\begin{itemize}
     187%\parsep=2pt
     188%\topsep 0pt
     189\itemsep -0.3em
    185190\item $AP_{\sigma} = \widehat{AP}_i$ : a finite set of atomic propositions which corresponds to the variables in the abstract model     
    186191\item $S_{\sigma} = \{s_{i}|s_i\in \sigma\}\cup\{s_T\}$
    … …  
    252257
    253258\begin{property}{Counterexample eviction}
     259\vspace*{-2mm}
    254260\begin{enumerate}
     261\itemsep -0.3em
    255262\item If {\textbf{$K(\sigma) \vDash \varphi  \Rightarrow AKS(\varphi) $ will
    256263not eliminate $\sigma$}}.
    … …  
    272279\end{proof}
    273280
     281\vspace*{-2mm}
    274282The proposed approach ensures that the refinement excludes the counterexample
    275283and  respects the definition \ref{def:goodrefinement}.
Note: See TracChangeset for help on using the changeset viewer.