Changeset 76 for papers


Ignore:
Timestamp:
Mar 28, 2012, 3:21:52 PM (13 years ago)
Author:
ema
Message:
 
Location:
papers/FDL2012
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • papers/FDL2012/abstraction_refinement.tex

    r70 r76  
    1919
    2020Moreover, the refinement steps should be easy to compute and ensure a fast
    21 convergence by the minimizing the number of iteration of the CEGAR loop.
     21convergence by minimizing the number of iterations of the CEGAR loop.
    2222
    2323Refinements based on the concretization of selected abstract variables in $\widehat{M}_i$ ensure item 2. Concretization can be performed either in modifying the AKS of $\widehat{M}_i$, by changing some abstract value to concrete ones, but this approach is rude : in order to ensure item 1, concretization needs to be coherent 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.
     
    2929\subsection{Refinement by negation of the counterexample}
    3030
    31 The counterexample at a refinement step $i$, $\sigma$ is a path in the
    32 abstract model $\widehat{M}_i$ which dissatisfy $\Phi$.  In the counterexample given by the model-checker, the variables value in each states are boolean.
     31The counterexample at a refinement step $i$, $\sigma$, is a path in the
     32abstract model $\widehat{M}_i$ which dissatisfies $\Phi$.  In the counterexample given by the model-checker, the variable configuration in each state is boolean.
    3333The spurious counterexample $\sigma$ is defined such that :
    3434\begin{definition}
     
    6666\emph{Example}. Assume $AP = \{v_0,v_1,v_2\}$ and $\sigma = s_0 \rightarrow s_1, \ldots$ and $\widehat{L}(s_0) = \{\mathbf{f},\mathbf{f},\mathbf{f}\}$ meaning the configuration associated with $s_0$ assigns false to each variable. The negation of this configuration represents a set of seven concrete configurations which are covered by three (abstract) configurations: $\{\{\mathbf{t},\top,\top\},\{\mathbf{f},\mathbf{t},\top\},\{\mathbf{f},\mathbf{f},\mathbf{t}\}\}$.
    6767
    68 To build the final AKS representing all sequences but spurious counter-example $\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $s"_i$ by $n = \mid AP_{\overline\sigma} \mid$ states $s"_i^k$ with $k \in [0..n-1]$ and assigns to each of them a label of $n$ variables $\{v_0, \ldots, v_{n-1}\}$ defined such that : ${L}(s"_i^k) = \{\forall l \in [0..k], v_l = \neg  {L}_{i}(s'_i)[v_l], \forall l \in [k+1..n-1], v_l = \top\}$.
    69 \TODO{connexion des $s"_i^k$}
     68To build the final AKS representing all sequences but spurious counter-example $\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $s"_i$ by $n = \mid AP_{\overline\sigma} \mid$ states $s"_i^k$ with $k \in [0..n-1]$ and assigns to each of them a label of $n$ variables $\{v_0, \ldots, v_{n-1}\}$ defined such that : ${L}(s"_i^k) = \{\forall l \in [0..k], v_l = \neg  {L}_{i}(s'_i)[v_l], \forall l \in [k+1..n-1], v_l = \top\}$. each state $s"_i^k$ is connected to predecessor and successor states as state $s"_i$ was.
    7069
    71 \TODO{Revoir notation def 3 pour f,t,top et introduire notation ${L}_{i}(s'_i)[v_l]$}
    72 
    73 This final AKS presents a number of states which is linear with product of the length of the counter-example and the number of atomic propositions. However, removing, at each refinement step, the spurious counter-example {\em only} induces a low convergence. Moreover, in some cases, this strategy may not converge: suppose that all sequences of the form $a.b^*.c$ are spurious counter-examples. At a given refinement step $i$, a particular counter example $\sigma_i = s_0 \rightarrow s_1 \rightarrow \ldots s_n$ with $L(s_0) = a, \forall k \in [1, n-1], L(s_k) = b, L(s_n) = c$. Removing this counter-example does not prevent from a new spurious counter-example at step $i+1$ :  $\sigma_{i+1} = s_0 \rightarrow s_1 \rightarrow \ldots s_{n+1}$ with $L(s_0) = a, \forall k \in [1, n], L(s_k) = b, L(s_{n+1}) = c$. The strategy consisting of elimination spurious counter-example {\em one by one} diverges in this case. However, we cannot eliminate all the sequences of the form $a.b^*.c$ in a unique refinement step since we do not a priori know if at least one of these sequence is executable in the concrete model.
     70This final AKS presents a number of states in $\cal{O}(\mid\sigma\mid\times\mid AP\mid)$. However, removing, at each refinement step, the spurious counter-example {\em only} induces a low convergence. Moreover, in some cases, this strategy may not converge: suppose that all sequences of the form $a.b^*.c$ are spurious counter-examples (here $a$, $b$ and $c$ represent concrete state configurations). At a given refinement step $i$, a particular counter example $\sigma_i = s_0 \rightarrow s_1 \rightarrow \ldots s_n$ with $L(s_0) = a, \forall k \in [1, n-1], L(s_k) = b, L(s_n) = c$. Removing this counter-example does not prevent from a new spurious counter-example at step $i+1$ :  $\sigma_{i+1} = s_0 \rightarrow s_1 \rightarrow \ldots s_{n+1}$ with $L(s_0) = a, \forall k \in [1, n], L(s_k) = b, L(s_{n+1}) = c$. The strategy consisting of elimination spurious counter-example {\em one by one} diverges in this case. However, we cannot eliminate all the sequences of the form $a.b^*.c$ in a unique refinement step since we do not a priori know if at least one of these sequence is executable in the concrete model.
    7471
    7572From these considerations, we are interested in removing {\em sets of behaviors encompassing the spurious counter-example} but still guaranteeing an over-approximation of the set of tree-organized behaviors of the concrete model. The strengthening of the abstraction $\widehat{M}_i$ with the adjunction of AKS of already verified local CTL properties eliminates sets of behaviors and guarantees the over-approximation but does not guarantee the elimination of the counter example. We present in the following section a strategy to select sets of CTL properties eliminating the spurious counter example.
  • papers/FDL2012/framework.tex

    r68 r76  
    11The model-checking technique we propose is based on the Counterexample-guided
    22Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. The overall
    3 descritpion of our methodology is shown in figure \ref{cegar}.
     3description of our methodology is shown in figure \ref{cegar}.
    44We take into account the structure of the system as a set of synchronous components,
    5 each of which has been previously verified and a set of CTL properties is attached to each component. This set refers to the specification of the component. We would like to verify whether a concrete model, $M$ presumedly huge sized composed of several components, satisfies a global property $\Phi$. Due to state space combinatorial explosion phenomenon that occurs when verifying huge and complex systems, an abstraction or approximation of the concrete model has to be done in order to be able to verify the system with model-checking techniques. Instead of building the product of the concrete components, we replace each concrete component by an abstraction of its behavior derived from a subset of the CTL properties it satisfies. Each abstract component represents an over-approximation of the set of behaviors of its related concrete component \cite{braunstein07ctl_abstraction}.
     5each of which has been previously verified and a set of CTL properties is attached to each component. This set refers to the specification of the component. We would like to verify whether a concrete model, $M$ presumedly huge sized and composed of several components, satisfies a global ACTL property $\Phi$. Due to state space combinatorial explosion phenomenon that occurs when verifying huge and complex systems, an abstraction or approximation of the concrete model has to be done in order to be able to verify the system with model-checking techniques. Instead of building the product of the concrete components, we replace each concrete component by an abstraction of its behavior derived from a subset of the CTL properties it satisfies. Each abstract component represents an over-approximation of the set of behaviors of its related concrete component \cite{braunstein07ctl_abstraction}.
    66
    77%\subsection{Overall Description of our methodology}
     
    99concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is
    1010generated and tested in the model-checker. As the abstract model is an
    11 over-approximation of the concrete model and we have restrained our
    12 verification to ACTL properties only. As shown in \cite{clarke94model} if $\Phi$ holds on the the abstract model then we are certain that it holds in the concrete model as well.
    13 However, if $\Phi$ doesn't hold in the abstract model then we can't conclude anything regarding the concrete model until the counterexample,
    14 $\sigma$ given by the model-checker has been analyzed.
     11over-approximation of the concrete model and the global property $\Phi$ is in the ACTL fragment, if $\Phi$ holds on the the abstract model then it holds in the concrete model as well \cite{clarke94model}. However, if $\Phi$ does not hold in the abstract model then one cannot conclude anything regarding the concrete model until the counterexample, $\sigma$, given by the model-checker has been analyzed.
     12In this last case, the test of spurious counter-example is translated into a SAT problem \TODO{citer ref SAT spurious}. When a counterexample is proven to be spurious, the refinement phase occurs, injecting more preciseness into the (abstract) model to be analyzed.
    1513
    16 In the case where model-checking failed, the counterexample given by the
    17 model-checker  has to be analysed. We use a SAT solver to check whether the counterexample is spurious or not. When a counterexample is proved to be spurious, we proceed to the refinement phase.
    18 \TODO{ref du papier sur le spurious + petite explication sur SAT et
    19 déroulement}
    2014%\bigskip
    2115%\begin{definition}
     
    4539
    4640\subsection{Concrete system definition}
    47 As mention earlier, in our verification methodology, we have a concrete model which consists of several components and each component comes with its specification or more precisely, properties that hold in the component. Given 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 $\varphi$.
     41As mention earlier, in our verification methodology, we have a concrete model which consists of several components and each component comes with its specification or more precisely, properties that hold in the component. Given 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$.
    4842
    4943
    50 The concrete system is a synchronous compositon of components, each of which
     44The concrete system is a synchronous composition of components, each of which
    5145described as a Moore machine.
    5246\begin{definition}
     
    7064Moore machine with a specification associated $\varphi_i = \{\varphi_i^1 \ldots
    7165\varphi_i^k\}$ Each $\varphi_i^j$ is a CTL$\setminus$X formula whose
    72 propositions $AP$ belongs to $\{I_i\cup O_i\cup R_i\}$ .
     66propositions $AP$ belong to $\{I_i\cup O_i\cup R_i\}$ .
    7367\end{definition}
    7468
     
    7670
    7771Our abstraction consists in reducing the size of the representation model by
    78 freeing some of its variables. The point is to determine the good set of variable
     72letting free some of its variables. The point is to determine the good set of variable
    7973to be freed and when to free them. We take advantage of the CTL specification
    8074of each component: a CTL property may be seen as a partial view of the tree of
    8175behaviors of its variables. All the variables not specified by the property
    8276can be freed. We introduced the Abstract Kripke Structure (AKS for short) which exactly
    83 specifies when the variable of the prperty can be freed.
     77specifies when the variable of the property can be freed.
    8478The abstraction of a component is represented by an AKS,
    8579derived from a subset of the CTL properties the component satisfies.
     
    8781$\varphi$, simulates all execution trees whose initial state satisfies
    8882$\varphi$. In AKS($\varphi$), states are tagged with the truth values of
    89 $\varphi$'s atomic propositions, among four truth values : inconsistent,
    90 false, true and unknown (either true or false).
     83$\varphi$'s atomic propositions, among the four truth values of Belnap's logic \cite{belnap77}: inconsistent ($\bot$),
     84false ($\mathbf{f}$), true ($\mathbf{t}$) and unknown ($\top$)).
    9185States with inconsistent truth values are not represented since they refer to non possible
    9286assignments of the atomic propositions. A set of fairness constraints eliminates non-progress cycles.
     
    10397\item { $\widehat{S}$ : a finite set of states}
    10498\item { $\widehat{S}_0 \subseteq \widehat{S}$ : a set of initial states}
    105 \item { $\widehat{L} : \widehat{S} \rightarrow 2^{Lit}$ : a labeling function which labels each state with the set of atomic propositions true in that state. Lit is a set of literals such that $Lit = AP \cup \{\bar{p} | p \in AP \}$. With this labeling definition, an atomic proposition in a state can have 4 different values as detailed below:}
    106                 \begin{itemize}
    107                         \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{unknown} in} s }
    108                         \item {$ p \notin \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) : p $\emph{ is \textbf{false} in} s}
    109                         \item {$ p \in \widehat{L}(s) \wedge \bar{p} \notin \widehat{L}(s) : p $\emph{ is \textbf{true} in} s}
    110                   \item {$ p \in \widehat{L}(s) \wedge \bar{p} \in \widehat{L}(s) :  p $\emph{ is \textbf{inconsistent} in} s}
    111                 \end{itemize}
     99\item { $\widehat{L} : \widehat{S} \rightarrow \cal{B}^{\mid AP \mid}$ with $\cal{B} = \{\bot, \mathbf{f}, \mathbf{t},\top\}$: a labeling function which labels each state with configuration of current value of each atomic proposition.}
    112100\item { $\widehat{R} \subseteq \widehat{S} \times \widehat{S}$ : a transition relation where $ \forall s \in \widehat{S}, \exists s' \in \widehat{S}$ such that $(s,s') \in \widehat{R}$ }
    113101\item { $\widehat{F}$ : a set of fairness constraints (generalized B\"uchi
     
    117105%\bigskip
    118106
     107We 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$.
    119108
    120109As the abstract model $\widehat{M}$ is generated from the conjunction of verified properties of the components in the concrete model $M$, it can be seen as the composition of the AKS of each property.
    121110The AKS composition has been defined in \cite{braunstein_phd07}; it extends
    122 the classical synchrounous composition of Moore machine to deal with
     111the classical synchronous composition of Moore machine to deal with
    123112four-valued variables.
    124113%\bigskip
    125114
    126115\begin{definition} An \emph{Abstract model} $\widehat{M}$is obtained by
    127 synchronous composition of components abstractions.
    128 Let $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]$:
     116synchronous composition of components abstractions. Let $n$ be the number of components in the model and $m$ be the number of selected verified properties of a component;
     117let $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]$:
    129118
    130119\begin{itemize}
     
    133122\end{itemize}
    134123
    135 \hspace*{3mm}with :\\
    136 \hspace*{5mm}- $ n \in \mathbb{N} $ : the number of components in the model \\
    137 \hspace*{5mm}- $ m \in \mathbb{N} $ : the number of selected verified properties of a component
    138 
    139124\end{definition}
    140 %\bigskip
    141125
    142126
    143 The generation of an abstract model in the form of AKS from CTL formulas,
    144 based on the works of Braunstein \cite{braunstein07ctl_abstraction},
    145 has been successfully implemented by Bara \cite{bara08abs_composant}.
     127The 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}).
    146128
    147129
    148130%\subsection{Characterization of AKS}
    149131
    150 In an abstract kripke structure a state where a variable $p$ is {\it unknown}
     132In an abstract Kripke structure a state where a variable $p$ is {\it unknown}
    151133can simulate all states in which $p$ is either true or false. It
    152 is concise representation of the set of more concrete states in which $p$
     134is a concise representation of the set of more concrete states in which $p$
    153135is either true or false.  A state $s$ is said to be an \emph{abstract state}
    154136if one its variable $p$ is {\it unknown}.
     
    167149
    168150\begin{property}
    169 Let A1 and A2 two abstractions such that A2 is obtained by concretizing one abstract variable of A1 (resp A1 is obtained by abstracting one variable in A2). Then A1 simulates A2.
     151Let $A_i$ and $A_j$ two abstractions such that $A_j$ is obtained by concretizing one abstract variable of $A_i$ (resp $A_i$ is obtained by abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$, denoted by $A_j \sqsubseteq A_i$.
    170152\end{property}
    171153\begin{proof}
    172154As the concretization of state reduces the set of concrete configuration the
    173155abstract state represents but does not affect the transition relation of the
    174 AKS. The unroll execution tree of A2 is a subtree of the one of A1. Then  A1 simulates A2.
     156AKS. The unroll execution tree of $A_j$ is a subtree of the one of $A_i$. Then  $A_i$ simulates $A_j$.
    175157\end{proof}
    176158
  • papers/FDL2012/myBib.bib

    r69 r76  
    123123    title = "{Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking}",
    124124    journal = {32nd ACM/IEEE Design Automation Conference},
    125     year = 1995   
     125    year = 1995
    126126}
    127127
     
    132132    pages = {80-89},
    133133    year = 2007
     134}
     135
     136@article{ belnap77,
     137    author = "N. Belnap",
     138    title = "{A useful four-valued logic}",
     139    journal = {Modern Uses of Multiple-Valued Logic},
     140    pages = {8-37},
     141    year = 1977
    134142}
    135143
     
    342350 title     = "Using {BibTeX}. {D}ocumentation for general {B}ib{\TeX} users",
    343351 year      =  1988,
    344  month     =  jan 
     352 month     =  jan
    345353}
    346354
     
    355363    year = 2009
    356364}
    357 
Note: See TracChangeset for help on using the changeset viewer.