Changeset 81 for papers/FDL2012


Ignore:
Timestamp:
Apr 4, 2012, 3:21:25 PM (13 years ago)
Author:
cecile
Message:

typos et texte un peu allégé

Location:
papers/FDL2012
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • papers/FDL2012/abstraction_refinement.tex

    r79 r81  
    99\begin{definition} An efficient \emph{refinement} verifies the following properties:
    1010\begin{enumerate}
    11 \item The new refinement is an over-approximation of the concrete model: $\widehat{M}_{i+1} \sqsubseteq \widehat{M}$.
     11\item The new refinement is an over-approximation of the concrete model:
     12$\widehat{M} \sqsubseteq \widehat{M}_{i+1}$.
    1213\item The new refinement is more concrete than the previous one:
    13 $\widehat{M}_{i} \sqsubseteq \widehat{M}_{i+1}$.
     14$\widehat{M}_{i+1} \sqsubseteq \widehat{M}_{i}$.
    1415\item The spurious counterexample in $\widehat{M}_i$ is  removed from
    1516$\widehat{M_{i+1}}$.
    … …  
    1718\label{def:goodrefinement}
    1819\end{definition}
    19 
    2020Moreover, the refinement steps should be easy to compute and ensure a fast
    2121convergence by minimizing the number of iterations of the CEGAR loop.
    2222
    23 Refinements 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.
    24 Another way to concretize some variables at selected instants is to compose (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.
     23Refinements based on the concretization of selected abstract variables in
     24$\widehat{M}_i$ ensure item 2. Concretization can be performed either in
     25modifying the AKS of $\widehat{M}_i$, by changing some abstract value to
     26concrete ones, but this approach is rude : in order to ensure item 1,
     27concretization 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.
     28%Another way to concretize some variables at selected instants is to compose
     29%(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.
    2530
    26 Several proposals can be made. The most straightforward consists in building the AKS representing all possible executions except the  spurious counterexample ; however the AKS representation may be huge and the process is not guaranteed to converge. A second possibility is to build an AKS with additional CTL properties of the components ; the AKS remains small but item 3 is not guaranteed, hence delaying the convergence. The final proposal combines both previous ones : first local CTL properties eliminating the spurious counter example are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$.
     31We propose to compose the abstraction with another AKS to build a good refinement
     32according to definition \ref{def:goodrefinement}.
     33We have  several options. The most straightforward consists in building
     34an AKS representing all possible executions except the  spurious counterexample ; however the AKS representation may be huge and the process is not guaranteed to converge. A second possibility is to build an AKS with additional CTL properties of the components ; the AKS remains small but item 3 is not guaranteed, hence delaying the convergence. The final proposal combines both previous ones : first local CTL properties eliminating the spurious counter example are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$.
    2735
    2836
    29 \subsection{Refinement by negation of the counterexample}
     37\subsection{Negation of the counterexample}
    3038
    3139The counterexample at a refinement step $i$, $\sigma$, is a path in the
    3240abstract model $\widehat{M}_i$ which dissatisfies $\Phi$.  In the
    3341counterexample given by the model-checker, the variable configuration in each
    34 state is boolean. We name $\check{L_i}$ this new labeling.
     42state is Boolean. We name $\widehat{L_i}$ this new labeling.
    3543The spurious counterexample $\sigma$ is defined such that :
    3644\begin{definition}
    37 Let $\sigma$ be a \emph{counter-example} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
     45Let $\sigma$ be a \emph{spurious counter-example} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
    3846\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of  length $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
    3947\rightarrow s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$.
    … …  
    4755\end{itemize}
    4856\end{definition}
    49 In the following we denote by
    50 The construction of the AKS representing all executions except the one described by the spurious counter-example is done in two steps.
    51 \subsubsection{step 1 : Build the structure of the AKS.}
     57The construction of the AKS representing all executions except the one
     58described by the spurious counter-example is done in two steps.
     59
     60\subsubsection{Step 1~:~Build the structure of the AKS.}
     61
    5262
    5363\begin{definition}
    54 Let $\sigma$ be a counter-example of  length $|\sigma| = n$, the \emph{ AKS of the
     64Let $\sigma$ be a spurious counter-example of  length $|\sigma| = n$, the \emph{ AKS of the
    5565counter-example negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}},
    5666\widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}},
    … …  
    5969\item $AP_{\overline{\sigma}} = {AP}_i$:
    6070The set of atomic propositions coincides with the one of $\sigma$
    61 \item $\widehat{S}_{\overline{\sigma}}$: $\{s_T\} \cup \{s_{i}'|\forall i`in
     71
     72\item $\widehat{S}_{\overline{\sigma}}$: $\{s_T\} \cup \{s_{i}'|\forall i\in
    6273[0..n-2] \vee s_i\in
    63 \sigma\}\cup \{\bar{s_{i}}|\forall i in [0..n-1] \vee s_i\in \sigma\}$
    64 \item $\widehat{L}_{\overline{\sigma}}$ is such that $s_i'$ represents the
    65 (concrete) configuration of state $s_i$ and state $\bar{s_i}$  represents all
    66 configurations but the one of $s_i$. This last set may not be representable by
    67 the labeling function defined in def \ref{def-aks}. State labeling is treated
    68 in the second step. $s_t$ is a state where all atomic propositions are {\it unknown}.
     74\sigma\}\cup \{\bar{s_{i}}|\forall i \in [0..n-1] \vee s_i\in \sigma\}$
     75
     76\item $\widehat{L}_{\overline{\sigma}}$  with
     77$L_{\overline{\sigma}}(s_i') = L_i(s_i), \forall i \in [0..n-2]$ and
     78$L_{\overline{\sigma}}(\bar{s_i}) = \bar{L_i(s_i)}, \forall i \in [0..n-1]$
    6979
    7080\item $\widehat{S}_{0{\overline{\sigma}}} = \{ s_0',\bar{s_0}\}$
     81
    7182\item $\widehat{R}_{\overline{\sigma}} = \{(\bar{s_i},s_T), \forall i\in
    7283[0..n-1]\} \cup \{(s_i',\bar{s_{i+1}}), \forall i\in[0..n-2]\} \cup
    … …  
    7687\end{itemize}
    7788\end{definition}
    78 The size of this structure is linear with the size of the counter-example, however it is not a strict AKS since the representation of the set of configurations in states $s"$ may lead to a union of labels.
     89Note that in the labeling function represent (concrete) configuration of state $s_i$ and state $\bar{s_i}$  represents all
     90configurations but the one of $s_i$. This last set may not be representable by
     91the labeling function defined in def \ref{def-aks}. State labeling is treated
     92in the second step. $s_T$ is a state where all atomic propositions are {\it unknown}.
     93%The size of this structure is linear with the size of the counter-example.
    7994
    80 \subsubsection{Step 2 : Expand state configurations representing the negation of a concrete configuration.}
    81 We return back to the labeling of states of $AKS(\overline{\sigma})$. As states $s'$ are associated with the same (concrete) configuration as their corresponding state in $\sigma$, their labeling is straightforward : $\forall i \in [0..n-1], {L}_{\overline{\sigma}}(s'_i) = \widehat{L}_{i}(s_i)$.
    82 The set of configurations associated with a state $s"_i$ represents the negation of the one represented by ${L}_{\overline{\sigma}}(s'_i)$. This negation is not representable by the label of a single state but rather by a union of $\mid AP \mid$ labels.
     95\subsubsection{Step 2~:~Expand state configurations representing the negation of a concrete configuration.}
     96%We return back to the labeling of states of $AKS(\overline{\sigma})$. As states $s'$ are associated with the same (concrete) configuration as their corresponding state in $\sigma$, their labeling is straightforward : $\forall i \in [0..n-1], {L}_{\overline{\sigma}}(s'_i) = \widehat{L}_{i}(s_i)$.
     97The set of configurations associated with a state $\bar{s_i}$ represents the
     98negation of the one represented by ${L}_i(s'_i)$. This negation is not representable by the label of a single state but rather by a union of $\mid AP \mid$ labels.
    8399
    84 \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}\}\}$.
     100\emph{Example}. Assume $AP = \{v_0,v_1,v_2\}$ and $\sigma = s_0 \rightarrow s_1$ and $\widehat{L}(s_0) = \{\mathbf{f},\mathbf{f},\mathbf{f}\}$ 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}\}\}$.
    85101
    86 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\}$. each state $s"_i^k$ is connected to predecessor and successor states as state $s"_i$ was.
     102To build the final AKS representing all sequences but spurious counter-example
     103$\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $\bar{s_i}$ by
     104$k = \mid AP_{\overline\sigma} \mid$ states $\bar{s_i^j}$ with $j\in [0..k-1]$
     105and assigns to each of them a label of $n$ variables $\{v_0, \ldots,
     106v_{n-1}\}$ defined such that : ${L}(\bar{s_i^j} = \{\forall l \in [0..k-1],
     107v_l = \neg  {L}_{i}(s_i)[v_l], \forall l \in [j+1..k-1], v_l = \top\}$. each
     108state $\bar{s_i^j}$ is connected to the same predecessor and successor states
     109as state $\bar{s_i}$.
    87110
    88 This 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.
     111This 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 priors know if at least one of these sequence is executable in the concrete model.
    89112
    90 From 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.
     113From these considerations, we are interested in removing {\em sets of
     114behaviors encompassing the spurious counter-example} but still guaranteeing an
     115over-approximation of the set of tree-organized behaviors of the concrete
     116model. The strengthening of the abstraction $\widehat{M}_i$ with the
     117addition of AKS of already verified local CTL properties eliminates sets of
     118behaviors and guarantees the over-approximation (property
     119\ref{prop:concrete_compose}) 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.
    91120
    92121

  • papers/FDL2012/framework.tex

    r79 r81  
    33description 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 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}.
     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$ presumably huge sized and composed of several components, satisfies a global ACTL property $\Phi$.
     6%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.
     7Instead 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}.
    68
    79%\subsection{Overall Description of our methodology}
    8 In CEGAR loop methodology, in order to verify a global property $\Phi$ on a
    9 concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is
    10 generated and tested in the model-checker. As the abstract model is an
    11 over-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.
    12 In this last case, the test of spurious counter-example is translated into a
     10%In CEGAR loop methodology, in order to verify a global property $\Phi$ on a
     11%concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is
     12%generated and tested in the model-checker. As the abstract model is an
     13%over-approximation of the concrete model and the global property $\Phi$ is in the ACTL fragment,
     14As show in \cite{clarke94model} for over-approximation abstraction, if $\Phi$
     15holds on the the abstract model then it holds in the concrete model as well.
     16However, if $\Phi$ does not hold in the abstract model then one cannot conclude anything regarding the concrete model until the counterexample has been analyzed.
     17The test of spurious counter-example is then translated into a
    1318SAT problem as in \cite{clarke00cegar}. When a counterexample is proven to be spurious, the refinement phase occurs, injecting more preciseness into the (abstract) model to be analyzed.
    1419
    … …  
    4045
    4146\subsection{Concrete system definition}
    42 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 $\Phi$.
    43 
    44 
     47As mention earlier, our concrete model consists of several components and each
     48component comes with its specification.
    4549The concrete system is a synchronous composition of components, each of which
    4650described as a Moore machine.
    … …  
    4852A \emph{Moore machine} $C$ is defined by a tuple $\langle I, O, R,$ $\delta, \lambda, \mathbf{R}_0 \rangle$, where,
    4953\begin{itemize}
    50 \item $I$ is a finite set of boolean inputs signals.
    51 \item $O$ is a finite set of boolean outputs signals.
    52 \item $R$ is a finite set of boolean sequential elements (registers).
     54\item $I$ is a finite set of Boolean inputs signals.
     55\item $O$ is a finite set of Boolean outputs signals.
     56\item $R$ is a finite set of Boolean sequential elements (registers).
    5357\item $\delta : 2^I \times 2^R \rightarrow 2^R$ is the transition function.
    5458\item $\lambda : 2^R \rightarrow 2^O$ is the output function.
    … …  
    5761\end{definition}
    5862
    59 \emph{States} (or configurations) of the circuit correspond to boolean configurations of all the sequential elements.
     63\emph{States} (or configurations) of the circuit correspond to Boolean configurations of all the sequential elements.
    6064
    6165\begin{definition}
    … …  
    7074\subsection{Abstraction definition}
    7175
    72 Our abstraction consists in reducing the size of the representation model by
     76Our abstraction reduces the size of the representation model by
    7377letting free some of its variables. The point is to determine the good set of variable
    7478to be freed and when to free them. We take advantage of the CTL specification
    … …  
    132136%\subsection{Characterization of AKS}
    133137
    134 In an abstract Kripke structure a state where a variable $p$ is {\it unknown}
     138In an AKS a state where a variable $p$ is {\it unknown}
    135139can simulate all states in which $p$ is either true or false. It
    136140is a concise representation of the set of more concrete states in which $p$
    … …  
    151155
    152156\begin{property}[Concretization]
     157\label{prop:concrete}
    153158Let $A_i$ and $A_j$ two abstractions such that $A_j$ is obtained by
    154 concretizing one abstract variable of $A_i$ (resp $A_i$ is obtained by
    155 abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$, denoted by
    156 $A_i \sqsubseteq A_j$.
     159concretizing one abstract variable of $A_i$ (resp. $A_i$ is obtained by
     160abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$ and $A_j$
     161concretizes $A_i$ , denoted by
     162$A_j \sqsubseteq A_i$.
    157163\end{property}
    158164\begin{proof}
    159165As the concretization of state reduces the set of concrete configuration the
    160166abstract state represents but does not affect the transition relation of the
    161 AKS. The unroll execution tree of $A_j$ is a subtree of the one of $A_i$. Then  $A_i$ simulates $A_j$.
     167AKS. The unroll execution tree of $A_j$ is a sub-tree of the one of $A_i$. Then
     168$A_i$ simulates $A_j$.
    162169\end{proof}
    163170
    164 \begin{property}[Compostion and Concretization]
     171\begin{property}[Composition and Concretization]
    165172\label{prop:concrete_compose}
    166173Let $\widehat{M_i}$ be an abstract model of $M$ and $\varphi_j^k$ be a property
    167174of a component $C_j$ of M,  $\widehat{M}_{i+1} = \widehat{M_i}\parallel
    168 AKS(\varphi_j^k) $ is simulated by $ \widehat{M_i}$, $\widehat{M_i}
    169 \sqsubseteq \widehat{M}_{i+1}$.
     175AKS(\varphi_j^k) $ is more concrete that $ \widehat{M_i}$, $\widehat{M_{i+1}}
     176\sqsubseteq \widehat{M}_i$.
    170177\end{property}
    171178
    172179\begin{proof}
    173 By the property of the parallel composition, we have directly  $\widehat{M_i}
    174 \sqsubseteq \widehat{M}_{i} \parallel AKS(\varphi_j^k$.
     180Let $s = (s_i,s_{\varphi_j^k})$ be a state in $S_{i+1}$, such that $s_i\in S_i$
     181and $s_{\varphi_j^k} \in S_{\varphi_j^k}$.
     182The label of $s_{i+1}$ respects the Belnap logic operator. For all $p \in
     183AP_i \cup AP_{\varphi_j^k}$ we have the following label~:
     184\begin{itemize}
     185\topsep -.5em
     186\itemsep -0.5em
     187\item  $\widehat{L}_{i+1}[p] = \top$ iff  p is {\it unknown} in both states or
     188does not belong to the set of atomic proposition.
     189\item  $\widehat{L}_{i+1}[p] = \mathbf{t}$ (or $\mathbf{f}$) iff $p$ is true
     190(or false) in $s_{\varphi_j^k}$ (resp. $s_i$)  and {\it unknown} in $s_i$
     191(resp. $s_{\varphi_j^k}$).
     192\end{itemize}
     193By property \ref{prop:concrete}, $M_{i+1}$ is more concrete than $M_i$ and by
     194the property of parallel composition,
     195$\widehat{M_i} \sqsubseteq \widehat{M}_{i} \parallel AKS(\varphi_j^k$).
    175196\end{proof}
    176197
    177198\subsection{Initial abstraction}
    178 We suppose that our concrete model is a composition of several components and
    179 each component has been previously verified. Hence, we have a set of verified
    180 properties for each component of the concrete model. The main idea of this
    181 technique is that we would like to make use of these properties to generate a
    182 better abstract model. Properties of the components that appear to be related
    183 to the global property to be verified, $\Phi$ are selected to generate the
    184 abstract model $\widehat{M}_i$. This method is particularly interesting as it
    185 gives a possibility to converge quicker to an abstract model that is
    186 sufficient to satisfy the global property $\Phi$.
    187 In the following, we will name primary variables the set of variable that
    188 appears in the global property.
    189 
    190 In the initial abstraction generation, all primary variables have to be
     199Given 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$.
     200%We suppose that our concrete model is a composition of several components and
     201%each component has been previously verified. Hence, we have a set of verified
     202%properties for each component of the concrete model. The main idea of this
     203%technique is that we would like to make use of these properties to generate a
     204%better abstract model. Properties of the components that appear to be related
     205%to the global property to be verified, $\Phi$ are selected to generate the
     206%abstract model $\widehat{M}_i$. This method is particularly interesting as it
     207%gives a possibility to converge quicker to an abstract model that is
     208%sufficient to satisfy the global property $\Phi$.
     209%In the following, we will name primary variables the set of variable that
     210%appears in the global property.
     211In the initial abstraction generation, all variables that appear int $\Phi$ have to be
    191212represented. Therefore the properties in the specification of each component
    192 where the primary variables are present will be used to generate the initial
     213where these variables are present will be used to generate the initial
    193214abstraction, $\widehat{M}_0$ and we will verify the satisfiability of the
    194215global property $\Phi$ on this abstract model. If the model-checking failed and the counterexample given is found to be spurious, we will then proceed with the refinement process.

  • papers/FDL2012/ordering_filter_properties.tex

    r79 r81  
    88%\bigskip
    99
    10 The ordering of the properties is based on the variable dependency graph
    11 where the roots are primary variables.
    12 The variables in the model are weighted according to their dependency level
    13 \emph{vis-à-vis} primary variables and the properties is weighted according to the sum of the weights
    14 of the variables present in it. We want to select the properties specifying
    15 behaviors that may have an impact on the global property. We observed that
     10%The ordering of the properties is based on the variable dependency graph
     11%where the roots are primary variables.
     12%The variables in the model are weighted according to their dependency level
     13%\emph{vis-à-vis} primary variables and the properties is weighted according to the sum of the weights
     14%of the variables present in it. We want to select the properties specifying
     15%behaviors that may have an impact on the global property.
     16We observed that
    1617the more closer a variable is from the primary
    1718variable the more it affects the primary variable. Hence, a property
    … …  
    3233we consider the minimum depth.
    3334\item Give a weight to each variable (see algorithm  \ref{algo:weight}).
    34 \item Compute the weight of properties for each component.
     35\item Compute the weight of properties for each component~: sum of the
     36property variables weight.
    3537\end{enumerate}
    3638
    … …  
    129131
    130132
    131 Each properties  pertinence is evaluated by adding the weights of all the variables in it.
     133%Each properties  pertinence is evaluated by adding the weights of all the variables in it.
    132134It is definitely not an exact pertinence calculation of properties but provides a good indicator
    133135of their possible impact on the global property.
    … …  
    140142\subsection{Filtering properties}
    141143The refinement step consists of adding new AKS of properties selected according to
    142 their pertinence. This refinement respects items 1 and 2 of definition
    143 \ref{def:goodrefinement}. The first item comes from AKS definition and the
    144 composition property \ref{prop:concrete_compose}.
    145 Adding a new AKS in the abstraction leads to an abstraction where more behaviors
    146 are characterized. Hence there is more constrains behavior and more concretize
    147 states.
    148 
    149 
     144their pertinence.
     145%This refinement respects items 1 and 2 of definition
     146%\ref{def:goodrefinement}. The first item comes from AKS definition and the
     147%composition property \ref{prop:concrete_compose}.
     148%Adding a new AKS in the abstraction leads to an abstraction where more behaviors
     149%are characterized. Hence there is more constrains behavior and more concretize
     150%states.
    150151Unfortunately, this refinement does not ensure that the spurious counterexample
    151152is evicted.
    … …  
    155156In order to reach this objective, a Abstract Kripke structure of the counterexample $\sigma$, $K(\sigma)$
    156157is generated. $K(\sigma)$ is a succession of states corresponding to the counterexample path which dissatisfies
    157 the global property $\Phi$ as show in figure \ref{AKSNegCex}. In case where
    158 the counter-example exibits a bounded path, we add a last
     158the global property $\Phi$
     159%as show in figure \ref{AKSNegCex}.
     160In case where the spurious counter-example exhibits a bounded path, we add a last
    159161state $s_T$ where all variable are free({\it unknown}). The tree starting from this
    160162state represents all the possible future of the counterexample.
    … …  
    183185\item $S_{\sigma} = \{s_{i}|s_i\in \sigma\}\cup\{s_T\}$
    184186\item $S_{0\sigma} = \{s_{0}\}$
    185 \item $L_{\sigma} = \check{L}_i$
     187\item $L_{\sigma} = \widehat{L}_i$
    186188\item $R_{\sigma} =  \{(s_{k}, s_{k+1})|(s_{k}\rightarrow s_{k+1})\in
    187189\sigma\}\cup\{(s_{n-1},s_T)\}$
    … …  
    215217%
    216218%
    217 \begin{figure}[h!]
    218    \centering
    219 
    220 \begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=2cm,
    221                     thick]
    222   \tikzstyle{every state}=[fill=none,draw=blue,text=black, minimum size=1.1cm]
    223 
    224   \node[initial,state] (A)                    {$s_{0}$};
    225   \node[state]         (B) [below of=A]       {$s_{1}$};
    226   \node[node distance=1.5cm]       (C) [below of=B]       {$\ldots$};
    227   \node[state,node distance=1.5cm]       (D) [below of=C]     {$s_{n-1}$};
    228   \node[state]         (E) [below of=D]     {$s_T$};
    229 
    230   \path (A) edge node {} (B)
    231         (B) edge node {} (C)
    232         (C) edge node {} (D)
    233         (D) edge node {} (E)
    234         (E) edge[loop right] node {} (E);
    235 
    236 \end{tikzpicture}
    237 
    238    \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma$, $K(\sigma)$}
    239 \end{figure}
     219%\begin{figure}[h!]
     220%   \centering
     221%
     222%\begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=2cm,
     223%                    thick]
     224%  \tikzstyle{every state}=[fill=none,draw=blue,text=black, minimum size=1.1cm]
     225%
     226%  \node[initial,state] (A)                    {$s_{0}$};
     227%  \node[state]         (B) [below of=A]       {$s_{1}$};
     228%  \node[node distance=1.5cm]      (C) [below of=B]       {$\ldots$};
     229%  \node[state,node distance=1.5cm]       (D) [below of=C]     {$s_{n-1}$};
     230%  \node[state]         (E) [below of=D]     {$s_T$};
     231%
     232%  \path (A) edge node {} (B)
     233%        (B) edge node {} (C)
     234%        (C) edge node {} (D)
     235%        (D) edge node {} (E)
     236%        (E) edge[loop right] node {} (E);
     237%
     238%\end{tikzpicture}
     239%
     240%   \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma$, $K(\sigma)$}
     241%\end{figure}
    240242
    241243All the properties available for refinement are then model-checked on $K(\sigma)$. If the
    242244property holds then the property will not discriminate the counterexample.
    243245Hence this property is not a good candidate for refinement.
    244 Therefore all properties that are satisfied are chosen to be
     246Therefore all properties that are not satisfied are chosen to be
    245247integrated in the next step of refinement. At this stage, we already have a
    246248list of potential properties that definitely eliminates the current counterexample $\sigma$ and might converge the abstract model towards a model sufficient to verify the global property $\Phi$.
    … …  
    262264$AKS(\varphi)$, thus $\sigma$ is not a possible path in $AKS(\varphi)$
    263265otherwise $AKS(\varphi)\not\models \varphi$ that is not feasible due to AKS
    264 definition and the composition with $M_i$ with $AKS(\varphi)$ will eleiminate
     266definition and the composition with $M_i$ with $AKS(\varphi)$ will eliminate
    265267$\sigma$.
    266268\end{enumerate}
    267269\end{proof}
    268270
    269 The property at the top of the list (not yet selected and excluding the properties
    270 which are satisfied by $K(\sigma)$) is selected to be integrated in the generation of $\widehat{M}_{i+1}$.
    271 We ensure that our refinement respects the definition \ref{def:goodrefinement}.
    272 Moreover, the time needed to build an AKS is neglectible and building the
    273 next abstraction is just a parallel composition with the previous one. Thus the refinement
    274  we propose is not time consuming.
     271The propose approach ensure that the refinement excludes the counter-example
     272and  respects the definition \ref{def:goodrefinement}.
     273We will show in our experiments that first the time needed to build an AKS is
     274negligible and secondly the refinement converges rapidly.
     275%The property at the top of the list (not yet selected and excluding the properties
     276%which are satisfied by $K(\sigma)$) is selected to be integrated in the generation of $\widehat{M}_{i+1}$.
     277%We ensure that our refinement respects the definition \ref{def:goodrefinement}.
     278%Moreover, the time needed to build an AKS is neglectible and building the
     279%next abstraction is just a parallel composition with the previous one. Thus the refinement
     280% we propose is not time consuming.
    275281
    276282
Note: See TracChangeset for help on using the changeset viewer.