source: papers/FDL2012/ordering_filter_properties.tex @ 79

 We propose an
heuristic to order the properties  depending on the structure
of each component.
%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 has to be analyzed.
After this point, we refer to the variables present in the global property  as \emph{primary variables}.

%\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 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
contains.
Moreover, a global property often specifies the behavior at the interface of
components. Typically, a global property ensures that a message sent is
always acknowledged or the good target gets the message. This kind of behavior
relates the input-output behaviors of components. 
We have decided to allocate an extra weight for variables which are present at the interface of a component 
whereas variables which do not interfere with a primary variable are weighted 0. 
Here is how we proceed:
\begin{enumerate}
\item Build the structural dependency graph for all primary variables.
\item Compute the depth of all variables (DFS or BFS)
in all dependency graphs.
Note that a variable may belong to more than one dependency graph, in that case
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.
\end{enumerate}

The algorithm \ref{algo:weight} gives weight according to the variable distance to the
primary variable with extra weight for interface variable and primary variable.

\begin{algorithm}[ht]
\caption{Compute Weight}
\label{algo:weight}

\KwIn{ $\{V\}$, the set of all dependency graph variable}
\KwOut{$\{(v,w)| v \in V, w \in N\}$, The set of variables with their weight}

\Begin{
$p = $ max(depth(V))  \\
\For{$v\in V$}{
        d = depth(v) \;
        $w = 2^{p-d}*p$\;
        \If(v is primary variable){$d == 0$}
        {
                $w = 5 * w$\;
        }
        \If(v is an interface variable){$v\in{I\cup O}$}
        {
                $w = 3 * w $
        }
}
}
\end{algorithm}
%\begin{enumerate}
%
%\item {\emph{Establishment of primary variables' dependency and maximum graph depth}\\
%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.
%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})) $.
%
%}
%
%\item {\emph{Weight allocation for each variables} \\
%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:
%\begin{itemize}
%\item{All the variables at degree $max_d$ of every dependency graph will be allocated the weight of $p$.}
% \\ \hspace*{20mm} $Wv_{max_d} = p$
%\item{All the variables at degree $max_d - 1$ of every dependency graph will be allocated the weight of $2Wv_{max_d}$.}
%\\ \hspace*{20mm} $Wv_{max_d - 1} = 2Wv_{max_d}$
%\item{...}
%\item{All the variables at degree $1$ of every dependency graph will be allocated the weight of $2Wv_{2}$.}
% \\ \hspace*{20mm} $Wv_{1} = 2Wv_{2}$
%\item{All the variables at degree $0$ (i.e. the primary variables) will be allocated the weight of $10Wv_{1}$.}
% \\ \hspace*{20mm} $Wv_{0} = 10Wv_{1}$
%\end{itemize}
%
%We can see here that the primary variables are given a considerable
%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$.
%}
%
%
%\item {\emph{Ordering of the properties} \\
%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}}$ .
%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$.
%
%
%}
%
%\end{enumerate}

%\bigskip

%\emph{\underline{Example:}}  \\
%
%For example, if a global property $\phi$ consists of 3 variables: $ p, q, r $ where:
%\begin{itemize}
%\item{$p$ is dependent of $a$ and $b$}
%\item{$b$ is dependent of $c$}
%\item{$q$ is dependent of $x$}
%\item{$r$ is independent}
%\end{itemize}
%
%Example with unit weight= 50.
%The primary variables: $p$, $q$ and $r$ are weighted $100*10=1000$ each. \\
%The secondary level variables : $a$, $b$ and $x$ are weighted $50x2=100$ each. \\
%The tertiary level variable $c$ is weighted $50$. \\
%The weight of a non-related variable is $0$.
%
%
%\bigskip
%\begin{figure}[h!]
%   \centering
%%   \includegraphics[width=1.2\textwidth]{Dependency_graph_weight_PNG}
%%     \hspace*{-15mm}
%     \includegraphics{Dependency_graph_weight_PNG}
%   \caption{\label{DepGraphWeight} Example of weighting}
%\end{figure}

%Dans la figure~\ref{étiquette} page~\pageref{étiquette},  



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.
After this pre-processing phase, we  have a list of properties $L_\phi$
ordered according to their pertinence with regards to the global property.




\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.


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
$\sigma$ thus will not eliminate it. 
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
state $s_T$ where all variable are free({\it unknown}). The tree starting from this
state represents all the possible future of the counterexample.




%\begin{enumerate}
%
%\item {\emph{\underline{Step 1:}}} \\
%
%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$.
%
%\bigskip
%
\begin{definition}
Let $\sigma$ be a counter-example of length $n$ in $\widehat{M}_i$ such
that $ \sigma =  s_{0}\rightarrow  s_{1}\rightarrow \ldots \rightarrow
s_{n-1}$. The \emph{Kripke structure derived from $\sigma$} is 6-tuple
$K(\sigma_i) = (AP_{\sigma}, S_{\sigma}, S_{0\sigma}, L_{\sigma},
R_{\sigma},F_{\sigma})$
such that:

\begin{itemize}
\item $AP_{\sigma} = \widehat{AP}_i$ : a finite set of atomic propositions which corresponds to the variables in the abstract model     
\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 $R_{\sigma} =  \{(s_{k}, s_{k+1})|(s_{k}\rightarrow s_{k+1})\in
\sigma\}\cup\{(s_{n-1},s_T)\}$ 
\item $F_{\sigma} = \emptyset$ 
\end{itemize}
\end{definition}

%%\bigskip
%All the properties available are then model-checked on $K(\sigma_i)$.
%
%If:
%\begin{itemize}
%\item {\textbf{$K(\sigma_i) \vDash \varphi  \Rightarrow \varphi $ will not eliminate $\sigma_i$}}
%\item {\textbf{$K(\sigma_i) \nvDash \varphi  \Rightarrow \varphi $ will eliminate $\sigma_i$}}
%\end{itemize}
%
%%\bigskip
%
%
%%\begin{figure}[h!]
%%   \centering
%%%   \includegraphics[width=1.2\textwidth]{K_sigma_i_S_PNG}
%%%     \hspace*{-15mm}
%%     \includegraphics{K_sigma_i_S_PNG}
%%   \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$}
%%\end{figure}
%
%%Dans la figure~\ref{étiquette} page~\pageref{étiquette},  
%
%%\bigskip
%
%
\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
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$.

\begin{property}{Counterexample eviction}
\begin{enumerate}
\item If {\textbf{$K(\sigma) \vDash \varphi  \Rightarrow AKS(\varphi) $ will
not eliminate $\sigma$}}.
\item If {\textbf{$K(\sigma) \nvDash \varphi  \Rightarrow AKS(\varphi) $ will
eliminate $\sigma$}}.
\end{enumerate}
\end{property}
\begin{proof}
\begin{enumerate}
\item By construction, $AKS(\varphi)$ simulates all models that verify 
$\varphi$. Thus the tree described by $K(\sigma)$ is simulated by $AKS(\varphi)$,
it implies that $\sigma$ is still a possible path in $AKS(\varphi)$.
\item $K(\sigma)$, where $\varphi$ does not hold, is not simulated by
$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
$\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.


%
%}
%%\bigskip
%
%\item {\emph{\underline{Step 2:}} \\
%
%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}$.
%%\bigskip
%
%}
%\end{enumerate}
%
%$\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.
%