Index: /papers/FDL2012/abstraction_refinement.tex =================================================================== --- /papers/FDL2012/abstraction_refinement.tex (revision 68) +++ /papers/FDL2012/abstraction_refinement.tex (revision 69) @@ -12,5 +12,5 @@ \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 +\item The spurious counterexample in $\widehat{M}_i$ is removed from $\widehat{M_{i+1}}$. \end{enumerate} @@ -22,7 +22,7 @@ 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. +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 counterexample, 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$. +Several proposals can be made. The most straightforward consists in building the AKS representing all possible executions except the spurious counterexample ; 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$. @@ -31,17 +31,14 @@ 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 : +The spurious counterexample $\sigma$ is defined such that : \begin{definition} -\textbf{\emph{The counterexample $\sigma$ :}} \\ -\\ -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]$. +Let $\sigma$ be a \emph{counter-example} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i}, +\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of length$|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots +\rightarrow 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}), 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 a counterexample in $\widehat{M}_i$: $s_0\not\models \Phi$. \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$. Index: /papers/FDL2012/myBib.bib =================================================================== --- /papers/FDL2012/myBib.bib (revision 68) +++ /papers/FDL2012/myBib.bib (revision 69) @@ -7,4 +7,30 @@ pages = {293-318}, year = 1992 +} + +@ARTICLE{clarke94model, + author = {E.M.~Clarke and O.~Grumberg and D.E.~Long}, + title = {{Model Checking and Abstraction}}, + journal = {ACM Transactions on Programming Languages and Systems}, + year = {1994}, + volume = {16}, + pages = {1512--1542}, + number = {5}, + address = {New York, NY, USA}, + doi = {http://doi.acm.org/10.1145/186025.186051}, + issn = {0164-0925}, + keywords = {model cheking, abstraction, CTL, preservation}, + publisher = {ACM Press} +} +@PHDTHESIS{braunstein_phd07, + author = {C.~Braunstein}, + title = {"Conception Incrémentale, Vérification de Composants Matériels et + Méthode d'abstraction pour la Vérification de SystÚmes Intégrés sur + Puce"}, + school = {{Universitée Pierre et Marie Curie (Paris 6)}}, + year = {2007}, + address = {LIP6/SOC}, + owner = {cecile}, + timestamp = {2007.04.16} } Index: /papers/FDL2012/ordering_filter_properties.tex =================================================================== --- /papers/FDL2012/ordering_filter_properties.tex (revision 68) +++ /papers/FDL2012/ordering_filter_properties.tex (revision 69) @@ -1,9 +1,9 @@ We take advantage of the specification of verified components to build more -accurate abstractions. The key, here, is how to select the part of the -specification relevent for the proof of the global property. We propose an -heuristic to order the properties of each component depending on the structure +accurate abstractions. The key is how to select the part of the +specification relevant enough to prove the global property. We propose an +heuristic to order the properties depending on the structure of each component. %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 has to be analysed. +In order to do so, the variable dependency of the variables present in global property has to be analyzed. After this point, we refer to the variables present in the global property as \emph{primary variables}. @@ -14,20 +14,21 @@ The variables in the model are weighted according to their dependency level \emph{vis-à-vis} primary variables and the properties will be weighted according to the sum of the weights -of the variables present in it. We want to select the properties that describe -behaviors that have an impact on the global one. Hence, the more closer a variable is from the primary -variable the more its behavior affects the primary variable. A property will -have higher priority the more of primary or close to primary variables it +of the variables present in it. We want to select the properties specifying +behaviors that may have an impact on the global property. We observed that +the more closer a variable is from the primary +variable the more it affects the primary variable. Hence, a property will +have higher priority according to the number of primary or close to primary variables it contains. Moreover, a global property often specifies the behavior at the interface of -components. Typicaly, a global property will ensure that a message sent is -always acknoledge or the good target get the message. This kind of behavior -relates the input-output behaviors of components. -We have decided to allocate an extra weight for variables which are present at the interface of a component -whereas variables which do not interfere in the obtention of a primary variable will be weighted 0. +components. Typically, a global property will ensure that a message sent is +always acknowledge or the good target get the message. This kind of behavior +relates the input-output behaviors of components. +We have decided to allocate an extra weight for variables which are present at the interface of a component +whereas variables which do not interfere with a primary variable will be weighted 0. Here is how we proceed: \begin{enumerate} \item Build the dependency graph for all primary variables. \item Compute the depth of all variables (DFS or BFS) -algorithm for all dependency graph. +in all dependency graph. Note that a variable may belong to more than one dependency graph, in that case we consider the minimum depth. @@ -39,5 +40,5 @@ primary variable with extra weight for interface variable and primary variable. -\begin{algorithm}[h] +\begin{algorithm}[ht] \caption{Compute Weight} \label{algo:weight} @@ -130,9 +131,9 @@ -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 +Each verified properties available pertinence will be evaluated by adding the weights of all the variables in it. +It is definitely not an exact pertinence 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. +ordered according to their pertinence in comparison to the global property. @@ -141,78 +142,78 @@ \subsection{Filtering properties} 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 +their pertinence. This refinement respects items 1 and 2 of definition \ref{def:goodrefinement}. The first item comes form AKS definition. +<<<<<<< .mine 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. -\TODO{Cecile}{Mettre definition, property and proof ?????} - -Unforutnatly, this refinement does not ensure that the spurious counter-example +\remark{Cécile}{Mettre definition, property and proof ?????} + +Unfortunately, this refinement does not ensure that the spurious counterexample 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: - -\begin{enumerate} - -\item {\emph{\underline{Step 1:}} \\ - -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 Kripke Structure 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$. - -\bigskip - +we filter out properties that don't have an impact on the counterexample $\sigma$ thus won't eliminate it. +In order to reach this objective, a Abstract Kripke structure of the counterexample $\sigma$, $K(\sigma)$ +is generated. $K(\sigma)$ is a succession of states corresponding to the counterexample path which dissatisfies +the global property $\Phi$ as show in figure \ref{AKSNegCex}. We add a last +state $s_t$ where all variable are free({\it unknown}). The tree starting from this +state represents all the possible future of the counterexample. + + + + +%\begin{enumerate} +% +%\item {\emph{\underline{Step 1:}}} \\ +% +%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 Kripke Structure 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$. +% +%\bigskip +% \begin{definition} -\textbf{\emph{The counterexample $\sigma_i$ Kripke Structure $K(\sigma_i)$ :}} \\ -Let a counterexample of length $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]$, we have \\ -$K(\sigma_i) = (AP_{\sigma_i}, S_{\sigma_i}, S_{0\sigma_i}, L_{\sigma_i}, R_{\sigma_i})$ a 5-tuple consisting of : +Let $\sigma$ be a counter-example of length $n$ in $\widehat{M}_i$ such +that $ \sigma = s_{0}\rightarrow s_{1}\rightarrow \ldots \rightarrow +s_{n-1}$. The \emph{Kripke structure derived from $\sigma$} is 6-tuple +$K(\sigma_i) = (AP_{\sigma}, S_{\sigma}, S_{0\sigma}, L_{\sigma}, +R_{\sigma},F_{\sigma})$ +such that: \begin{itemize} -\item { $AP_{\sigma_i}$ : a finite set of atomic propositions which corresponds to the variables in the abstract model $\widehat{V}_{i}$ } -\item { $S_{\sigma_i} = \{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}\}$} -\item { $S_{0\sigma_i} = \{s_{\bar{a}i,0}\}$} -\item { $L_{\sigma_i}$ : $S_{\sigma_i} \rightarrow 2^{AP_{\sigma_i}}$ : a labeling function which labels each state with the set of atomic propositions true in that state. } -\item { $R_{\sigma_i}$ = $ (s_{\bar{a}i,k}, s_{\bar{a}i,k+1})$ } +\item $AP_{\sigma} = \widehat{AP}_i$ : a finite set of atomic propositions which corresponds to the variables in the abstract model +\item $S_{\sigma} = \{s_{i}|s_i\in \sigma\}\cup\{s_T\}$ +\item $S_{0\sigma} = \{s_{0}\}$ +\item $L_{\sigma} = \widehat{L}_i$ +\item $R_{\sigma} = \{(s_{k}, s_{k+1})|(s_{k}\rightarrow s_{k+1})\in +\sigma\}\cup\{(s_{n-1},s_T)\}$ +\item $F_{\sigma} = \emptyset$ \end{itemize} \end{definition} -%\bigskip -All the properties available are then model-checked on $K(\sigma_i)$. - -If: -\begin{itemize} -\item {\textbf{$K(\sigma_i) \vDash \varphi \Rightarrow \varphi $ will not eliminate $\sigma_i$}} -\item {\textbf{$K(\sigma_i) \nvDash \varphi \Rightarrow \varphi $ will eliminate $\sigma_i$}} -\end{itemize} - -%\bigskip - - -%\begin{figure}[h!] -% \centering -%% \includegraphics[width=1.2\textwidth]{K_sigma_i_S_PNG} -%% \hspace*{-15mm} -% \includegraphics{K_sigma_i_S_PNG} -% \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$} -%\end{figure} - -%Dans la figure~\ref{étiquette} page~\pageref{étiquette},   - -%\bigskip - - +%%\bigskip +%All the properties available are then model-checked on $K(\sigma_i)$. +% +%If: +%\begin{itemize} +%\item {\textbf{$K(\sigma_i) \vDash \varphi \Rightarrow \varphi $ will not eliminate $\sigma_i$}} +%\item {\textbf{$K(\sigma_i) \nvDash \varphi \Rightarrow \varphi $ will eliminate $\sigma_i$}} +%\end{itemize} +% +%%\bigskip +% +% +%%\begin{figure}[h!] +%% \centering +%%% \includegraphics[width=1.2\textwidth]{K_sigma_i_S_PNG} +%%% \hspace*{-15mm} +%% \includegraphics{K_sigma_i_S_PNG} +%% \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$} +%%\end{figure} +% +%%Dans la figure~\ref{étiquette} page~\pageref{étiquette},   +% +%%\bigskip +% +% \begin{figure}[h!] \centering @@ -220,37 +221,68 @@ \begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=2cm, thick] - \tikzstyle{every state}=[fill=none,draw=blue,text=black, minimum size=1.5cm] - - \node[initial,state] (A) {$s_{\bar{a}i,0}$}; - \node[state] (B) [below of=A] {$s_{\bar{a}i,1}$}; - - \node[state] (C) [below of=B] {$s_{\bar{a}i,k}$}; - - \node[state] (D) [below of=C] {$s_{\bar{a}i,n-1}$}; - \node[state] (E) [below of=D] {$s_{\bar{a}i,n}$}; - - \path (A) edge node {} (B) - (B) edge node {} (C) - (C) edge node {} (D) - (D) edge node {} (E); + \tikzstyle{every state}=[fill=none,draw=blue,text=black, minimum size=1.1cm] + + \node[initial,state] (A) {$s_{0}$}; + \node[state] (B) [below of=A] {$s_{1}$}; + \node[node distance=1.5cm] (C) [below of=B] {$\ldots$}; + \node[state,node distance=1.5cm] (D) [below of=C] {$s_{n-1}$}; + \node[state] (E) [below of=D] {$s_T$}; + + \path (A) edge node {} (B) + (B) edge node {} (C) + (C) edge node {} (D) + (D) edge node {} (E) + (E) edge[loop right] node {} (E); \end{tikzpicture} - \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$} + \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma$, $K(\sigma)$} \end{figure} - -} -%\bigskip - -\item {\emph{\underline{Step 2:}} \\ - -The property at the top of the list (not yet selected and excluding the properties which are satisfied by $K(\sigma_i)$) is selected to be integrated in the generation of $\widehat{M}_{i+1}$. -%\bigskip - -} +All the properties available for refinement are then model-checked on $K(\sigma)$. If the +property holds then the property will not discriminate the counterexample. +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$ and might converge the abstract model towards a model sufficient to verify the global property $\Phi$. + +\begin{property}{Counterexample evicted} +\begin{enumerate} +\item If {\textbf{$K(\sigma) \vDash \varphi \Rightarrow AKS(\varphi) $ will +not eliminate $\sigma$}}. +\item If {\textbf{$K(\sigma) \nvDash \varphi \Rightarrow AKS(\varphi) $ will +eliminate $\sigma$}}. \end{enumerate} - -$\widehat{M}_{i+1}$ is model-checked and the refinement process is repeated until the model satisfies the global property or there is no property left to be integrated in next abstraction. - - +\end{property} +\begin{proof} +By construction, $AKS(\varphi)$ simulates all model that verify +$\varphi$. Thus the tree describes by $K(\sigma)$ exists in $AKS(\varphi)$, +$\sigma$ is still a possible path in $AKS(\varphi)$.\\ +Conversely $K(\sigma_i)$, where $\varphi$ does not hold, is not simulated by +$AKS(\varphi)$, thus $\sigma$ is not a possible path in $AKS(\varphi)$ +otherwise $AKS(\varphi)\not\models \varphi$ that is not feasible due to AKS +definition. + +\end{proof} + +The property at the top of the list (not yet selected and excluding the properties +which are satisfied by $K(\sigma)$) is selected to be integrated in the generation of $\widehat{M}_{i+1}$. +We ensure that our refinement respect the definition \ref{def:goodrefinement}. +Moreover, the time needed to build an AKS can be neglected and building the +next abstraction is just a parallel composition with the previous one. Thus the refinement + we propose is not time consuming. + + +% +%} +%%\bigskip +% +%\item {\emph{\underline{Step 2:}} \\ +% +%The property at the top of the list (not yet selected and excluding the properties which are satisfied by $K(\sigma_i)$) is selected to be integrated in the generation of $\widehat{M}_{i+1}$. +%%\bigskip +% +%} +%\end{enumerate} +% +%$\widehat{M}_{i+1}$ is model-checked and the refinement process is repeated until the model satisfies the global property or there is no property left to be integrated in next abstraction. +% +