![(please configure the [header_logo] section in trac.ini)](/trac/verif_tools/chrome/site/your_project_logo.png){kind=logo}
Changeset 82
- Timestamp:
- Apr 5, 2012, 12:05:33 PM (13 years ago)
- Location:
- papers/FDL2012
- Files:
-
- 3 edited
-
abstraction_refinement.tex (modified) (5 diffs)
-
framework.tex (modified) (5 diffs)
-
ordering_filter_properties.tex (modified) (6 diffs)
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/abstraction_refinement.tex
r81 r82 48 48 \begin{itemize} 49 49 \item All its variables are concrete: $\forall s_i$ and $\forall p\in 50 \widehat{AP}_i$, $p$ is either true or false according to $\ check{L_i}$.50 \widehat{AP}_i$, $p$ is either true or false according to $\widehat{L_i}$. 51 51 (not {\it unknown}), and $s_0 $ is an initial state of the concrete system: $s_0 \in \mathbf{R}_0$ 52 52 \item $\sigma$ is a counterexample in $\widehat{M}_i$: $s_0\not\models \Phi$. … … 71 71 72 72 \item $\widehat{S}_{\overline{\sigma}}$: $\{s_T\} \cup \{s_{i}'|\forall i\in 73 [0..n-2] \ vee s_i\in74 \sigma\}\cup \{\bar{s_{i}}|\forall i \in [0..n-1] \ vee s_i\in \sigma\}$73 [0..n-2] \wedge s_i\in 74 \sigma\}\cup \{\bar{s_{i}}|\forall i \in [0..n-1] \wedge s_i\in \sigma\}$ 75 75 76 76 \item $\widehat{L}_{\overline{\sigma}}$ with 77 77 $L_{\overline{\sigma}}(s_i') = L_i(s_i), \forall i \in [0..n-2]$ and 78 $L_{\overline{\sigma}}(\bar{s_i}) = \bar{L_i(s_i)}, \forall i \in [0..n-1]$ 78 $L(s_T) = \{\top, \forall p \in AP_{\bar{\sigma}}\}$, 79 $L_{\overline{\sigma}}(\bar{s_i})$ is explained in the next construction step. 79 80 80 81 \item $\widehat{S}_{0{\overline{\sigma}}} = \{ s_0',\bar{s_0}\}$ … … 87 88 \end{itemize} 88 89 \end{definition} 89 Note that in the labeling function represent(concrete) configuration of state $s_i$ and state $\bar{s_i}$ represents all90 configurations butthe one of $s_i$. This last set may not be representable by90 The labeling function fo $s_i'$ represents (concrete) configuration of state $s_i$ and state $\bar{s_i}$ represents all 91 configurations {\it but} the one of $s_i$. This last set may not be representable by 91 92 the labeling function defined in def \ref{def-aks}. State labeling is treated 92 93 in the second step. $s_T$ is a state where all atomic propositions are {\it unknown}. … … 96 97 %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)$. 97 98 The set of configurations associated with a state $\bar{s_i}$ represents the 98 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.99 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. 99 100 100 101 \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 104 $\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $\bar{s_i}$ by 104 105 $k = \mid AP_{\overline\sigma} \mid$ states $\bar{s_i^j}$ with $j\in [0..k-1]$ 105 and assigns to each of them a label of $ n$ variables $\{v_0, \ldots,106 v_{ n-1}\}$ defined such that : ${L}(\bar{s_i^j} = \{\forall l \in [0..k-1],106 and assigns to each of them a label of $k$ variables $\{v_0, \ldots, 107 v_{k-1}\}$ defined such that : ${L}(\bar{s_i^j} = \{\forall l \in [0..k-1], 107 108 v_l = \neg {L}_{i}(s_i)[v_l], \forall l \in [j+1..k-1], v_l = \top\}$. each 108 109 state $\bar{s_i^j}$ is connected to the same predecessor and successor states -
papers/FDL2012/framework.tex
r81 r82 3 3 description of our methodology is shown in figure \ref{cegar}. 4 4 We take into account the structure of the system as a set of synchronous components, 5 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$. 5 each of which has been previously verified and a set of CTL properties is 6 attached to each component. This set refers to the specification of the 7 component. We would like to verify whether a concrete model, $M$ presumably 8 big sized and composed of several components, satisfies a global ACTL property $\Phi$. 6 9 %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. 7 10 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 92 false ($\mathbf{f}$), true ($\mathbf{t}$) and unknown ($\top$)). 90 93 States with inconsistent truth values are not represented since they refer to non possible 91 assignments of the atomic propositions. A set of fairness constraints eliminates non-progress cycles. 94 assignments of the atomic propositions. A set of fairness constraints 95 eliminates non-progress cycles. The transformation algorithm of a 96 CTL$\setminus$X property into an AKS is described in 97 \cite{braunstein07ctl_abstraction,braunstein_phd07}. 92 98 93 99 … … 158 164 Let $A_i$ and $A_j$ two abstractions such that $A_j$ is obtained by 159 165 concretizing one abstract variable of $A_i$ (resp. $A_i$ is obtained by 160 abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$ and $A_j$ 161 concretizes $A_i$ , denoted by 166 abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$, denoted by 162 167 $A_j \sqsubseteq A_i$. 163 168 \end{property} … … 180 185 Let $s = (s_i,s_{\varphi_j^k})$ be a state in $S_{i+1}$, such that $s_i\in S_i$ 181 186 and $s_{\varphi_j^k} \in S_{\varphi_j^k}$. 182 The label of $s_{i+1}$ respects the Belnap logic operator. For all $p \in 187 The label of $s_{i+1}$ is obtained by applying the Belnap logic operator and 188 to values of variables in $s_i$ and $s_{\varphi_j^k}$. For all $p \in 183 189 AP_i \cup AP_{\varphi_j^k}$ we have the following label~: 184 190 \begin{itemize} … … 209 215 %In the following, we will name primary variables the set of variable that 210 216 %appears in the global property. 211 In the initial abstraction generation, all variables that appear in t$\Phi$ have to be217 In the initial abstraction generation, all variables that appear in $\Phi$ have to be 212 218 represented. Therefore the properties in the specification of each component 213 219 where these variables are present will be used to generate the initial -
papers/FDL2012/ordering_filter_properties.tex
r81 r82 17 17 the more closer a variable is from the primary 18 18 variable the more it affects the primary variable. Hence, a property 19 ha vehigher priority according to the number of primary or close to primary variables it19 has higher priority according to the number of primary or close to primary variables it 20 20 contains. 21 21 Moreover, a global property often specifies the behavior at the interface of … … 28 28 \begin{enumerate} 29 29 \item Build the structural dependency graph for all primary variables. 30 \item Compute the depth of all variables (DFS or BFS)30 \item Compute the depth of all variables 31 31 in all dependency graphs. 32 32 Note that a variable may belong to more than one dependency graph, in that case … … 149 149 %are characterized. Hence there is more constrains behavior and more concretize 150 150 %states. 151 Unfortunately, this refinement does not ensure that the spurious counterexample152 is evicted.153 151 As we would like to ensure the elimination of the counter-example previously found, 154 152 we filter out properties that do not have an impact on the counterexample … … 158 156 the global property $\Phi$ 159 157 %as show in figure \ref{AKSNegCex}. 160 In case where the spurious counter-example exhibits a bounded path, we add a last161 state $s_T$ where all variable are free({\it unknown}). The tree starting from this162 state represents all the possible future of the counterexample.158 %In case where the spurious counter-example exhibits a bounded path, we add a last 159 %state $s_T$ where all variable are free({\it unknown}). The tree starting from this 160 %state represents all the possible future of the counterexample. 163 161 164 162 … … 185 183 \item $S_{\sigma} = \{s_{i}|s_i\in \sigma\}\cup\{s_T\}$ 186 184 \item $S_{0\sigma} = \{s_{0}\}$ 187 \item $L_{\sigma} = \widehat{L}_i $185 \item $L_{\sigma} = \widehat{L}_i \cup L(s_T) = \{\top, \forall p \in AP_{\sigma}\}$ 188 186 \item $R_{\sigma} = \{(s_{k}, s_{k+1})|(s_{k}\rightarrow s_{k+1})\in 189 187 \sigma\}\cup\{(s_{n-1},s_T)\}$ … … 269 267 \end{proof} 270 268 271 The propose approach ensurethat the refinement excludes the counter-example269 The proposed approach ensures that the refinement excludes the counter-example 272 270 and respects the definition \ref{def:goodrefinement}. 273 271 We will show in our experiments that first the time needed to build an AKS is
Note: See TracChangeset
for help on using the changeset viewer.
