Changeset 56 for papers/FDL2012/abstraction_refinement.tex

Timestamp:

Mar 8, 2012, 2:00:31 PM (13 years ago)

Author:

cecile

Message:

add defintions concrete, and modify refinement, cex defintion

File:

• papers/FDL2012/abstraction_refinement.tex (modified) (1 diff)

papers/FDL2012/abstraction_refinement.tex

@@ -1 @@
-\subsection{Generalities}
 
 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$.
 
-\subsubsection{Refinement}
-The model-checker provides a counterexample when a property failed during model-checking. The counterexample can be \emph{spurious} which means that the path is impossible in the concrete model $M$ or the counterexample is real which implies that $M \nvDash \phi $.When a counterexample is found to be spurious, it means that the current abstract model $\widehat{M}_i$ is too coarse and has to be refined. In this section, we will discuss about the refinement technique based on the integration of more verified properties of the concrete model's components in the abstract model to be generated. Moreover, the refinement step from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ has to be conservative and respects the properties below:
+\subsection{Properties of good refinement}
+When a counterexample is found to be spurious, it means that the current abstract model $\widehat{M}_i$ is too coarse and has to be refined.
+In this section, we will discuss about the refinement technique based on the integration of more verified properties of the concrete model's components in the abstract model to be generated. Moreover, the refinement step from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ respects the properties below:
 
 %\medskip
 
 \begin{property}
-All $\widehat{M}_i$ generated are upper-approximations of $M$. Furthermore, we guarantee that $\widehat{M}_{i+1} \sqsubseteq \widehat{M}_i$.
+\begin{enumerate}
+\item The new refinment is an over-approximation of the concrete model: $\widehat{M}_{i+1} \sqsubseteq \widehat{M}$.
+\item The new refinment is more concrete than the previous one:
+$\widehat{M}_{i} \sqsubseteq \widehat{M}_{i+1}$.
+\item The spurious counter-example in $\widehat{M}_i$ is  removed from
+$\widehat{M_{i+1}}$.
+\end{enumerate}
 \end{property}
-%\bigskip
-\begin{property}
-$\sigma_i$ is a counterexample of $\widehat{M}_i$ and $\sigma_i$ is not a counterexample of $\widehat{M}_{i+1}$.
-\end{property}
-
-%\bigskip
-%\newpage
-
-\subsubsection{The Counterexample}
-
-
-The counterexample at a refinement step $i$, $\sigma_i$ is a path in the abstract model $\widehat{M}_i$ which dissatisfy $\phi$.  In the counterexample given by the model-checker, the variables' value in each states are boolean.
-%\medskip
-
+
+Moreover, the refinement steps should be easy to compute and ensure a fast
+convergence by the minimizing the number of iteration of the CEGAR loop.
+
+
+A possible refinement : concretization of selected abstract variables. How to choose variables and instants of concretization : introduce new CTL properties. The question is : how to select pertinent CTL properties ???
+
+\TODO{discussion sur comment garantir les points 1/2/3 et le reste du bon
+rafinement}
+\subsection{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
+abstract model $\widehat{M}_i$ which dissatisfy $\Phi$.  In the counterexample given by the model-checker, the variables' value in each states are boolean.
+The spurious counter-example $\sigma$ is defined such that :
 \begin{definition}
-\textbf{\emph{The counterexample $\sigma_i$ :}} \\
+\textbf{\emph{The counterexample $\sigma$ :}} \\
 \\
-Let $\widehat{M}_i =(\widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i}, \widehat{L}_i, \widehat{R}_i, \widehat{F}_i)$ and let the length of the counterexample, $|\sigma_i| = n$: $ \sigma_i = \langle s_{\bar{a}i,0}, s_{\bar{a}i,1}, s_{\bar{a}i,2}, ... , s_{\bar{a}i,k},$ $s_{\bar{a}i,k+1}, ... , s_{\bar{a}i,n}\rangle $ with $ \forall k \in [0,n-1], ~s_{\bar{a}i,k} \subseteq s_{i,k}  \in \widehat{S}_i, ~s_{\bar{a}i,0} \subseteq s_{i,0} \in \widehat{S}_{0i}$ and $(s_{i,k}, s_{i,k+1}) \in \widehat{R}_i$. \\
-Furthermore, for each state in $\sigma_i$ we have $s_{\bar{a}i,k} = \langle v_{\bar{a}i,k}^1, v_{\bar{a}i,k}^2, ... ,  v_{\bar{a}i,k}^p, ... , v_{\bar{a}i,k}^q \rangle$, $\forall p \in [1,q], ~v_{\bar{a}i,k}^p \in \widehat{V}_{i,k}$ with $\widehat{V}_{i,k} \in 2^q$. \\
-\\
-(\emph{\underline{Note} :} In AKS $\widehat{M}_i$, the variables are actually 3-valued : $\widehat{V}_{i,k} \in 3^q$. We differenciate the 3-valued variables  $v_{i,k}^p$ from boolean variables with $v_{\bar{a}i,k}^p$.)\\
-
-%\medskip
-
+Let $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
+\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ and let the length of the
+counterexample, $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
+s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$. 
+\begin{itemize}
+\item All its variables are concrete: $\forall s_i$ and $\forall p\in
+\widehat{AP}_i$, $p$ is either true or false
+(not {\it unknown}).
+\item  $\sigma$ is a counter-example in  $\widehat{M}_i$: $s_0\not\models \Phi$.
+\item  $\sigma$ is not a path of the concrete system $M$: $\exists k$ such
+that $(s_{k}, s_{k+1}) \not\in R$.
 \end{definition}
 
 %\bigskip
 
-\begin{definition}
-\textbf{\emph{Spurious counterexample :}} \\
-\\
-Let $\sigma_c = \langle s_{c,0}, s_{c,1}, s_{c,2}, ... , s_{c,k}, s_{c,k+1}, ... , s_{c,n}\rangle$ a path of length $n$ in the concrete model $M$ and in each state of $\sigma_c$ we have $s_{c,k} = \langle v_{c,k}^1, v_{c,k}^2, ... ,  v_{c,k}^{p'}, ... , v_{c,k}^{q'} \rangle$ with $\forall p' \in [1,q'], ~v_{i,k}^{p'} \in V_{c,k}$ and $V_{c,k} \in 2^{q'}$.\\
-
-\smallskip
-
-If $\forall k$ we have $\widehat{V}_{i,k} \subseteq V_{c,k}$ and $\forall v_{\bar{a}i,k} \in \widehat{V}_{i,k}, ~s_{i,k}|_{v_{\bar{a}i,k}} = s_{c,k}|_{v_{c,k}} $ then $M \nvDash \phi$ else $\sigma_i$ is \emph{spurious}.
-
-\end{definition}
-
-
-
-\subsection{Pre-processing and pertinency ordering of properties}
+%\begin{definition}
+%\textbf{\emph{Spurious counterexample :}} \\
+%\\
+%Let $\sigma_c = \langle s_{c,0}, s_{c,1}, s_{c,2}, ... , s_{c,k}, s_{c,k+1}, ... , s_{c,n}\rangle$ a path of length $n$ in the concrete model $M$ and in each state of $\sigma_c$ we have $s_{c,k} = \langle v_{c,k}^1, v_{c,k}^2, ... ,  v_{c,k}^{p'}, ... , v_{c,k}^{q'} \rangle$ with $\forall p' \in [1,q'], ~v_{i,k}^{p'} \in V_{c,k}$ and $V_{c,k} \in 2^{q'}$.\\
+%
+%\smallskip
+%
+%If $\forall k$ we have $\widehat{V}_{i,k} \subseteq V_{c,k}$ and $\forall v_{\bar{a}i,k} \in \widehat{V}_{i,k}, ~s_{i,k}|_{v_{\bar{a}i,k}} = s_{c,k}|_{v_{c,k}} $ then $M \nvDash \phi$ else $\sigma_i$ is \emph{spurious}.
+%
+%\end{definition}
+
+
+
+\subsection{Ordering of properties}
 
 Before generating an abstract model to verify a global property $\phi$, the verified properties of all the components in the concrete model are ordered according to their pertinency in comparison to a global property $\phi$. In order to do so, the variable dependency of the variables present in global property $\phi$ has to be analysed. After this point, we refer to the variables present in the global property $\phi$ as \emph{primary variables}.