Changeset 79 for papers/FDL2012/ordering_filter_properties.tex
- Timestamp:
- Mar 30, 2012, 5:02:20 PM (12 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/ordering_filter_properties.tex
r69 r79 1 We take advantage of the specification of verified components to build more 2 accurate abstractions. The key is how to select the part of the 3 specification relevant enough to prove the global property. We propose an 1 We propose an 4 2 heuristic to order the properties depending on the structure 5 3 of each component. … … 10 8 %\bigskip 11 9 12 The ordering of the properties will bebased on the variable dependency graph10 The ordering of the properties is based on the variable dependency graph 13 11 where the roots are primary variables. 14 12 The variables in the model are weighted according to their dependency level 15 \emph{vis-à -vis} primary variables and the properties will beweighted according to the sum of the weights13 \emph{vis-à -vis} primary variables and the properties is weighted according to the sum of the weights 16 14 of the variables present in it. We want to select the properties specifying 17 15 behaviors that may have an impact on the global property. We observed that 18 16 the more closer a variable is from the primary 19 variable the more it affects the primary variable. Hence, a property will17 variable the more it affects the primary variable. Hence, a property 20 18 have higher priority according to the number of primary or close to primary variables it 21 19 contains. 22 20 Moreover, a global property often specifies the behavior at the interface of 23 components. Typically, a global property will ensurethat a message sent is24 always acknowledge or the good target getthe message. This kind of behavior21 components. Typically, a global property ensures that a message sent is 22 always acknowledged or the good target gets the message. This kind of behavior 25 23 relates the input-output behaviors of components. 26 24 We have decided to allocate an extra weight for variables which are present at the interface of a component 27 whereas variables which do not interfere with a primary variable will be weighted 0.25 whereas variables which do not interfere with a primary variable are weighted 0. 28 26 Here is how we proceed: 29 27 \begin{enumerate} 30 \item Build the dependency graph for all primary variables.28 \item Build the structural dependency graph for all primary variables. 31 29 \item Compute the depth of all variables (DFS or BFS) 32 in all dependency graph .30 in all dependency graphs. 33 31 Note that a variable may belong to more than one dependency graph, in that case 34 32 we consider the minimum depth. 35 \item Give a weight to each variable s(see algorithm \ref{algo:weight}).33 \item Give a weight to each variable (see algorithm \ref{algo:weight}). 36 34 \item Compute the weight of properties for each component. 37 35 \end{enumerate} … … 131 129 132 130 133 Each verified properties available pertinence will beevaluated by adding the weights of all the variables in it.131 Each properties pertinence is evaluated by adding the weights of all the variables in it. 134 132 It is definitely not an exact pertinence calculation of properties but provides a good indicator 135 133 of their possible impact on the global property. 136 After this pre-processing phase, we willhave a list of properties $L_\phi$137 ordered according to their pertinence in comparisonto the global property.134 After this pre-processing phase, we have a list of properties $L_\phi$ 135 ordered according to their pertinence with regards to the global property. 138 136 139 137 … … 143 141 The refinement step consists of adding new AKS of properties selected according to 144 142 their pertinence. This refinement respects items 1 and 2 of definition 145 \ref{def:goodrefinement}. The first item comes f orm AKS definition.146 <<<<<<< .mine 143 \ref{def:goodrefinement}. The first item comes from AKS definition and the 144 composition property \ref{prop:concrete_compose}. 147 145 Adding a new AKS in the abstraction leads to an abstraction where more behaviors 148 146 are characterized. Hence there is more constrains behavior and more concretize 149 147 states. 150 148 151 \remark{Cécile}{Mettre definition, property and proof ?????}152 149 153 150 Unfortunately, this refinement does not ensure that the spurious counterexample 154 151 is evicted. 155 As we would like to ensure the elimination of the counterexample previously found, 156 we filter out properties that don't have an impact on the counterexample $\sigma$ thus won't eliminate it. 152 As we would like to ensure the elimination of the counter-example previously found, 153 we filter out properties that do not have an impact on the counterexample 154 $\sigma$ thus will not eliminate it. 157 155 In order to reach this objective, a Abstract Kripke structure of the counterexample $\sigma$, $K(\sigma)$ 158 156 is generated. $K(\sigma)$ is a succession of states corresponding to the counterexample path which dissatisfies 159 the global property $\Phi$ as show in figure \ref{AKSNegCex}. We add a last 160 state $s_t$ where all variable are free({\it unknown}). The tree starting from this 157 the global property $\Phi$ as show in figure \ref{AKSNegCex}. In case where 158 the counter-example exibits a bounded path, we add a last 159 state $s_T$ where all variable are free({\it unknown}). The tree starting from this 161 160 state represents all the possible future of the counterexample. 162 161 … … 184 183 \item $S_{\sigma} = \{s_{i}|s_i\in \sigma\}\cup\{s_T\}$ 185 184 \item $S_{0\sigma} = \{s_{0}\}$ 186 \item $L_{\sigma} = \ widehat{L}_i$185 \item $L_{\sigma} = \check{L}_i$ 187 186 \item $R_{\sigma} = \{(s_{k}, s_{k+1})|(s_{k}\rightarrow s_{k+1})\in 188 187 \sigma\}\cup\{(s_{n-1},s_T)\}$ … … 243 242 property holds then the property will not discriminate the counterexample. 244 243 Hence this property is not a good candidate for refinement. 245 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$. 246 247 \begin{property}{Counterexample evicted} 244 Therefore all properties that are satisfied are chosen to be 245 integrated in the next step of refinement. At this stage, we already have a 246 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$. 247 248 \begin{property}{Counterexample eviction} 248 249 \begin{enumerate} 249 250 \item If {\textbf{$K(\sigma) \vDash \varphi \Rightarrow AKS(\varphi) $ will … … 254 255 \end{property} 255 256 \begin{proof} 256 By construction, $AKS(\varphi)$ simulates all model that verify 257 $\varphi$. Thus the tree describes by $K(\sigma)$ exists in $AKS(\varphi)$, 258 $\sigma$ is still a possible path in $AKS(\varphi)$.\\ 259 Conversely $K(\sigma_i)$, where $\varphi$ does not hold, is not simulated by 257 \begin{enumerate} 258 \item By construction, $AKS(\varphi)$ simulates all models that verify 259 $\varphi$. Thus the tree described by $K(\sigma)$ is simulated by $AKS(\varphi)$, 260 it implies that $\sigma$ is still a possible path in $AKS(\varphi)$. 261 \item $K(\sigma)$, where $\varphi$ does not hold, is not simulated by 260 262 $AKS(\varphi)$, thus $\sigma$ is not a possible path in $AKS(\varphi)$ 261 263 otherwise $AKS(\varphi)\not\models \varphi$ that is not feasible due to AKS 262 definition. 263 264 definition and the composition with $M_i$ with $AKS(\varphi)$ will eleiminate 265 $\sigma$. 266 \end{enumerate} 264 267 \end{proof} 265 268 266 269 The property at the top of the list (not yet selected and excluding the properties 267 270 which are satisfied by $K(\sigma)$) is selected to be integrated in the generation of $\widehat{M}_{i+1}$. 268 We ensure that our refinement respect the definition \ref{def:goodrefinement}.269 Moreover, the time needed to build an AKS can be neglectedand building the271 We ensure that our refinement respects the definition \ref{def:goodrefinement}. 272 Moreover, the time needed to build an AKS is neglectible and building the 270 273 next abstraction is just a parallel composition with the previous one. Thus the refinement 271 274 we propose is not time consuming.
Note: See TracChangeset
for help on using the changeset viewer.