Ignore:
Timestamp:
Mar 14, 2012, 3:40:47 PM (13 years ago)
Author:
cecile
Message:

algo weight up to date

File:
1 edited

Legend:

Unmodified
Added
Removed
  • papers/FDL2012/abstraction_refinement.tex

    r63 r65  
    3131\TODO{Rafinement par négation du contre-exemple}
    3232The counterexample at a refinement step $i$, $\sigma$ is a path in the
    33 abstract model $\widehat{M}_i$ which dissatisfy $\Phi$.  In the counterexample given by the model-checker, the variables' value in each states are boolean.
     33abstract model $\widehat{M}_i$ which dissatisfy $\Phi$.  In the counterexample given by the model-checker, the variables value in each states are boolean.
    3434The spurious counter-example $\sigma$ is defined such that :
    3535\begin{definition}
     
    7676\subsection{Ordering of properties}
    7777
    78 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 $\phi$ has to be analysed. After this point, we refer to the variables present in the global property $\phi$ as \emph{primary variables}.
    79 
    80 %\bigskip
    81 
    82 The ordering of the properties will be based on the variable dependency graph.
    83 The variables in the model are weighted according to their dependency level
    84 \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 have decided to allocate a supplementary 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. Here is how we proceed:
    85 
    86 
    87 \begin{enumerate}
    88 
    89 \item {\emph{Establishment of primary variables' dependency and maximum graph depth}\\
    90 Each primary variable will be examined and their dependency graph is elobarated. The maximum graph depth among the primary variable dependency graphs will be identified and used to calibrate the weight of all the variables related to the global property.
    91 Given the primary variables of $\phi$, $V_{\phi} =  \langle v_{\phi_0}, v_{\phi_1}, ... , v_{\phi_k}, ... , v_{\phi_n} \rangle$ and $G{\_v_{\phi_k}}$ the dependency graph of primary variable $v_{\phi_k}$, we have the maximum graph depth $max_{d} = max(depth(Gv_{\phi_0}), depth(Gv_{\phi_1}), ... , depth(Gv_{\phi_k}), ... ,$\\$ depth(Gv_{\phi_n})) $.
    92 
    93 }
    94 
    95 \item {\emph{Weight allocation for each variables} \\
    96 Let's suppose $max_d$ is the maximum dependency graph depth calculated and $p$ is the unit weight. We allocate the variable weight as follows:
    97 \begin{itemize}
    98 \item{All the variables at degree $max_d$ of every dependency graph will be allocated the weight of $p$.}
    99  \\ \hspace*{20mm} $Wv_{max_d} = p$
    100 \item{All the variables at degree $max_d - 1$ of every dependency graph will be allocated the weight of $2Wv_{max_d}$.}
    101 \\ \hspace*{20mm} $Wv_{max_d - 1} = 2Wv_{max_d}$
    102 \item{...}
    103 \item{All the variables at degree $1$ of every dependency graph will be allocated the weight of $2Wv_{2}$.}
    104  \\ \hspace*{20mm} $Wv_{1} = 2Wv_{2}$
    105 \item{All the variables at degree $0$ (i.e. the primary variables) will be allocated the weight of $10Wv_{1}$.}
    106  \\ \hspace*{20mm} $Wv_{0} = 10Wv_{1}$
    107 \end{itemize}
    108 
    109 We can see here that the primary variables are given a considerable
    110 ponderation due to their pertinency \emph{vis-à-vis} global  property. Furthermore, we will allocate a supplementary weight of $3Wv_{1}$ to variables at the interface of a component as they are the variables which assure the connection between the components if there is at least one variable in the dependency graph established in the previous step in the property. All other non-related variables have a weight equals to $0$.
    111 }
    112 
    113 
    114 \item {\emph{Ordering of the properties} \\
    115 Properties will be ordered according to the sum of the weight of the variables in it. Therefore, given a property $\varphi_i$ which contains $n+1$ variables, $V_{\varphi_i} =  \langle v_{\varphi_{i0}}, v_{\varphi_{i1}}, ... , v_{\varphi_{ik}}, ... , v_{\varphi_{in}} \rangle$, the weight  of $\varphi_i$ , $W_{\varphi_i} = \sum_{k=0}^{n} Wv_{\varphi_{ik}}$ .
    116 After this stage, we will check all the properties with weight $>0$ and allocate a supplementary weight of $3Wv_{1}$ for every variable at the interface present in the propery. After this process, the final weight of a property is obtained and the properties will be ordered in a list with the weight  decreasing (the heaviest first). We will refer to the ordered list of properties related to the global property $\phi$ as $L_\phi$.
    117 
    118 
    119 }
    120 
    121 \end{enumerate}
    122 
    123 %\bigskip
    124 
    125 \emph{\underline{Example:}}  \\
    126 
    127 For example, if a global property $\phi$ consists of 3 variables: $ p, q, r $ where:
    128 \begin{itemize}
    129 \item{$p$ is dependent of $a$ and $b$}
    130 \item{$b$ is dependent of $c$}
    131 \item{$q$ is dependent of $x$}
    132 \item{$r$ is independent}
    133 \end{itemize}
    134 
    135 Example with unit weight= 50.
    136 The primary variables: $p$, $q$ and $r$ are weighted $100x10=1000$ each. \\
    137 The secondary level variables : $a$, $b$ and $x$ are weighted $50x2=100$ each. \\
    138 The tertiary level variable $c$ is weighted $50$. \\
    139 The weight of a non-related variable is $0$.
    140 
    141 So 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 of their possible impact on the global property.
    142 
    143 \bigskip
    144 \begin{figure}[h!]
    145    \centering
    146 %   \includegraphics[width=1.2\textwidth]{Dependency_graph_weight_PNG}
    147 %     \hspace*{-15mm}
    148      \includegraphics{Dependency_graph_weight_PNG}
    149    \caption{\label{DepGraphWeight} Example of weighting}
    150 \end{figure}
    151 
    152 %Dans la figure~\ref{étiquette} page~\pageref{étiquette},  
    153 
    154 
    155 
    156 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.
    157 
    158 
    159 
    160 
    161 
    162 
    163 
    164 \subsection{Filtering properties}
    165 
    166 The refinement process from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ can be seperated into 2 steps:
    167 
    168 \begin{enumerate}
    169 
    170 \item {\emph{\underline{Step 1:}} \\
    171 
    172 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$.
    173 
    174 \bigskip
    175 
    176 \begin{definition}
    177 \textbf{\emph{The counterexample $\sigma_i$ Kripke Structure $K(\sigma_i)$ :}} \\
    178 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 \\
    179 $K(\sigma_i) = (AP_{\sigma_i}, S_{\sigma_i}, S_{0\sigma_i}, L_{\sigma_i}, R_{\sigma_i})$ a 5-tuple consisting of :
    180 
    181 \begin{itemize}
    182 \item { $AP_{\sigma_i}$ : a finite set of atomic propositions which corresponds to the variables in the abstract model $\widehat{V}_{i}$ }     
    183 \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}\}$}
    184 \item { $S_{0\sigma_i} = \{s_{\bar{a}i,0}\}$}
    185 \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. }
    186 \item { $R_{\sigma_i}$ = $ (s_{\bar{a}i,k}, s_{\bar{a}i,k+1})$ }
    187 \end{itemize}
    188 \end{definition}
    189 
    190 %\bigskip
    191 All the properties available are then model-checked on $K(\sigma_i)$.
    192 
    193 If:
    194 \begin{itemize}
    195 \item {\textbf{$K(\sigma_i) \vDash \varphi  \Rightarrow \varphi $ will not eliminate $\sigma_i$}}
    196 \item {\textbf{$K(\sigma_i) \nvDash \varphi  \Rightarrow \varphi $ will eliminate $\sigma_i$}}
    197 \end{itemize}
    198 
    199 %\bigskip
    200 
    201 
    202 \begin{figure}[h!]
    203    \centering
    204 %   \includegraphics[width=1.2\textwidth]{K_sigma_i_S_PNG}
    205 %     \hspace*{-15mm}
    206      \includegraphics{K_sigma_i_S_PNG}
    207    \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$}
    208 \end{figure}
    209 
    210 %Dans la figure~\ref{étiquette} page~\pageref{étiquette},  
    211 
    212 %\bigskip
    213 
    214 
    215 \begin{figure}[h!]
    216    \centering
    217 
    218 \begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=1.8cm,
    219                     thick]
    220   \tikzstyle{every state}=[fill=none,draw=blue,text=black]
    221 
    222   \node[initial,state] (A)                            {$s_{\bar{a}i,0}$};
    223   \node[state]           (B) [below of=A]     {$s_{\bar{a}i,1}$};
    224 
    225   \node[state]           (C) [below of=B]        {$s_{\bar{a}i,k}$};
    226 
    227   \node[state]           (D) [below of=C]       {$s_{\bar{a}i,n-1}$};
    228   \node[state]           (E) [below of=D]       {$s_{\bar{a}i,n}$};
    229 
    230   \path (A) edge              node {} (B)
    231             (B) edge       node {} (C)
    232             (C) edge             node {} (D)
    233             (D) edge             node {} (E);
    234 
    235 \end{tikzpicture}
    236 
    237    \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$}
    238 \end{figure}
    239 
    240 
    241 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$.
    242 
    243 }
    244 %\bigskip
    245 
    246 \item {\emph{\underline{Step 2:}} \\
    247 
    248 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}$.
    249 %\bigskip
    250 
    251 }
    252 \end{enumerate}
    253 
    254 $\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.
    255 
    256 
     78\input{ordering_filter_properties}
Note: See TracChangeset for help on using the changeset viewer.