Index: /papers/FDL2012/abstraction_refinement.tex =================================================================== --- /papers/FDL2012/abstraction_refinement.tex (revision 81) +++ /papers/FDL2012/abstraction_refinement.tex (revision 82) @@ -48,5 +48,5 @@ \begin{itemize} \item All its variables are concrete: $\forall s_i$ and $\forall p\in -\widehat{AP}_i$, $p$ is either true or false according to $\check{L_i}$. +\widehat{AP}_i$, $p$ is either true or false according to $\widehat{L_i}$. (not {\it unknown}), and $s_0 $ is an initial state of the concrete system: $s_0 \in \mathbf{R}_0$ \item $\sigma$ is a counterexample in $\widehat{M}_i$: $s_0\not\models \Phi$. @@ -71,10 +71,11 @@ \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\}$ +[0..n-2] \wedge s_i\in +\sigma\}\cup \{\bar{s_{i}}|\forall i \in [0..n-1] \wedge 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]$ +$L(s_T) = \{\top, \forall p \in AP_{\bar{\sigma}}\}$, +$L_{\overline{\sigma}}(\bar{s_i})$ is explained in the next construction step. \item $\widehat{S}_{0{\overline{\sigma}}} = \{ s_0',\bar{s_0}\}$ @@ -87,6 +88,6 @@ \end{itemize} \end{definition} -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 fo $s_i'$ represents (concrete) configuration of state $s_i$ and state $\bar{s_i}$ represents all +configurations {\it 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}. @@ -96,5 +97,5 @@ %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. +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$ 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}\}\}$. @@ -103,6 +104,6 @@ $\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], +and assigns to each of them a label of $k$ variables $\{v_0, \ldots, +v_{k-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 Index: /papers/FDL2012/framework.tex =================================================================== --- /papers/FDL2012/framework.tex (revision 81) +++ /papers/FDL2012/framework.tex (revision 82) @@ -3,5 +3,8 @@ 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$ presumably huge sized and composed of several components, satisfies a global ACTL property $\Phi$. +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 +big 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}. @@ -89,5 +92,8 @@ false ($\mathbf{f}$), true ($\mathbf{t}$) and unknown ($\top$)). States with inconsistent truth values are not represented since they refer to non possible -assignments of the atomic propositions. A set of fairness constraints eliminates non-progress cycles. +assignments of the atomic propositions. A set of fairness constraints +eliminates non-progress cycles. The transformation algorithm of a +CTL$\setminus$X property into an AKS is described in +\cite{braunstein07ctl_abstraction,braunstein_phd07}. @@ -158,6 +164,5 @@ 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$ and $A_j$ -concretizes $A_i$ , denoted by +abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$, denoted by $A_j \sqsubseteq A_i$. \end{property} @@ -180,5 +185,6 @@ 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 +The label of $s_{i+1}$ is obtained by applying the Belnap logic operator and +to values of variables in $s_i$ and $s_{\varphi_j^k}$. For all $p \in AP_i \cup AP_{\varphi_j^k}$ we have the following label~: \begin{itemize} @@ -209,5 +215,5 @@ %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 +In the initial abstraction generation, all variables that appear in $\Phi$ have to be represented. Therefore the properties in the specification of each component where these variables are present will be used to generate the initial Index: /papers/FDL2012/ordering_filter_properties.tex =================================================================== --- /papers/FDL2012/ordering_filter_properties.tex (revision 81) +++ /papers/FDL2012/ordering_filter_properties.tex (revision 82) @@ -17,5 +17,5 @@ the more closer a variable is from the primary variable the more it affects the primary variable. Hence, a property -have higher priority according to the number of primary or close to primary variables it +has 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 @@ -28,5 +28,5 @@ \begin{enumerate} \item Build the structural dependency graph for all primary variables. -\item Compute the depth of all variables (DFS or BFS) +\item Compute the depth of all variables in all dependency graphs. Note that a variable may belong to more than one dependency graph, in that case @@ -149,6 +149,4 @@ %are characterized. Hence there is more constrains behavior and more concretize %states. -Unfortunately, this refinement does not ensure that the spurious counterexample -is evicted. As we would like to ensure the elimination of the counter-example previously found, we filter out properties that do not have an impact on the counterexample @@ -158,7 +156,7 @@ 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. +%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. @@ -185,5 +183,5 @@ \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 $L_{\sigma} = \widehat{L}_i \cup L(s_T) = \{\top, \forall p \in AP_{\sigma}\}$ \item $R_{\sigma} = \{(s_{k}, s_{k+1})|(s_{k}\rightarrow s_{k+1})\in \sigma\}\cup\{(s_{n-1},s_T)\}$ @@ -269,5 +267,5 @@ \end{proof} -The propose approach ensure that the refinement excludes the counter-example +The proposed approach ensures 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