Changeset 67 for papers/FDL2012

Timestamp:

Mar 14, 2012, 4:27:45 PM (13 years ago)

Author:

cecile

Message:

Refinement text filter added

Location:

papers/FDL2012

Files:

• abstraction_refinement.tex (modified) (1 diff)
• ordering_filter_properties.tex (modified) (4 diffs)

papers/FDL2012/abstraction_refinement.tex

@@ -15 +15 @@
 $\widehat{M_{i+1}}$.
 \end{enumerate}
+\label{def:goodrefinement}
 \end{definition}
 

papers/FDL2012/ordering_filter_properties.tex

@@ -100 +100 @@
 %\bigskip
 
-\emph{\underline{Example:}}  \\
-
-For example, if a global property $\phi$ consists of 3 variables: $ p, q, r $ where:
-\begin{itemize}
-\item{$p$ is dependent of $a$ and $b$}
-\item{$b$ is dependent of $c$}
-\item{$q$ is dependent of $x$}
-\item{$r$ is independent}
-\end{itemize}
-
-Example with unit weight= 50.
-The primary variables: $p$, $q$ and $r$ are weighted $100x10=1000$ each. \\
-The secondary level variables : $a$, $b$ and $x$ are weighted $50x2=100$ each. \\
-The tertiary level variable $c$ is weighted $50$. \\
-The weight of a non-related variable is $0$.
-
-So each verified properties available pertinency will be evaluated by adding the weights of all the variables in it. It is definitely not an exact pertinency calculation of properties but provides a good indicator of their possible impact on the global property.
-
-\bigskip
-\begin{figure}[h!]
-   \centering
-%   \includegraphics[width=1.2\textwidth]{Dependency_graph_weight_PNG}
-%     \hspace*{-15mm}
-     \includegraphics{Dependency_graph_weight_PNG}
-   \caption{\label{DepGraphWeight} Example of weighting}
-\end{figure}
+%\emph{\underline{Example:}}  \\
+%
+%For example, if a global property $\phi$ consists of 3 variables: $ p, q, r $ where:
+%\begin{itemize}
+%\item{$p$ is dependent of $a$ and $b$}
+%\item{$b$ is dependent of $c$}
+%\item{$q$ is dependent of $x$}
+%\item{$r$ is independent}
+%\end{itemize}
+%
+%Example with unit weight= 50.
+%The primary variables: $p$, $q$ and $r$ are weighted $100*10=1000$ each. \\
+%The secondary level variables : $a$, $b$ and $x$ are weighted $50x2=100$ each. \\
+%The tertiary level variable $c$ is weighted $50$. \\
+%The weight of a non-related variable is $0$.
+%
+%
+%\bigskip
+%\begin{figure}[h!]
+%   \centering
+%%   \includegraphics[width=1.2\textwidth]{Dependency_graph_weight_PNG}
+%%     \hspace*{-15mm}
+%     \includegraphics{Dependency_graph_weight_PNG}
+%   \caption{\label{DepGraphWeight} Example of weighting}
+%\end{figure}
 
 %Dans la figure~\ref{étiquette} page~\pageref{étiquette},  
@@ -131 +130 @@
 
 
-After this pre-processing phase, we will have a list of properties $L_\phi  $ ordered according to their pertinency in comparison to the global property.
-
-
-
+Each verified properties available pertinency will be evaluated by adding the weights of all the variables in it.
+It is definitely not an exact pertinency calculation of properties but provides a good indicator 
+of their possible impact on the global property.
+After this pre-processing phase, we will have a list of properties $L_\phi$
+ordered according to their pertinency in comparison to the global property.
 
 
@@ -140 +140 @@
 
 \subsection{Filtering properties}
-\TODO{Explaining w.r. to good refinement}
+The refinement step consists of adding new AKS of properties selected according to
+their pertinency. This refinement respects the points 1 and 2 of definition
+\ref{def:goodrefinement}. The first item comes form AKS definition. 
+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. 
+
+\Remark{Cécile}{Mettre definition, property and proof ?????}
+
+Unforutnatly, this refinement does not ensure that the spurious counter-example
+is evicted. 
+As we would like to ensure the elimination of the counterexample previously found,
+we filter out properties that don't have an impact on the counterexample $\sigma_i$ thus won't eliminate it. 
+In order to reach this obective, a AKS of the counterexample $\sigma_i$, $K(\sigma_i)$
+is generated. $K(\sigma_i)$ is a succession of states corresponding to the counterexample path which dissatisfies 
+the global property $\Phi$. It is an abstract kripke structure since not all
+variables are concrete.
+Each properties
+All the properties available are then model-checked on $K(\sigma_i)$. If the
+property holds then the property will not discriminate the counter-example.
+Hence this property is not a good candidate for refinement.
+Therefore all properties that are satisfied won't be chosen to be integrated in the next step of refinement. At this stage, we already have a list of potential properties that will definitely eliminate the current counterexample $\sigma_i$ and might converge the abstract model towards a model sufficient to verify the global property $\phi$.
+
+
+\TODO{Revoir la definition et Proof}
+
 The refinement process from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ can be seperated into 2 steps:
 
@@ -216 +241 @@
 
 
-Therefore all properties that are satisfied won't be chosen to be integrated in the next step of refinement. At this stage, we already have a list of potential properties that will definitely eliminate the current counterexample $\sigma_i$ and might converge the abstract model towards a model sufficient to verify the global property $\phi$.
-
 }
 %\bigskip