Changeset 69 for papers/FDL2012


Ignore:
Timestamp:
Mar 15, 2012, 2:27:06 PM (13 years ago)
Author:
cecile
Message:

partie raffinement avec liste des propriétés mis à jour

Location:
papers/FDL2012
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • papers/FDL2012/abstraction_refinement.tex

    r68 r69  
    1212\item The new refinement is more concrete than the previous one:
    1313$\widehat{M}_{i} \sqsubseteq \widehat{M}_{i+1}$.
    14 \item The spurious counter-example in $\widehat{M}_i$ is  removed from
     14\item The spurious counterexample in $\widehat{M}_i$ is  removed from
    1515$\widehat{M_{i+1}}$.
    1616\end{enumerate}
    … …  
    2222
    2323Refinements based on the concretization of selected abstract variables in $\widehat{M}_i$ ensure item 2. Concretization can be performed either in modifying the AKS of $\widehat{M}_i$, by changing some abstract value to concrete ones, but this approach is rude : in order to ensure item 1, concretization needs to be coherent with the sequences of values in the concrete system. The difficulty resides in defining the proper abstract variable to concretize, at which precise instant, and with which Boolean value.
    24 Another way to concretize some variables at selected instants is to compose (by a synchronous product) the AKS  of $\widehat{M}_i$ with a new AKS, provided this latest represents over-approximations of the set of behaviors of $M$. By construction, this product satisfies items 1 and 2. We now have to compute an AKS eliminating the spurious counter-example, being easily computable and ensuring a quick convergence of the CEGAR loop.
     24Another way to concretize some variables at selected instants is to compose (by a synchronous product) the AKS  of $\widehat{M}_i$ with a new AKS, provided this latest represents over-approximations of the set of behaviors of $M$. By construction, this product satisfies items 1 and 2. We now have to compute an AKS eliminating the spurious counterexample, being easily computable and ensuring a quick convergence of the CEGAR loop.
    2525
    26 Several proposals can be made. The most straightforward consists in building the AKS representing all possible executions except the  spurious counter-example ; however the AKS representation may be huge and the process is not guaranteed to converge. A second possibility is to build an AKS with additional CTL properties of the components ; the AKS remains small but item 3 is not guaranteed, hence delaying the convergence. The final proposal combines both previous ones : first local CTL properties eliminating the spurious counter example are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$.
     26Several proposals can be made. The most straightforward consists in building the AKS representing all possible executions except the  spurious counterexample ; however the AKS representation may be huge and the process is not guaranteed to converge. A second possibility is to build an AKS with additional CTL properties of the components ; the AKS remains small but item 3 is not guaranteed, hence delaying the convergence. The final proposal combines both previous ones : first local CTL properties eliminating the spurious counter example are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$.
    2727
    2828
    … …  
    3131The counterexample at a refinement step $i$, $\sigma$ is a path in the
    3232abstract model $\widehat{M}_i$ which dissatisfy $\Phi$.  In the counterexample given by the model-checker, the variables value in each states are boolean.
    33 The spurious counter-example $\sigma$ is defined such that :
     33The spurious counterexample $\sigma$ is defined such that :
    3434\begin{definition}
    35 \textbf{\emph{The counterexample $\sigma$ :}} \\
    36 \\
    37 Let $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
    38 \widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ and let the length of the
    39 counterexample, $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
    40 s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$.
     35Let $\sigma$ be a \emph{counter-example} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
     36\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of  length$|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
     37\rightarrow s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$.
    4138\begin{itemize}
    4239\item All its variables are concrete: $\forall s_i$ and $\forall p\in
    4340\widehat{AP}_i$, $p$ is either true or false
    4441(not {\it unknown}), and $s_0 $ is an initial state of the concrete system: $s_0 \in \mathbf{R}_0$
    45 \item  $\sigma$ is a counter-example in  $\widehat{M}_i$: $s_0\not\models \Phi$.
     42\item  $\sigma$ is a counterexample in  $\widehat{M}_i$: $s_0\not\models \Phi$.
    4643\item  $\sigma$ is not a path of the concrete system $M$: $\exists k \in [1..n-1]$ such
    4744that $\forall j < k, (s_j,s_{j+1}) \in R$ and $(s_{k}, s_{k+1}) \not\in R$.

  • papers/FDL2012/myBib.bib

    r64 r69  
    77    pages = {293-318},
    88    year = 1992
     9}
     10
     11@ARTICLE{clarke94model,
     12  author = {E.M.~Clarke and O.~Grumberg and D.E.~Long},
     13  title = {{Model Checking and Abstraction}},
     14  journal = {ACM Transactions on Programming Languages and Systems},
     15  year = {1994},
     16  volume = {16},
     17  pages = {1512--1542},
     18  number = {5},
     19  address = {New York, NY, USA},
     20  doi = {http://doi.acm.org/10.1145/186025.186051},
     21  issn = {0164-0925},
     22  keywords = {model cheking, abstraction, CTL, preservation},
     23  publisher = {ACM Press}
     24}
     25@PHDTHESIS{braunstein_phd07,
     26  author = {C.~Braunstein},
     27  title = {"Conception Incrémentale, Vérification de Composants Matériels et
     28        Méthode d'abstraction pour la Vérification de SystÚmes Intégrés sur
     29        Puce"},
     30  school = {{Universitée Pierre et Marie Curie (Paris 6)}},
     31  year = {2007},
     32  address = {LIP6/SOC},
     33  owner = {cecile},
     34  timestamp = {2007.04.16}
    935}
    1036

  • papers/FDL2012/ordering_filter_properties.tex

    r68 r69  
    11We take advantage of the specification of verified components to build more
    2 accurate abstractions. The key, here, is how to select the part of the
    3 specification relevent for the proof of the global property. We propose an
    4 heuristic to order the properties of each component depending on the structure
     2accurate abstractions. The key is how to select the part of the
     3specification relevant enough to prove the global property. We propose an
     4heuristic to order the properties depending on the structure
    55of each component.
    66%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$.
    7 In order to do so, the variable dependency of the variables present in global property has to be analysed.
     7In order to do so, the variable dependency of the variables present in global property has to be analyzed.
    88After this point, we refer to the variables present in the global property  as \emph{primary variables}.
    99
    … …  
    1414The variables in the model are weighted according to their dependency level
    1515\emph{vis-à-vis} primary variables and the properties will be weighted according to the sum of the weights
    16 of the variables present in it. We want to select the properties that describe
    17 behaviors that have an impact on the global one. Hence, the more closer a variable is from the primary
    18 variable the more its behavior affects the primary variable. A property will
    19 have higher priority the more of primary or close to primary variables it
     16of the variables present in it. We want to select the properties specifying
     17behaviors that may have an impact on the global property. We observed that
     18the more closer a variable is from the primary
     19variable the more it affects the primary variable. Hence, a property will
     20have higher priority according to the number of primary or close to primary variables it
    2021contains.
    2122Moreover, a global property often specifies the behavior at the interface of
    22 components. Typicaly, a global property will ensure that a message sent is
    23 always acknoledge or the good target get the message. This kind of behavior
    24 relates the input-output behaviors of components.
    25 We have decided to allocate an extra weight for variables which are present at the interface of a component
    26 whereas variables which do not interfere in the obtention of a primary variable will be weighted 0.
     23components. Typically, a global property will ensure that a message sent is
     24always acknowledge or the good target get the message. This kind of behavior
     25relates the input-output behaviors of components. 
     26We have decided to allocate an extra weight for variables which are present at the interface of a component 
     27whereas variables which do not interfere with a primary variable will be weighted 0.
    2728Here is how we proceed:
    2829\begin{enumerate}
    2930\item Build the dependency graph for all primary variables.
    3031\item Compute the depth of all variables (DFS or BFS)
    31 algorithm for all dependency graph.
     32in all dependency graph.
    3233Note that a variable may belong to more than one dependency graph, in that case
    3334we consider the minimum depth.
    … …  
    3940primary variable with extra weight for interface variable and primary variable.
    4041
    41 \begin{algorithm}[h]
     42\begin{algorithm}[ht]
    4243\caption{Compute Weight}
    4344\label{algo:weight}
    … …  
    130131
    131132
    132 Each verified properties available pertinency will be evaluated by adding the weights of all the variables in it.
    133 It is definitely not an exact pertinency calculation of properties but provides a good indicator
     133Each verified properties available pertinence will be evaluated by adding the weights of all the variables in it.
     134It is definitely not an exact pertinence calculation of properties but provides a good indicator
    134135of their possible impact on the global property.
    135136After this pre-processing phase, we will have a list of properties $L_\phi$
    136 ordered according to their pertinency in comparison to the global property.
     137ordered according to their pertinence in comparison to the global property.
    137138
    138139
    … …  
    141142\subsection{Filtering properties}
    142143The refinement step consists of adding new AKS of properties selected according to
    143 their pertinency. This refinement respects the points 1 and 2 of definition
     144their pertinence. This refinement respects items 1 and 2 of definition
    144145\ref{def:goodrefinement}. The first item comes form AKS definition.
     146<<<<<<< .mine
    145147Adding a new AKS in the abstraction leads to an abstraction where more behaviors
    146148are characterized. Hence there is more constrains behavior and more concretize
    147149states.
    148150
    149 \TODO{Cecile}{Mettre definition, property and proof ?????}
    150 
    151 Unforutnatly, this refinement does not ensure that the spurious counter-example
     151\remark{Cécile}{Mettre definition, property and proof ?????}
     152
     153Unfortunately, this refinement does not ensure that the spurious counterexample
    152154is evicted.
    153155As we would like to ensure the elimination of the counterexample previously found,
    154 we filter out properties that don't have an impact on the counterexample $\sigma_i$ thus won't eliminate it.
    155 In order to reach this obective, a AKS of the counterexample $\sigma_i$, $K(\sigma_i)$
    156 is generated. $K(\sigma_i)$ is a succession of states corresponding to the counterexample path which dissatisfies
    157 the global property $\Phi$. It is an abstract kripke structure since not all
    158 variables are concrete.
    159 Each properties
    160 All the properties available are then model-checked on $K(\sigma_i)$. If the
    161 property holds then the property will not discriminate the counter-example.
    162 Hence this property is not a good candidate for refinement.
    163 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$.
    164 
    165 
    166 \TODO{Revoir la definition et Proof}
    167 
    168 The refinement process from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ can be seperated into 2 steps:
    169 
    170 \begin{enumerate}
    171 
    172 \item {\emph{\underline{Step 1:}} \\
    173 
    174 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$.
    175 
    176 \bigskip
    177 
     156we filter out properties that don't have an impact on the counterexample $\sigma$ thus won't eliminate it.
     157In order to reach this objective, a Abstract Kripke structure of the counterexample $\sigma$, $K(\sigma)$
     158is generated. $K(\sigma)$ is a succession of states corresponding to the counterexample path which dissatisfies
     159the global property $\Phi$ as show in figure \ref{AKSNegCex}. We add a last
     160state $s_t$ where all variable are free({\it unknown}). The tree starting from this
     161state represents all the possible future of the counterexample.
     162
     163
     164
     165
     166%\begin{enumerate}
     167%
     168%\item {\emph{\underline{Step 1:}}} \\
     169%
     170%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$.
     171%
     172%\bigskip
     173%
    178174\begin{definition}
    179 \textbf{\emph{The counterexample $\sigma_i$ Kripke Structure $K(\sigma_i)$ :}} \\
    180 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 \\
    181 $K(\sigma_i) = (AP_{\sigma_i}, S_{\sigma_i}, S_{0\sigma_i}, L_{\sigma_i}, R_{\sigma_i})$ a 5-tuple consisting of :
     175Let $\sigma$ be a counter-example of length $n$ in $\widehat{M}_i$ such
     176that $ \sigma =  s_{0}\rightarrow  s_{1}\rightarrow \ldots \rightarrow
     177s_{n-1}$. The \emph{Kripke structure derived from $\sigma$} is 6-tuple
     178$K(\sigma_i) = (AP_{\sigma}, S_{\sigma}, S_{0\sigma}, L_{\sigma},
     179R_{\sigma},F_{\sigma})$
     180such that:
    182181
    183182\begin{itemize}
    184 \item { $AP_{\sigma_i}$ : a finite set of atomic propositions which corresponds to the variables in the abstract model $\widehat{V}_{i}$ }     
    185 \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}\}$}
    186 \item { $S_{0\sigma_i} = \{s_{\bar{a}i,0}\}$}
    187 \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. }
    188 \item { $R_{\sigma_i}$ = $ (s_{\bar{a}i,k}, s_{\bar{a}i,k+1})$ }
     183\item $AP_{\sigma} = \widehat{AP}_i$ : a finite set of atomic propositions which corresponds to the variables in the abstract model     
     184\item $S_{\sigma} = \{s_{i}|s_i\in \sigma\}\cup\{s_T\}$
     185\item $S_{0\sigma} = \{s_{0}\}$
     186\item $L_{\sigma} = \widehat{L}_i$
     187\item $R_{\sigma} =  \{(s_{k}, s_{k+1})|(s_{k}\rightarrow s_{k+1})\in
     188\sigma\}\cup\{(s_{n-1},s_T)\}$
     189\item $F_{\sigma} = \emptyset$
    189190\end{itemize}
    190191\end{definition}
    191192
    192 %\bigskip
    193 All the properties available are then model-checked on $K(\sigma_i)$.
    194 
    195 If:
    196 \begin{itemize}
    197 \item {\textbf{$K(\sigma_i) \vDash \varphi  \Rightarrow \varphi $ will not eliminate $\sigma_i$}}
    198 \item {\textbf{$K(\sigma_i) \nvDash \varphi  \Rightarrow \varphi $ will eliminate $\sigma_i$}}
    199 \end{itemize}
    200 
    201 %\bigskip
    202 
    203 
    204 %\begin{figure}[h!]
    205 %   \centering
    206 %%   \includegraphics[width=1.2\textwidth]{K_sigma_i_S_PNG}
    207 %%     \hspace*{-15mm}
    208 %     \includegraphics{K_sigma_i_S_PNG}
    209 %   \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$}
    210 %\end{figure}
    211 
    212 %Dans la figure~\ref{étiquette} page~\pageref{étiquette},  
    213 
    214 %\bigskip
    215 
    216 
     193%%\bigskip
     194%All the properties available are then model-checked on $K(\sigma_i)$.
     195%
     196%If:
     197%\begin{itemize}
     198%\item {\textbf{$K(\sigma_i) \vDash \varphi  \Rightarrow \varphi $ will not eliminate $\sigma_i$}}
     199%\item {\textbf{$K(\sigma_i) \nvDash \varphi  \Rightarrow \varphi $ will eliminate $\sigma_i$}}
     200%\end{itemize}
     201%
     202%%\bigskip
     203%
     204%
     205%%\begin{figure}[h!]
     206%%   \centering
     207%%%   \includegraphics[width=1.2\textwidth]{K_sigma_i_S_PNG}
     208%%%     \hspace*{-15mm}
     209%%     \includegraphics{K_sigma_i_S_PNG}
     210%%   \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$}
     211%%\end{figure}
     212%
     213%%Dans la figure~\ref{étiquette} page~\pageref{étiquette},  
     214%
     215%%\bigskip
     216%
     217%
    217218\begin{figure}[h!]
    218219   \centering
    … …  
    220221\begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=2cm,
    221222                    thick]
    222   \tikzstyle{every state}=[fill=none,draw=blue,text=black, minimum size=1.5cm]
    223 
    224   \node[initial,state] (A)                            {$s_{\bar{a}i,0}$};
    225   \node[state]           (B) [below of=A]     {$s_{\bar{a}i,1}$};
    226 
    227   \node[state]           (C) [below of=B]        {$s_{\bar{a}i,k}$};
    228 
    229   \node[state]           (D) [below of=C]       {$s_{\bar{a}i,n-1}$};
    230   \node[state]           (E) [below of=D]       {$s_{\bar{a}i,n}$};
    231 
    232   \path (A) edge              node {} (B)
    233             (B) edge       node {} (C)
    234             (C) edge             node {} (D)
    235             (D) edge             node {} (E);
     223  \tikzstyle{every state}=[fill=none,draw=blue,text=black, minimum size=1.1cm]
     224
     225  \node[initial,state] (A)                    {$s_{0}$};
     226  \node[state]         (B) [below of=A]       {$s_{1}$};
     227  \node[node distance=1.5cm]       (C) [below of=B]       {$\ldots$};
     228  \node[state,node distance=1.5cm]       (D) [below of=C]     {$s_{n-1}$};
     229  \node[state]         (E) [below of=D]     {$s_T$};
     230
     231  \path (A) edge node {} (B)
     232        (B) edge node {} (C)
     233        (C) edge node {} (D)
     234        (D) edge node {} (E)
     235        (E) edge[loop right] node {} (E);
    236236
    237237\end{tikzpicture}
    238238
    239    \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$}
     239   \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma$, $K(\sigma)$}
    240240\end{figure}
    241241
    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 }
     242All the properties available for refinement are then model-checked on $K(\sigma)$. If the
     243property holds then the property will not discriminate the counterexample.
     244Hence this property is not a good candidate for refinement.
     245Therefore 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}
     248\begin{enumerate}
     249\item If {\textbf{$K(\sigma) \vDash \varphi  \Rightarrow AKS(\varphi) $ will
     250not eliminate $\sigma$}}.
     251\item If {\textbf{$K(\sigma) \nvDash \varphi  \Rightarrow AKS(\varphi) $ will
     252eliminate $\sigma$}}.
    252253\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 
     254\end{property}
     255\begin{proof}
     256By 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)$.\\
     259Conversely $K(\sigma_i)$, where $\varphi$ does not hold, is not simulated by
     260$AKS(\varphi)$, thus $\sigma$ is not a possible path in $AKS(\varphi)$
     261otherwise $AKS(\varphi)\not\models \varphi$ that is not feasible due to AKS
     262definition.
     263
     264\end{proof}
     265
     266The property at the top of the list (not yet selected and excluding the properties
     267which are satisfied by $K(\sigma)$) is selected to be integrated in the generation of $\widehat{M}_{i+1}$.
     268We ensure that our refinement respect the definition \ref{def:goodrefinement}.
     269Moreover, the time needed to build an AKS can be neglected and building the
     270next abstraction is just a parallel composition with the previous one. Thus the refinement
     271 we propose is not time consuming.
     272
     273
     274%
     275%}
     276%%\bigskip
     277%
     278%\item {\emph{\underline{Step 2:}} \\
     279%
     280%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}$.
     281%%\bigskip
     282%
     283%}
     284%\end{enumerate}
     285%
     286%$\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.
     287%
     288
Note: See TracChangeset for help on using the changeset viewer.