Index: /papers/FDL2012/abstraction_refinement.tex =================================================================== --- /papers/FDL2012/abstraction_refinement.tex (revision 80) +++ /papers/FDL2012/abstraction_refinement.tex (revision 81) @@ -9,7 +9,8 @@ \begin{definition} An efficient \emph{refinement} verifies the following properties: \begin{enumerate} -\item The new refinement is an over-approximation of the concrete model: $\widehat{M}_{i+1} \sqsubseteq \widehat{M}$. +\item The new refinement is an over-approximation of the concrete model: +$\widehat{M} \sqsubseteq \widehat{M}_{i+1}$. \item The new refinement is more concrete than the previous one: -$\widehat{M}_{i} \sqsubseteq \widehat{M}_{i+1}$. +$\widehat{M}_{i+1} \sqsubseteq \widehat{M}_{i}$. \item The spurious counterexample in $\widehat{M}_i$ is removed from $\widehat{M_{i+1}}$. @@ -17,23 +18,30 @@ \label{def:goodrefinement} \end{definition} - Moreover, the refinement steps should be easy to compute and ensure a fast convergence by minimizing the number of iterations of the CEGAR loop. -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 counterexample, being easily computable and ensuring a quick convergence of the CEGAR loop. +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 consistent 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 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 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$. +We propose to compose the abstraction with another AKS to build a good refinement +according to definition \ref{def:goodrefinement}. +We have several options. The most straightforward consists in building +an 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$. -\subsection{Refinement by negation of the counterexample} +\subsection{Negation of the counterexample} The counterexample at a refinement step $i$, $\sigma$, is a path in the abstract model $\widehat{M}_i$ which dissatisfies $\Phi$. In the counterexample given by the model-checker, the variable configuration in each -state is boolean. We name $\check{L_i}$ this new labeling. +state is Boolean. We name $\widehat{L_i}$ this new labeling. The spurious counterexample $\sigma$ is defined such that : \begin{definition} -Let $\sigma$ be a \emph{counter-example} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i}, +Let $\sigma$ be a \emph{spurious 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]$. @@ -47,10 +55,12 @@ \end{itemize} \end{definition} -In the following we denote by -The construction of the AKS representing all executions except the one described by the spurious counter-example is done in two steps. -\subsubsection{step 1 : Build the structure of the AKS.} +The construction of the AKS representing all executions except the one +described by the spurious counter-example is done in two steps. + +\subsubsection{Step 1~:~Build the structure of the AKS.} + \begin{definition} -Let $\sigma$ be a counter-example of length $|\sigma| = n$, the \emph{ AKS of the +Let $\sigma$ be a spurious counter-example of length $|\sigma| = n$, the \emph{ AKS of the counter-example negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}}, \widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}}, @@ -59,14 +69,15 @@ \item $AP_{\overline{\sigma}} = {AP}_i$: The set of atomic propositions coincides with the one of $\sigma$ -\item $\widehat{S}_{\overline{\sigma}}$: $\{s_T\} \cup \{s_{i}'|\forall i`in + +\item $\widehat{S}_{\overline{\sigma}}$: $\{s_T\} \cup \{s_{i}'|\forall i\in [0..n-2] \vee s_i\in -\sigma\}\cup \{\bar{s_{i}}|\forall i in [0..n-1] \vee s_i\in \sigma\}$ -\item $\widehat{L}_{\overline{\sigma}}$ is such that $s_i'$ represents the -(concrete) configuration of state $s_i$ and state $\bar{s_i}$ represents all -configurations but the one of $s_i$. This last set may not be representable by -the labeling function defined in def \ref{def-aks}. State labeling is treated -in the second step. $s_t$ is a state where all atomic propositions are {\it unknown}. +\sigma\}\cup \{\bar{s_{i}}|\forall i \in [0..n-1] \vee s_i\in \sigma\}$ + +\item $\widehat{L}_{\overline{\sigma}}$ with +$L_{\overline{\sigma}}(s_i') = L_i(s_i), \forall i \in [0..n-2]$ and +$L_{\overline{\sigma}}(\bar{s_i}) = \bar{L_i(s_i)}, \forall i \in [0..n-1]$ \item $\widehat{S}_{0{\overline{\sigma}}} = \{ s_0',\bar{s_0}\}$ + \item $\widehat{R}_{\overline{\sigma}} = \{(\bar{s_i},s_T), \forall i\in [0..n-1]\} \cup \{(s_i',\bar{s_{i+1}}), \forall i\in[0..n-2]\} \cup @@ -76,17 +87,35 @@ \end{itemize} \end{definition} -The size of this structure is linear with the size of the counter-example, however it is not a strict AKS since the representation of the set of configurations in states $s"$ may lead to a union of labels. +Note that in the labeling function represent (concrete) configuration of state $s_i$ and state $\bar{s_i}$ represents all +configurations but the one of $s_i$. This last set may not be representable by +the labeling function defined in def \ref{def-aks}. State labeling is treated +in the second step. $s_T$ is a state where all atomic propositions are {\it unknown}. +%The size of this structure is linear with the size of the counter-example. -\subsubsection{Step 2 : Expand state configurations representing the negation of a concrete configuration.} -We return back to the labeling of states of $AKS(\overline{\sigma})$. As states $s'$ are associated with the same (concrete) configuration as their corresponding state in $\sigma$, their labeling is straightforward : $\forall i \in [0..n-1], {L}_{\overline{\sigma}}(s'_i) = \widehat{L}_{i}(s_i)$. -The set of configurations associated with a state $s"_i$ represents the negation of the one represented by ${L}_{\overline{\sigma}}(s'_i)$. This negation is not representable by the label of a single state but rather by a union of $\mid AP \mid$ labels. +\subsubsection{Step 2~:~Expand state configurations representing the negation of a concrete configuration.} +%We return back to the labeling of states of $AKS(\overline{\sigma})$. As states $s'$ are associated with the same (concrete) configuration as their corresponding state in $\sigma$, their labeling is straightforward : $\forall i \in [0..n-1], {L}_{\overline{\sigma}}(s'_i) = \widehat{L}_{i}(s_i)$. +The set of configurations associated with a state $\bar{s_i}$ represents the +negation of the one represented by ${L}_i(s'_i)$. This negation is not representable by the label of a single state but rather by a union of $\mid AP \mid$ labels. -\emph{Example}. Assume $AP = \{v_0,v_1,v_2\}$ and $\sigma = s_0 \rightarrow s_1, \ldots$ and $\widehat{L}(s_0) = \{\mathbf{f},\mathbf{f},\mathbf{f}\}$ meaning the configuration associated with $s_0$ assigns false to each variable. The negation of this configuration represents a set of seven concrete configurations which are covered by three (abstract) configurations: $\{\{\mathbf{t},\top,\top\},\{\mathbf{f},\mathbf{t},\top\},\{\mathbf{f},\mathbf{f},\mathbf{t}\}\}$. +\emph{Example}. Assume $AP = \{v_0,v_1,v_2\}$ and $\sigma = s_0 \rightarrow s_1$ and $\widehat{L}(s_0) = \{\mathbf{f},\mathbf{f},\mathbf{f}\}$ the configuration associated with $s_0$ assigns false to each variable. The negation of this configuration represents a set of seven concrete configurations which are covered by three (abstract) configurations: $\{\{\mathbf{t},\top,\top\},\{\mathbf{f},\mathbf{t},\top\},\{\mathbf{f},\mathbf{f},\mathbf{t}\}\}$. -To build the final AKS representing all sequences but spurious counter-example $\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $s"_i$ by $n = \mid AP_{\overline\sigma} \mid$ states $s"_i^k$ with $k \in [0..n-1]$ and assigns to each of them a label of $n$ variables $\{v_0, \ldots, v_{n-1}\}$ defined such that : ${L}(s"_i^k) = \{\forall l \in [0..k], v_l = \neg {L}_{i}(s'_i)[v_l], \forall l \in [k+1..n-1], v_l = \top\}$. each state $s"_i^k$ is connected to predecessor and successor states as state $s"_i$ was. +To build the final AKS representing all sequences but spurious counter-example +$\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $\bar{s_i}$ by +$k = \mid AP_{\overline\sigma} \mid$ states $\bar{s_i^j}$ with $j\in [0..k-1]$ +and assigns to each of them a label of $n$ variables $\{v_0, \ldots, +v_{n-1}\}$ defined such that : ${L}(\bar{s_i^j} = \{\forall l \in [0..k-1], +v_l = \neg {L}_{i}(s_i)[v_l], \forall l \in [j+1..k-1], v_l = \top\}$. each +state $\bar{s_i^j}$ is connected to the same predecessor and successor states +as state $\bar{s_i}$. -This final AKS presents a number of states in $\cal{O}(\mid\sigma\mid\times\mid AP\mid)$. However, removing, at each refinement step, the spurious counter-example {\em only} induces a low convergence. Moreover, in some cases, this strategy may not converge: suppose that all sequences of the form $a.b^*.c$ are spurious counter-examples (here $a$, $b$ and $c$ represent concrete state configurations). At a given refinement step $i$, a particular counter example $\sigma_i = s_0 \rightarrow s_1 \rightarrow \ldots s_n$ with $L(s_0) = a, \forall k \in [1, n-1], L(s_k) = b, L(s_n) = c$. Removing this counter-example does not prevent from a new spurious counter-example at step $i+1$ : $\sigma_{i+1} = s_0 \rightarrow s_1 \rightarrow \ldots s_{n+1}$ with $L(s_0) = a, \forall k \in [1, n], L(s_k) = b, L(s_{n+1}) = c$. The strategy consisting of elimination spurious counter-example {\em one by one} diverges in this case. However, we cannot eliminate all the sequences of the form $a.b^*.c$ in a unique refinement step since we do not a priori know if at least one of these sequence is executable in the concrete model. +This final AKS presents a number of states in $\cal{O}(\mid\sigma\mid\times\mid AP\mid)$. However, removing, at each refinement step, the spurious counter-example {\em only} induces a low convergence. Moreover, in some cases, this strategy may not converge: suppose that all sequences of the form $a.b^*.c$ are spurious counter-examples (here $a$, $b$ and $c$ represent concrete state configurations). At a given refinement step $i$, a particular counter example $\sigma_i = s_0 \rightarrow s_1 \rightarrow \ldots s_n$ with $L(s_0) = a, \forall k \in [1, n-1], L(s_k) = b, L(s_n) = c$. Removing this counter-example does not prevent from a new spurious counter-example at step $i+1$ : $\sigma_{i+1} = s_0 \rightarrow s_1 \rightarrow \ldots s_{n+1}$ with $L(s_0) = a, \forall k \in [1, n], L(s_k) = b, L(s_{n+1}) = c$. The strategy consisting of elimination spurious counter-example {\em one by one} diverges in this case. However, we cannot eliminate all the sequences of the form $a.b^*.c$ in a unique refinement step since we do not a priors know if at least one of these sequence is executable in the concrete model. -From these considerations, we are interested in removing {\em sets of behaviors encompassing the spurious counter-example} but still guaranteeing an over-approximation of the set of tree-organized behaviors of the concrete model. The strengthening of the abstraction $\widehat{M}_i$ with the adjunction of AKS of already verified local CTL properties eliminates sets of behaviors and guarantees the over-approximation but does not guarantee the elimination of the counter example. We present in the following section a strategy to select sets of CTL properties eliminating the spurious counter example. +From these considerations, we are interested in removing {\em sets of +behaviors encompassing the spurious counter-example} but still guaranteeing an +over-approximation of the set of tree-organized behaviors of the concrete +model. The strengthening of the abstraction $\widehat{M}_i$ with the +addition of AKS of already verified local CTL properties eliminates sets of +behaviors and guarantees the over-approximation (property +\ref{prop:concrete_compose}) but does not guarantee the elimination of the counter example. We present in the following section a strategy to select sets of CTL properties eliminating the spurious counter example. Index: /papers/FDL2012/framework.tex =================================================================== --- /papers/FDL2012/framework.tex (revision 80) +++ /papers/FDL2012/framework.tex (revision 81) @@ -3,12 +3,17 @@ description 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 and composed of several components, satisfies a global ACTL 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}. +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$ presumably huge sized and composed of several components, satisfies a global ACTL 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} -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 the global property $\Phi$ is in the ACTL fragment, if $\Phi$ holds on the the abstract model then it holds in the concrete model as well \cite{clarke94model}. However, if $\Phi$ does not hold in the abstract model then one cannot conclude anything regarding the concrete model until the counterexample, $\sigma$, given by the model-checker has been analyzed. -In this last case, the test of spurious counter-example is translated into a +%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 the global property $\Phi$ is in the ACTL fragment, +As show in \cite{clarke94model} for over-approximation abstraction, if $\Phi$ +holds on the the abstract model then it holds in the concrete model as well. +However, if $\Phi$ does not hold in the abstract model then one cannot conclude anything regarding the concrete model until the counterexample has been analyzed. +The test of spurious counter-example is then translated into a SAT problem as in \cite{clarke00cegar}. When a counterexample is proven to be spurious, the refinement phase occurs, injecting more preciseness into the (abstract) model to be analyzed. @@ -40,7 +45,6 @@ \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 $\Phi$. - - +As mention earlier, our concrete model consists of several components and each +component comes with its specification. The concrete system is a synchronous composition of components, each of which described as a Moore machine. @@ -48,7 +52,7 @@ A \emph{Moore machine} $C$ is defined by a tuple $\langle I, O, R,$ $\delta, \lambda, \mathbf{R}_0 \rangle$, where, \begin{itemize} -\item $I$ is a finite set of boolean inputs signals. -\item $O$ is a finite set of boolean outputs signals. -\item $R$ is a finite set of boolean sequential elements (registers). +\item $I$ is a finite set of Boolean inputs signals. +\item $O$ is a finite set of Boolean outputs signals. +\item $R$ is a finite set of Boolean sequential elements (registers). \item $\delta : 2^I \times 2^R \rightarrow 2^R$ is the transition function. \item $\lambda : 2^R \rightarrow 2^O$ is the output function. @@ -57,5 +61,5 @@ \end{definition} -\emph{States} (or configurations) of the circuit correspond to boolean configurations of all the sequential elements. +\emph{States} (or configurations) of the circuit correspond to Boolean configurations of all the sequential elements. \begin{definition} @@ -70,5 +74,5 @@ \subsection{Abstraction definition} -Our abstraction consists in reducing the size of the representation model by +Our abstraction reduces the size of the representation model by letting free 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 @@ -132,5 +136,5 @@ %\subsection{Characterization of AKS} -In an abstract Kripke structure a state where a variable $p$ is {\it unknown} +In an AKS a state where a variable $p$ is {\it unknown} can simulate all states in which $p$ is either true or false. It is a concise representation of the set of more concrete states in which $p$ @@ -151,44 +155,61 @@ \begin{property}[Concretization] +\label{prop:concrete} Let $A_i$ and $A_j$ two abstractions such that $A_j$ is obtained by -concretizing one abstract variable of $A_i$ (resp $A_i$ is obtained by -abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$, denoted by -$A_i \sqsubseteq A_j$. +concretizing one abstract variable of $A_i$ (resp. $A_i$ is obtained by +abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$ and $A_j$ +concretizes $A_i$ , denoted by +$A_j \sqsubseteq A_i$. \end{property} \begin{proof} As the concretization of state reduces the set of concrete configuration the abstract state represents but does not affect the transition relation of the -AKS. The unroll execution tree of $A_j$ is a subtree of the one of $A_i$. Then $A_i$ simulates $A_j$. +AKS. The unroll execution tree of $A_j$ is a sub-tree of the one of $A_i$. Then +$A_i$ simulates $A_j$. \end{proof} -\begin{property}[Compostion and Concretization] +\begin{property}[Composition and Concretization] \label{prop:concrete_compose} Let $\widehat{M_i}$ be an abstract model of $M$ and $\varphi_j^k$ be a property of a component $C_j$ of M, $\widehat{M}_{i+1} = \widehat{M_i}\parallel -AKS(\varphi_j^k) $ is simulated by $ \widehat{M_i}$, $\widehat{M_i} -\sqsubseteq \widehat{M}_{i+1}$. +AKS(\varphi_j^k) $ is more concrete that $ \widehat{M_i}$, $\widehat{M_{i+1}} +\sqsubseteq \widehat{M}_i$. \end{property} \begin{proof} -By the property of the parallel composition, we have directly $\widehat{M_i} -\sqsubseteq \widehat{M}_{i} \parallel AKS(\varphi_j^k$. +Let $s = (s_i,s_{\varphi_j^k})$ be a state in $S_{i+1}$, such that $s_i\in S_i$ +and $s_{\varphi_j^k} \in S_{\varphi_j^k}$. +The label of $s_{i+1}$ respects the Belnap logic operator. For all $p \in +AP_i \cup AP_{\varphi_j^k}$ we have the following label~: +\begin{itemize} +\topsep -.5em +\itemsep -0.5em +\item $\widehat{L}_{i+1}[p] = \top$ iff p is {\it unknown} in both states or +does not belong to the set of atomic proposition. +\item $\widehat{L}_{i+1}[p] = \mathbf{t}$ (or $\mathbf{f}$) iff $p$ is true +(or false) in $s_{\varphi_j^k}$ (resp. $s_i$) and {\it unknown} in $s_i$ +(resp. $s_{\varphi_j^k}$). +\end{itemize} +By property \ref{prop:concrete}, $M_{i+1}$ is more concrete than $M_i$ and by +the property of parallel composition, +$\widehat{M_i} \sqsubseteq \widehat{M}_{i} \parallel AKS(\varphi_j^k$). \end{proof} \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. - -In the initial abstraction generation, all primary variables have to be +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 $\Phi$. +%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. +In the initial abstraction generation, all variables that appear int $\Phi$ 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 +where these 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. Index: /papers/FDL2012/ordering_filter_properties.tex =================================================================== --- /papers/FDL2012/ordering_filter_properties.tex (revision 80) +++ /papers/FDL2012/ordering_filter_properties.tex (revision 81) @@ -8,10 +8,11 @@ %\bigskip -The ordering of the properties is based on the variable dependency graph -where the roots are primary variables. -The variables in the model are weighted according to their dependency level -\emph{vis-à-vis} primary variables and the properties is weighted according to the sum of the weights -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 ordering of the properties is based on the variable dependency graph +%where the roots are primary variables. +%The variables in the model are weighted according to their dependency level +%\emph{vis-à-vis} primary variables and the properties is weighted according to the sum of the weights +%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 @@ -32,5 +33,6 @@ we consider the minimum depth. \item Give a weight to each variable (see algorithm \ref{algo:weight}). -\item Compute the weight of properties for each component. +\item Compute the weight of properties for each component~: sum of the +property variables weight. \end{enumerate} @@ -129,5 +131,5 @@ -Each properties pertinence is evaluated by adding the weights of all the variables in it. +%Each properties pertinence is 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. @@ -140,12 +142,11 @@ \subsection{Filtering properties} The refinement step consists of adding new AKS of properties selected according to -their pertinence. This refinement respects items 1 and 2 of definition -\ref{def:goodrefinement}. The first item comes from AKS definition and the -composition property \ref{prop:concrete_compose}. -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. - - +their pertinence. +%This refinement respects items 1 and 2 of definition +%\ref{def:goodrefinement}. The first item comes from AKS definition and the +%composition property \ref{prop:concrete_compose}. +%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. Unfortunately, this refinement does not ensure that the spurious counterexample is evicted. @@ -155,6 +156,7 @@ 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}. In case where -the counter-example exibits a bounded path, we add a last +the global property $\Phi$ +%as show in figure \ref{AKSNegCex}. +In case where the spurious counter-example exhibits a bounded path, 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. @@ -183,5 +185,5 @@ \item $S_{\sigma} = \{s_{i}|s_i\in \sigma\}\cup\{s_T\}$ \item $S_{0\sigma} = \{s_{0}\}$ -\item $L_{\sigma} = \check{L}_i$ +\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)\}$ @@ -215,32 +217,32 @@ % % -\begin{figure}[h!] - \centering - -\begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=2cm, - thick] - \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$, $K(\sigma)$} -\end{figure} +%\begin{figure}[h!] +% \centering +% +%\begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=2cm, +% thick] +% \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$, $K(\sigma)$} +%\end{figure} 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 are chosen to be +Therefore all properties that are not satisfied are chosen to be integrated in the next step of refinement. At this stage, we already have a list of potential properties that definitely eliminates the current counterexample $\sigma$ and might converge the abstract model towards a model sufficient to verify the global property $\Phi$. @@ -262,15 +264,19 @@ $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 and the composition with $M_i$ with $AKS(\varphi)$ will eleiminate +definition and the composition with $M_i$ with $AKS(\varphi)$ will eliminate $\sigma$. \end{enumerate} \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 respects the definition \ref{def:goodrefinement}. -Moreover, the time needed to build an AKS is neglectible and building the -next abstraction is just a parallel composition with the previous one. Thus the refinement - we propose is not time consuming. +The propose approach ensure that the refinement excludes the counter-example +and respects the definition \ref{def:goodrefinement}. +We will show in our experiments that first the time needed to build an AKS is +negligible and secondly the refinement converges rapidly. +%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 respects the definition \ref{def:goodrefinement}. +%Moreover, the time needed to build an AKS is neglectible and building the +%next abstraction is just a parallel composition with the previous one. Thus the refinement +% we propose is not time consuming.