Changeset 58 for papers/FDL2012/abstraction_refinement.tex

Timestamp:

Mar 9, 2012, 5:16:33 PM (13 years ago)

Author:

cecile

Message:

reordoring of the firsts definitions

File:

• papers/FDL2012/abstraction_refinement.tex (modified) (6 diffs)

papers/FDL2012/abstraction_refinement.tex

@@ -1 +1 @@
 
-We suppose that our concrete model is a composition of several components and each component has been previously verified. Hence, we have a set of verified properties for each component of the concrete model. The main idea of this technique is that we would like to make use of these properties to generate a better abstract model. Properties of the components that appear to be related to the global property to be verified, $\phi$ are selected to generate the abstract model $\widehat{M}_i$. This method is particularly interesting as it gives a possibility to converge quicker to an abstract model that is sufficient to satisfy the global property $\phi$.
 
 \subsection{Properties of good refinement}
@@ -8 +7 @@
 %\medskip
 
-\begin{property}
+\begin{definition} An efficient \emph{refinement} verified the following properties:
 \begin{enumerate}
 \item The new refinment is an over-approximation of the concrete model: $\widehat{M}_{i+1} \sqsubseteq \widehat{M}$.
@@ -16 +15 @@
 $\widehat{M_{i+1}}$.
 \end{enumerate}
-\end{property}
+\end{definition}
 
 Moreover, the refinement steps should be easy to compute and ensure a fast
@@ -26 +25 @@
 \TODO{discussion sur comment garantir les points 1/2/3 et le reste du bon
 rafinement}
-\subsection{The Counterexample}
-
-\TODO{Mettre la def avant}
+\subsection{Refinment by negation of the counterexample}
+
+\TODO{Mettre la def avant ?}
 \TODO{Rafinement par négation du contre-exemple}
 The counterexample at a refinement step $i$, $\sigma$ is a path in the
@@ -50 +49 @@
 \end{definition}
 
+2. Negation of states in an AKS
+
+a) An (abstract) configuration in a state of the AKS represents a (convex ?) set of states of the concrete component.
+
+b) The negation of an configuration may be represented by a set of abstract configurations
+
+c) building the AKS of a spurious counter-example may lead to a blow-up of the number of states of the AKS 
+
+
 %\bigskip
 
@@ -150 +158 @@
 
 
-\subsection{Initial abstraction generation}
-
-In the initial abstraction generation, all primary variables have to be represented. Therefore the first element(s) in the list where the primary variables are present will be used to generate the initial abstraction, $\widehat{M}_0$ and we will verify the satisfiability of the global 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.
-
-
-
-\subsection{Abstraction refinement}
+
+
+
+\subsection{Filtering properties}
 
 The refinement process from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ can be seperated into 2 steps: