Index: papers/FDL2012/framework.tex
===================================================================
--- papers/FDL2012/framework.tex	(revision 57)
+++ papers/FDL2012/framework.tex	(revision 58)
@@ -1,13 +1,21 @@
-The model-checking technique we propose is based on the Counterexample-guided Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. We take into account the structure of the system as a set of synchronous components, 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 composed of several components, satisfies a global 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}.
+The model-checking technique we propose is based on the Counterexample-guided
+Abstraction Refinement (CEGAR) methodology \cite{clarke00cegar}. The overall
+descritpion of our methodology is shown in figure \ref{cegar}.
+We take into account the structure of the system as a set of synchronous components, 
+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 composed of several components, satisfies a global 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}.
 
-\subsection{Overall Description of our methodology}
+%\subsection{Overall Description of our methodology}
 In CEGAR loop methodology, in order to verify a global property $\Phi$ on a
 concrete model $M$, an abstraction of the concrete model $\widehat{M}$ is
 generated and tested in the model-checker. As the abstract model is an
 over-approximation of the concrete model and we have restrained our
-verification to ACTL properties only, if $\Phi$ holds on the the abstract model then we are certain that it holds in the concrete model as well. 
+verification to ACTL properties only. As shown in \cite{clarke94model} if $\Phi$ holds on the the abstract model then we are certain that it holds in the concrete model as well. 
 However, if $\Phi$ doesn't hold in the abstract model then we can't conclude anything regarding the concrete model until the counterexample, 
-$\sigma$ given by the model-checker has been analyzed. \remark{Cecile}{cite
-Grumberg ovver-approx et ACTL poperties}
+$\sigma$ given by the model-checker has been analyzed. 
+
+In the case where model-checking failed, the counterexample given by the
+model-checker  has to be analysed. We use a SAT solver to check whether the counterexample is spurious or not. When a counterexample is proved to be spurious, we proceed to the refinement phase.
+\TODO{ref du papier sur le spurious + petite explication sur SAT et
+dÃ©roulement}
 %\bigskip
 %\begin{definition}
@@ -16,15 +24,15 @@
 %\end{definition}
 
-\begin{definition}
-Given $\widehat{M} = (\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ an abstract model of a concrete model, $M$ and $\Phi$, a global property to be verified on $M$, the model-checking result can be interpreted as follows:
-
-\begin{itemize}
-\item{$\widehat{M} \vDash \Phi \Rightarrow M \vDash \Phi$ : verification completed }
-\item{$\widehat{M} \nvDash \Phi$  and  $\exists \sigma$ : counterexample analysis required in order to determine whether $M \nvDash \Phi$ or $\widehat{M}$ is too coarse. }
-\end{itemize}
-\end{definition}
+%\begin{definition}
+%Given $\widehat{M} = (\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ an abstract model of a concrete model, $M$ and $\Phi$, a global property to be verified on $M$, the model-checking result can be interpreted as follows:
+%
+%\begin{itemize}
+%\item{$\widehat{M} \vDash \Phi \Rightarrow M \vDash \Phi$ : verification completed }
+%\item{$\widehat{M} \nvDash \Phi$  and  $\exists \sigma$ : counterexample analysis required in order to determine whether $M \nvDash \Phi$ or $\widehat{M}$ is too coarse. }
+%\end{itemize}
+%\end{definition}
 
 %\bigskip
-We can conclude that the property $\Phi$ doesn't hold in the concrete model $M$ if the counterexample path is possible in M. Otherwise the abstract model at step $i : \widehat{M}_i$, has to be refined if $\widehat{M}_i \nvDash \Phi$ and the counterexample obtained during model-checking was proven to be \emph{spurious}.
+%We can conclude that the property $\Phi$ doesn't hold in the concrete model $M$ if the counterexample path is possible in M. Otherwise the abstract model at step $i : \widehat{M}_i$, has to be refined if $\widehat{M}_i \nvDash \Phi$ and the counterexample obtained during model-checking was proven to be \emph{spurious}.
 
 \begin{figure}[h!]
@@ -36,10 +44,7 @@
 \end{figure}
 
+\subsection{Concrete system definition}
 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 $\varphi$. 
 
-In the case where model-checking failed, the counterexample given by the model-checker \cite{ucberkeley96vis}  has to be analysed. We use a SATSolver to check whether the counterexample is spurious or not. When a counterexample is proved to be spurious, we proceed to the refinement phase.
-\TODO{ref du papier sur le spurious + petite explication sur SAT et
-dÃ©roulement}
-\subsection{Concrete system definition}
 
 The concrete system is a synchronous compositon of components, each of which
@@ -57,5 +62,5 @@
 \end{definition}
 
-\emph{States} (or configurations) of the circuit correspond to boolean configurations of all the sequential elements. From now on, let $C = \langle I, O, R, \delta, \lambda, \mathbf{R}_0 \rangle$ be a sequential circuit.
+\emph{States} (or configurations) of the circuit correspond to boolean configurations of all the sequential elements.
 
 \begin{definition}
@@ -64,5 +69,5 @@
 $M = C_1 \parallel C_2 \parallel \ldots \parallel C_n$,where each $C_i$ is a
 Moore machine with a specification associated $\varphi_i = \{\varphi_i^1 \ldots
-\varphi_i^k\}$ Each $\varphi_i^j$ being a CTL$\setminus$X formula whose
+\varphi_i^k\}$ Each $\varphi_i^j$ is a CTL$\setminus$X formula whose
 propositions $AP$ belongs to $\{I_i\cup O_i\cup R_i\}$ .
 \end{definition}
@@ -71,10 +76,10 @@
 
 Our abstraction consists in reducing the size of the representation model by
-freeing some its variables. The point is to determine the good set of variable
+freeing some of its variables. The point is to determine the good set of variable
 to be freed and when to free them. We take advantage of the CTL specification
 of each component: a CTL property may be seen as a partial view of the tree of
 behaviors of its variables. All the variables not specified by the property
 can be freed. We introduced the Abstract Kripke Structure (AKS for short) which exactly
-specifies when the variable of the prperty can be frreed.
+specifies when the variable of the prperty can be freed.
 The abstraction of a component is represented by an AKS, 
 derived from a subset of the CTL properties the component satisfies.
@@ -89,11 +94,11 @@
  
 %Assume that we have an abstract Kripke structure (AKS) representing the abstract model $\widehat{M}$ of the concrete model of the system M with regard to the property to be verified, $\Phi$. The abstraction method is based on the work described in \cite{ braunstein07ctl_abstraction}. 
-The AKS associated with a CTL property $\varphi$ whose set of atomic propositions is $AP$ is a 6-tuple, \\ $\widehat{C} =(\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ which is defined as follows:
 
 \begin{definition}
-An abstract Kripke structure,\\ $\widehat{C} =(\widehat{AP}, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ is a 6-tuple consisting of :
+Give a CTL$\setminus$X property $\varphi$ whose set of atomic propositions is
+$\widehat{AP}$, An \emph{Abstract Kripke Structure}, \\ $AKS(\varphi) =(AP, \widehat{S}, \widehat{S}_0, \widehat{L}, \widehat{R}, \widehat{F})$ is a 6-tuple consisting of :
 
 \begin{itemize}
-\item { $\widehat{AP}$ : a finite set of atomic propositions}	
+\item { $AP$ : The finite set of atomic propositions of property $\varphi$ }	
 \item { $\widehat{S}$ : a finite set of states}
 \item { $\widehat{S}_0 \subseteq \widehat{S}$ : a set of initial states}
@@ -119,5 +124,6 @@
 %\bigskip
 
-\begin{definition}
+\begin{definition} An \emph{Abstract model} $\widehat{M}$is obtained by
+synchronous composition of components abstractions.
 Let $C_j$ be a component of the concrete model $M$ and $\varphi_{j}^k$ is a CTL formula describing a satisfied property of component $C_j$. Let $AKS (\varphi_{C_j^k})$ the AKS generated from $\varphi_j^k$. We have $\forall j \in [1,n]$ and $\forall k \in [1,m]$:
 
@@ -140,23 +146,26 @@
 
 
-\subsection{Characterization of AKS}
-TODO : PEUT ETRE A VENTILER DANS DIFFERENTES PARTIES ??
+%\subsection{Characterization of AKS}
 
-\begin{definition}
-A state $s$ is an abstract state if one its variable $p$ is {\it unknown}. It
+In an abstract kripke structure a state where a variable $p$ is {\it unknown}
+can simulate all states in which $p$ is either true or false. It
 is concise representation of the set of more concrete states in which $p$
-is either true or false. 
-\end{definition}
+is either true or false.  A state $s$ is said to be an \emph{abstract state}
+if one its variable $p$ is {\it unknown}.
 
-\begin{definition}
-The {\emph concretization} of an abstract $s$ with respect to the variable $p$
+%\begin{definition}
+%A state $s$ is an {\emph abstract state} if one its variable $p$ is {\it unknown}. 
+%\end{definition}
+
+\begin{definition}[]
+The \emph {concretization} of an abstract state $s$ with respect to the variable $p$
 ({\it unknown} in that state), assigns either true or false to $p$.
 
-The {\emph abstraction} of a state $s$ with respect to the variable $p$
+The \emph {abstraction} of a state $s$ with respect to the variable $p$
 (either true or false in that state), assigns  {\it unknown} to $p$.
 \end{definition}
 
 \begin{property}
-Let A1 and A2 two AKS such that A2 is obtained by concretizing one abstract variable of A1 (resp A1 is obtained by abstracting one variable in A2). Then A1 simulates A2.
+Let A1 and A2 two abstractions such that A2 is obtained by concretizing one abstract variable of A1 (resp A1 is obtained by abstracting one variable in A2). Then A1 simulates A2.
 \end{property}
 \begin{proof}
@@ -166,12 +175,24 @@
 \end{proof}
 
- 
-2. Negation of states in an AKS
+\TODO{Name the simulation/concretization relation}
 
-a) An (abstract) configuration in a state of the AKS represents a (convex ?) set of states of the concrete component.
+\subsection{Initial abstraction}
+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$.
+In the following, we will name primary variables the set of variable that
+appears in the global property.
 
-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 
+In the initial abstraction generation, all primary variables have to be
+represented. Therefore the properties in the specification of each component
+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.
 
 
