Changeset 81 for papers/FDL2012/ordering_filter_properties.tex

Timestamp:

Apr 4, 2012, 3:21:25 PM (12 years ago)

Author:

cecile

Message:

typos et texte un peu allégé

File:

• papers/FDL2012/ordering_filter_properties.tex (modified) (8 diffs)

papers/FDL2012/ordering_filter_properties.tex

@@ -8 +8 @@
 %\bigskip
 
-The ordering of the properties is based on the variable dependency graph
-where the roots are primary variables.
-The variables in the model are weighted according to their dependency level
-\emph{vis-Ã -vis} primary variables and the properties is weighted according to the sum of the weights
-of the variables present in it. We want to select the properties specifying 
-behaviors that may have an impact on the global property. We observed that 
+%The ordering of the properties is based on the variable dependency graph
+%where the roots are primary variables.
+%The variables in the model are weighted according to their dependency level
+%\emph{vis-Ã -vis} primary variables and the properties is weighted according to the sum of the weights
+%of the variables present in it. We want to select the properties specifying 
+%behaviors that may have an impact on the global property.
+We observed that 
 the more closer a variable is from the primary
 variable the more it affects the primary variable. Hence, a property 
@@ -32 +33 @@
 we consider the minimum depth.
 \item Give a weight to each variable (see algorithm  \ref{algo:weight}).
-\item Compute the weight of properties for each component.
+\item Compute the weight of properties for each component~: sum of the
+property variables weight.
 \end{enumerate}
 
@@ -129 +131 @@
 
 
-Each properties  pertinence is evaluated by adding the weights of all the variables in it.
+%Each properties  pertinence is evaluated by adding the weights of all the variables in it.
 It is definitely not an exact pertinence calculation of properties but provides a good indicator 
 of their possible impact on the global property.
@@ -140 +142 @@
 \subsection{Filtering properties}
 The refinement step consists of adding new AKS of properties selected according to
-their pertinence. This refinement respects items 1 and 2 of definition
-\ref{def:goodrefinement}. The first item comes from AKS definition and the
-composition property \ref{prop:concrete_compose}.
-Adding a new AKS in the abstraction leads to an abstraction where more behaviors
-are characterized. Hence there is more constrains behavior and more concretize
-states.
-
-
+their pertinence.
+%This refinement respects items 1 and 2 of definition
+%\ref{def:goodrefinement}. The first item comes from AKS definition and the
+%composition property \ref{prop:concrete_compose}.
+%Adding a new AKS in the abstraction leads to an abstraction where more behaviors
+%are characterized. Hence there is more constrains behavior and more concretize
+%states.
 Unfortunately, this refinement does not ensure that the spurious counterexample
 is evicted.
@@ -155 +156 @@
 In order to reach this objective, a Abstract Kripke structure of the counterexample $\sigma$, $K(\sigma)$
 is generated. $K(\sigma)$ is a succession of states corresponding to the counterexample path which dissatisfies 
-the global property $\Phi$ as show in figure \ref{AKSNegCex}. In case where
-the counter-example exibits a bounded path, we add a last
+the global property $\Phi$ 
+%as show in figure \ref{AKSNegCex}. 
+In case where the spurious counter-example exhibits a bounded path, we add a last
 state $s_T$ where all variable are free({\it unknown}). The tree starting from this
 state represents all the possible future of the counterexample.
@@ -183 +185 @@
 \item $S_{\sigma} = \{s_{i}|s_i\in \sigma\}\cup\{s_T\}$
 \item $S_{0\sigma} = \{s_{0}\}$
-\item $L_{\sigma} = \check{L}_i$
+\item $L_{\sigma} = \widehat{L}_i$
 \item $R_{\sigma} =  \{(s_{k}, s_{k+1})|(s_{k}\rightarrow s_{k+1})\in
 \sigma\}\cup\{(s_{n-1},s_T)\}$ 
@@ -215 +217 @@
 %
 %
-\begin{figure}[h!]
-   \centering
-
-\begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=2cm,
-                    thick]
-  \tikzstyle{every state}=[fill=none,draw=blue,text=black, minimum size=1.1cm]
-
-  \node[initial,state] (A)                    {$s_{0}$};
-  \node[state]         (B) [below of=A]       {$s_{1}$};
-  \node[node distance=1.5cm]       (C) [below of=B]       {$\ldots$};
-  \node[state,node distance=1.5cm]       (D) [below of=C]     {$s_{n-1}$};
-  \node[state]         (E) [below of=D]     {$s_T$};
-
-  \path (A) edge node {} (B)
-        (B) edge node {} (C)
-        (C) edge node {} (D)
-        (D) edge node {} (E)
-        (E) edge[loop right] node {} (E);
-
-\end{tikzpicture}
-
-   \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma$, $K(\sigma)$}
-\end{figure}
+%\begin{figure}[h!]
+%   \centering
+%
+%\begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=2cm,
+%                    thick]
+%  \tikzstyle{every state}=[fill=none,draw=blue,text=black, minimum size=1.1cm]
+%
+%  \node[initial,state] (A)                    {$s_{0}$};
+%  \node[state]         (B) [below of=A]       {$s_{1}$};
+%  \node[node distance=1.5cm]      (C) [below of=B]       {$\ldots$};
+%  \node[state,node distance=1.5cm]       (D) [below of=C]     {$s_{n-1}$};
+%  \node[state]         (E) [below of=D]     {$s_T$};
+%
+%  \path (A) edge node {} (B)
+%        (B) edge node {} (C)
+%        (C) edge node {} (D)
+%        (D) edge node {} (E)
+%        (E) edge[loop right] node {} (E);
+%
+%\end{tikzpicture}
+%
+%   \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma$, $K(\sigma)$}
+%\end{figure}
 
 All the properties available for refinement are then model-checked on $K(\sigma)$. If the
 property holds then the property will not discriminate the counterexample.
 Hence this property is not a good candidate for refinement.
-Therefore all properties that are satisfied are chosen to be
+Therefore all properties that are not satisfied are chosen to be
 integrated in the next step of refinement. At this stage, we already have a
 list 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$.
@@ -262 +264 @@
 $AKS(\varphi)$, thus $\sigma$ is not a possible path in $AKS(\varphi)$
 otherwise $AKS(\varphi)\not\models \varphi$ that is not feasible due to AKS
-definition and the composition with $M_i$ with $AKS(\varphi)$ will eleiminate
+definition and the composition with $M_i$ with $AKS(\varphi)$ will eliminate
 $\sigma$.
 \end{enumerate}
 \end{proof}
 
-The property at the top of the list (not yet selected and excluding the properties
-which are satisfied by $K(\sigma)$) is selected to be integrated in the generation of $\widehat{M}_{i+1}$.
-We ensure that our refinement respects the definition \ref{def:goodrefinement}.
-Moreover, the time needed to build an AKS is neglectible and building the
-next abstraction is just a parallel composition with the previous one. Thus the refinement
- we propose is not time consuming.
+The propose approach ensure that the refinement excludes the counter-example
+and  respects the definition \ref{def:goodrefinement}.
+We will show in our experiments that first the time needed to build an AKS is
+negligible and secondly the refinement converges rapidly.
+%The property at the top of the list (not yet selected and excluding the properties
+%which are satisfied by $K(\sigma)$) is selected to be integrated in the generation of $\widehat{M}_{i+1}$.
+%We ensure that our refinement respects the definition \ref{def:goodrefinement}.
+%Moreover, the time needed to build an AKS is neglectible and building the
+%next abstraction is just a parallel composition with the previous one. Thus the refinement
+% we propose is not time consuming.