Changeset 93


Ignore:
Timestamp:
Apr 10, 2012, 4:30:02 PM (13 years ago)
Author:
syed
Message:

/papers/FDL2012/

Location:
papers/FDL2012
Files:
6 edited

Legend:

Unmodified
Added
Removed

  • papers/FDL2012/FDL2012.tex

    r92 r93  
    3333
    3434
    35  \title{ An efficient refinement strategy exploiting components' properties in a CEGAR process}
     35 \title{ An efficient refinement strategy exploiting component properties in a CEGAR process}
    3636% \name{Syed Hussein S. ALWI, C\'{e}cile BRAUNSTEIN and Emmanuelle ENCRENAZ}
    3737% \thanks{This work was supported by...}}
    … …  
    9696complete specification of every components of the concrete model. Futhermore,
    9797it may be possible that none of the properties available is capable of
    98 eliminating the counterexample which is probably due to an uncomplete
     98eliminating the counterexample which is probably due to an incomplete
    9999specification or a counterexample that should be eliminated by the product of
    100100local properties. In this case, other refinement techniques such as the
    … …  
    102102good set of local properties to be integreted simultaneously, should be considered.
    103103We are currently investigating other complementary techniques to overcome these particular cases.
    104 A complementary approach consists in oimproving the specification of the
     104A complementary approach consists in improving the specification of the
    105105model~: at the component level, or for groups of components. The work of
    106106Kroening \cite{pwk2009-date} could help us in this direction.

  • papers/FDL2012/abstraction_refinement.tex

    r92 r93  
    2424
    2525Refinements based on the concretization of selected abstract variables in
    26 $\widehat{M}_i$ ensure item 2. Concretization can be performed either in
    27 modifying the AKS of $\widehat{M}_i$, by changing some abstract value to
    28 concrete ones, but this approach is rude : in order to ensure item 1,
    29 concretization needs to be consistent with the sequences of values in the concrete system. The difficulty resides in defining the proper abstract variable to concretize, at which precise instant, and with which Boolean value.
     26$\widehat{M}_i$ ensure item 2. Concretization can be performed by
     27modifying the AKS of $\widehat{M}_i$ by changing some abstract value to
     28concrete ones. However, this approach is rude : in order to ensure item 1,
     29the concretization needs to be consistent with the sequences of values in the concrete system. The difficulty resides in defining the proper abstract variable to concretize, at which precise instant, and with which Boolean value.
    3030%Another way to concretize some variables at selected instants is to compose
    3131%(by a synchronous product) the AKS  of $\widehat{M}_i$ with a new AKS, provided this latest represents over-approximations of the set of behaviors of $M$. By construction, this product satisfies items 1 and 2. We now have to compute an AKS eliminating the spurious counterexample, being easily computable and ensuring a quick convergence of the CEGAR loop.
    … …  
    9696\end{itemize}
    9797\end{definition}
    98 The labeling function fo $s_i'$ represents (concrete) configuration of state $s_i$ and state $\bar{s_i}$  represents all
     98The labeling function of $s_i'$ represents (concrete) configuration of state $s_i$ and state $\bar{s_i}$  represents all
    9999configurations {\it but} the one of $s_i$. This last set may not be representable by
    100100the labeling function defined in def \ref{def-aks}. State labeling is treated
    … …  
    114114and assigns to each of them a label of $k$ variables $\{v_0, \ldots,
    115115v_{k-1}\}$ defined such that : $\widehat{L}(\bar{s_i^j}) = \{\forall l \in [0..k-1],
    116 v_l = \neg  {L}_{i}(s_i)[v_l], \forall l \in [j+1..k-1], v_l = \top\}$. each
     116v_l = \neg  {L}_{i}(s_i)[v_l], \forall l \in [j+1..k-1], v_l = \top\}$. Each
    117117state $\bar{s_i^j}$ is connected to the same predecessor and successor states
    118118as state $\bar{s_i}$.

  • papers/FDL2012/exp_results.tex

    r92 r93  
    121121
    122122
    123 In Table \ref{TabVerif}, we compare the execution time and the number of refinment
     123In Table \ref{TabVerif}, we compare the execution time and the number of refinement
    124124between our technique (Prop. Select.), \emph{incremental\_ctl\_verification}
    125125(Incremental) and the standard model checking (Standard MC) computed using the
    … …  
    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 26 verifed components properties to be selected in VCI-PI plateform.
     13026 verifed components properties to be selected in VCI-PI platform.
    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

    r92 r93  
    1515%generated and tested in the model-checker. As the abstract model is an
    1616%over-approximation of the concrete model and the global property $\Phi$ is in the ACTL fragment,
    17 As show in \cite{clarke94model} for over-approximation abstraction, if $\Phi$
    18 holds on the the abstract model then it holds in the concrete model as well.
     17As shown in \cite{clarke94model} for over-approximation abstraction, if $\Phi$
     18holds in the abstract model then it holds in the concrete model as well.
    1919However, if $\Phi$ does not hold in the abstract model then one cannot conclude anything regarding the concrete model until the counterexample has been analyzed.
    2020The test of spurious counter-example is then translated into a
    … …  
    6060%\topsep -0.5em
    6161\itemsep -0.3em
    62 \item $I$ is a finite set of Boolean inputs signals.
    63 \item $O$ is a finite set of Boolean outputs signals.
     62\item $I$ is a finite set of Boolean input signals.
     63\item $O$ is a finite set of Boolean output signals.
    6464\item $R$ is a finite set of Boolean sequential elements (registers).
    6565\item $\delta : 2^I \times 2^R \rightarrow 2^R$ is the transition function.
    … …  
    7676$M = C_1 \parallel C_2 \parallel \ldots \parallel C_n$,where each $C_i$ is a
    7777Moore machine with a specification associated $\varphi_i = \{\varphi_i^1 \ldots
    78 \varphi_i^k\}$ Each $\varphi_i^j$ is a CTL$\setminus$X formula whose
     78\varphi_i^k\}$. Each $\varphi_i^j$ is a CTL$\setminus$X formula whose
    7979propositions $AP$ belong to $\{I_i\cup O_i\cup R_i\}$ .
    8080\end{definition}
    … …  
    126126
    127127\vspace*{-2mm}
    128 We 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$.
     128We 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$.
    129129
    130130
    … …  
    155155%\subsection{Characterization of AKS}
    156156
    157 In an AKS a state where a variable $p$ is {\it unknown}
     157In an AKS, a state where a variable $p$ is {\it unknown}
    158158can simulate all states in which $p$ is either true or false. It
    159159is a concise representation of the set of more concrete states in which $p$
    160160is either true or false.  A state $s$ is said to be an \emph{abstract state}
    161 if one its variable $p$ is {\it unknown}.
     161if one of its variable $p$ is {\it unknown}.
    162162
    163163%\begin{definition}

  • papers/FDL2012/introduction.tex

    r92 r93  
    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 guarantee a high level of quality in terms of safety and reliability while reducing financial risk.
     9using formal methods such as model checking guarantees a high level of quality in terms of safety and reliability while reducing financial risk.
    1010
    1111
    … …  
    2525
    2626
    27  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. A comprehensive approach to model-check component-based systems with abstraction refinement technique that uses verified properties as abstractions has been presented in \cite{LiSunXieSong08compAbsRef}.
     27 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 has been succesful and the application of the assume-guarantee reasoning has considerably reduced the model checking complexity. A comprehensive approach to model-check component-based systems with abstraction refinement technique that uses verified properties as abstractions has been presented in \cite{LiSunXieSong08compAbsRef}.
    2828
    2929
    … …  
    3434
    3535
    36 Recently, a CEGAR based technique that combines precise and approximated methods within one abstraction-refinement loop was proposed for software verification \cite{Sharygina_al12PreciseApprox}. This technique uses predicate abstraction and provides a strategy that interleaves approximated abtraction which is fast to compute and precise abstraction which is slow. The result shows a good compromise between the number of refinement iterations and verification time.
     36Recently, a CEGAR based technique that combines precise and approximated methods within one abstraction-refinement loop was proposed for software verification \cite{Sharygina_al12PreciseApprox}. This technique uses predicate abstraction and provides a strategy that interleaves approximated abstraction which is fast to compute and precise abstraction which is slow. The result shows a good compromise between the number of refinement iterations and verification time.
    3737
    3838
    … …  
    4242In 2007, a method to build abstractions of components into AKS (Abstract
    4343Kripke Structure), based on the set of the properties (CTL) each component
    44 verifies \cite{braunstein07ctl_abstraction}. The method is actually a
     44verifies was presented in \cite{braunstein07ctl_abstraction}. The method is actually a
    4545tentative to associate compositional and abstraction-refinement verification
    4646techniques. The generations of AKS from CTL formula have been successfully

  • papers/FDL2012/ordering_filter_properties.tex

    r92 r93  
    1515%behaviors that may have an impact on the global property.
    1616We observed that
    17 the closer a variable is from the primary
     17the closer a variable is to the primary
    1818variable, the higher influence it has on it.
    1919%Hence, a property
Note: See TracChangeset for help on using the changeset viewer.