Changeset 63

Timestamp:

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

Author:

ema

Message:

 

Location:

papers/FDL2012

Files:

• FDL2012.tex (modified) (2 diffs)
• abstraction_refinement.tex (modified) (4 diffs)

papers/FDL2012/FDL2012.tex

@@ -85 +85 @@
 We have presented a new strategy in the abstraction generation and refinement which is well adapted for compositional embedded systems. This verification technique is compatible and suits well in the natural development process of complex systems. Our preliminary experimental results shows an interesting performance in terms duration of abstraction generation and the number of refinement iteration. Futhermore, this technique enables us to overcome repetitive counterexamples due to the presence of cycles in the system's graph.
 
-Nevertheless, in order to function well, this refinement technique requires a complete specification of every components of the concrete model. Futhermore, it may be possible that none of the properties available is capable of eliminating the counterexample which probably due to the fact that the specification is not complete or counterexample given is provoqued by the composition of components. In this case, other refinement techniques such as the refinement by eliminating the counterexample only techniques should be considered. We are currently investigating other complementary techniques to overcome these particular cases.
+Nevertheless, in order to function well, this refinement technique requires a complete specification of every components of the concrete model. Furthermore, it may be possible that none of the properties available is capable of eliminating the counterexample which probably due to the fact that the specification is not complete or counterexample given is provoked by the composition of components. In this case, other refinement techniques such as the refinement by eliminating the counterexample only techniques should be considered. We are currently investigating other complementary techniques to overcome these particular cases.
 
 
@@ -100 +100 @@
 
 
-\end{document} 
+\end{document}

papers/FDL2012/abstraction_refinement.tex

@@ -9 +9 @@
 \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}$.
-\item The new refinment is more concrete than the previous one:
+\item The new refinement is an over-approximation of the concrete model: $\widehat{M}_{i+1} \sqsubseteq \widehat{M}$.
+\item The new refinement 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
@@ -20 +20 @@
 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{Refinment by negation of the counterexample}
+Refinements based on the concretization of selected abstract variables in $\widehat{M}_i$ ensure item 2. Concretization can be performed either in modifying the AKS of $\widehat{M}_i$, by changing some abstract value to concrete ones, but this approach is rude : in order to ensure item 1, concretization needs to be coherent with the sequences of values in the concrete system. The difficulty resides in defining the proper abstract variable to concretize, at which precise instant, and with which Boolean value.
+Another way to concretize some variables at selected instants is to compose (by a synchronous product) the AKS  of $\widehat{M}_i$ with a new AKS, provided this latest represents over-approximations of the set of behaviors of $M$. By construction, this product satisfies items 1 and 2. We now have to compute an AKS eliminating the spurious counter-example, being easily computable and ensuring a quick convergence of the CEGAR loop.
+
+Several proposals can be made. The most straightforward consists in building the AKS representing all possible executions except the  spurious counter-example ; however the AKS representation may be huge and the process is not guaranteed to converge. A second possibility is to build an AKS with additional CTL properties of the components ; the AKS remains small but item 3 is not guaranteed, hence delaying the convergence. The final proposal combines both previous ones : first local CTL properties eliminating the spurious counter example are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$.
+
+
+\subsection{Refinement by negation of the counterexample}
 
 \TODO{Mettre la def avant ?}
@@ -38 +39 @@
 \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]$. 
+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}).
+(not {\it unknown}), and $s_0 $ is an initial state of the concrete system: $s_0 \in \mathbf{R}_0$
 \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$.
+\item  $\sigma$ is not a path of the concrete system $M$: $\exists k \in [1..n-1]$ such
+that $\forall j < k, (s_j,s_{j+1}) \in R$ and $(s_{k}, s_{k+1}) \not\in R$.
 \end{itemize}
 \end{definition}
@@ -55 +56 @@
 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 
+c) building the AKS of a spurious counter-example may lead to a blow-up of the number of states of the AKS