Changeset 79 for papers/FDL2012


Ignore:
Timestamp:
Mar 30, 2012, 5:02:20 PM (12 years ago)
Author:
cecile
Message:

correction counter-example and its negation representation

Location:
papers/FDL2012
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • papers/FDL2012/abstraction_refinement.tex

    r76 r79  
    3030
    3131The counterexample at a refinement step $i$, $\sigma$, is a path in the
    32 abstract model $\widehat{M}_i$ which dissatisfies $\Phi$.  In the counterexample given by the model-checker, the variable configuration in each state is boolean.
     32abstract model $\widehat{M}_i$ which dissatisfies $\Phi$.  In the
     33counterexample given by the model-checker, the variable configuration in each
     34state is boolean. We name $\check{L_i}$ this new labeling.
    3335The spurious counterexample $\sigma$ is defined such that :
    3436\begin{definition}
    3537Let $\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
     38\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of  length $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
    3739\rightarrow s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$.
    3840\begin{itemize}
    3941\item All its variables are concrete: $\forall s_i$ and $\forall p\in
    40 \widehat{AP}_i$, $p$ is either true or false
     42\widehat{AP}_i$, $p$ is either true or false according to $\check{L_i}$.
    4143(not {\it unknown}), and $s_0 $ is an initial state of the concrete system: $s_0 \in \mathbf{R}_0$
    4244\item  $\sigma$ is a counterexample in  $\widehat{M}_i$: $s_0\not\models \Phi$.
    … …  
    4547\end{itemize}
    4648\end{definition}
    47 
     49In the following we denote by
    4850The construction of the AKS representing all executions except the one described by the spurious counter-example is done in two steps.
    4951\subsubsection{step 1 : Build the structure of the AKS.}
    50 Let us denote $AKS(\overline{\sigma})$ this AKS. $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}},
    51 \widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}}, \widehat{F}_{\overline{\sigma}} \rangle$.
     52
     53\begin{definition}
     54Let $\sigma$ be a counter-example of  length $|\sigma| = n$, the \emph{ AKS of the
     55counter-example negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}},
     56\widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}},
     57\widehat{F}_{\overline{\sigma}} \rangle$ is such that :
    5258\begin{itemize}
    53 \item The set of atomic propositions coincides with the one of $\sigma$ : $AP_{\overline{\sigma}} = {AP}_i$
    54 \item Build a state $s_T$, and for each state $s_i$ in $\sigma$, build two states $s'_i$ and $s"_i$.  $s_T \in S_{\overline{\sigma}}$ and forall $i$ in $[0..n-1]$ : $s'_i \in S_{\overline{\sigma}}$ and $s"_i \in S_{\overline{\sigma}}.$
    55 \item State labeling : $s'_i$ represents the (concrete) configuration of state $s_i$ and state $s"_i$  represents all configurations but the one of $s_i$. This last set may not be representable by the labeling function defined in def \ref{def-aks}. State labeling is treated in the second step.
    56 \item States $s'_0$ and $s"_0$ are initial states.
    57 \item Transitions : Forall $i$ in $[1..n-1]$, connect $s'_i$ and $s"_i$ to their predecessor state $s'_{i-1}$: $(s'_{i-1},s'_i) \in R_{\overline{\sigma}}$ and $(s'_{i-1},s"_i) \in R_{\overline{\sigma}}$ and connect all $s"$ states as predecessor of the $s_T$ state : $(s"_i,s_T) \in R_{\overline{\sigma}}$.
    58 \item \TODO{FAIRNESS}
     59\item $AP_{\overline{\sigma}} = {AP}_i$:
     60The set of atomic propositions coincides with the one of $\sigma$
     61\item $\widehat{S}_{\overline{\sigma}}$: $\{s_T\} \cup \{s_{i}'|\forall i`in
     62[0..n-2] \vee s_i\in
     63\sigma\}\cup \{\bar{s_{i}}|\forall i in [0..n-1] \vee s_i\in \sigma\}$
     64\item $\widehat{L}_{\overline{\sigma}}$ is such that $s_i'$ represents the
     65(concrete) configuration of state $s_i$ and state $\bar{s_i}$  represents all
     66configurations but the one of $s_i$. This last set may not be representable by
     67the labeling function defined in def \ref{def-aks}. State labeling is treated
     68in the second step. $s_t$ is a state where all atomic propositions are {\it unknown}.
     69
     70\item $\widehat{S}_{0{\overline{\sigma}}} = \{ s_0',\bar{s_0}\}$
     71\item $\widehat{R}_{\overline{\sigma}} = \{(\bar{s_i},s_T), \forall i\in
     72[0..n-1]\} \cup \{(s_i',\bar{s_{i+1}}), \forall i\in[0..n-2]\} \cup
     73\{(s_i',s_{i+1}',\forall  i\in[0..n-3]\}$
     74
     75\item $\widehat{F}_{\overline{\sigma}} = \emptyset$
    5976\end{itemize}
     77\end{definition}
    6078The size of this structure is linear with the size of the counter-example, however it is not a strict AKS since the representation of the set of configurations in states $s"$ may lead to a union of labels.
    6179

  • papers/FDL2012/framework.tex

    r77 r79  
    108108We denote by $\widehat{L}(s)$ the configuration of atomic propositions in state $s$ and by $\widehat{L}(s)[p]$ the projection of configuration $\widehat{L}(s)$ according to atomic proposition $p$.
    109109
     110
    110111As the abstract model $\widehat{M}$ is generated from the conjunction of verified properties of the components in the concrete model $M$, it can be seen as the composition of the AKS of each property.
    111112The AKS composition has been defined in \cite{braunstein_phd07}; it extends
    … …  
    114115%\bigskip
    115116
    116 \begin{definition} An \emph{Abstract model} $\widehat{M}$is obtained by
     117\begin{definition} An \emph{Abstract model} $\widehat{M}$ is obtained by
    117118synchronous composition of components abstractions. Let $n$ be the number of components in the model and $m$ be the number of selected verified properties of a component;
    118119let $C_j$ be a component of the concrete model $M$ and $\varphi_{j}^k$ is a CTL formula describing a satisfied property of component $C_j$. Let $AKS (\varphi_{C_j^k})$ the AKS generated from $\varphi_j^k$. We have $\forall j \in [1,n]$ and $\forall k \in [1,m]$:
    … …  
    149150\end{definition}
    150151
    151 \begin{property}
    152 Let $A_i$ and $A_j$ two abstractions such that $A_j$ is obtained by concretizing one abstract variable of $A_i$ (resp $A_i$ is obtained by abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$, denoted by $A_j \sqsubseteq A_i$.
     152\begin{property}[Concretization]
     153Let $A_i$ and $A_j$ two abstractions such that $A_j$ is obtained by
     154concretizing one abstract variable of $A_i$ (resp $A_i$ is obtained by
     155abstracting one variable in $A_j$). Then $A_i$ simulates $A_j$, denoted by
     156$A_i \sqsubseteq A_j$.
    153157\end{property}
    154158\begin{proof}
    … …  
    158162\end{proof}
    159163
    160 \TODO{Name the simulation/concretization relation}
     164\begin{property}[Compostion and Concretization]
     165\label{prop:concrete_compose}
     166Let $\widehat{M_i}$ be an abstract model of $M$ and $\varphi_j^k$ be a property
     167of a component $C_j$ of M,  $\widehat{M}_{i+1} = \widehat{M_i}\parallel
     168AKS(\varphi_j^k) $ is simulated by $ \widehat{M_i}$, $\widehat{M_i}
     169\sqsubseteq \widehat{M}_{i+1}$.
     170\end{property}
     171
     172\begin{proof}
     173By the property of the parallel composition, we have directly  $\widehat{M_i}
     174\sqsubseteq \widehat{M}_{i} \parallel AKS(\varphi_j^k$.
     175\end{proof}
    161176
    162177\subsection{Initial abstraction}

  • 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
    42heuristic to order the properties  depending on the structure
    53of each component.
    … …  
    108%\bigskip
    119
    12 The ordering of the properties will be based on the variable dependency graph
     10The ordering of the properties is based on the variable dependency graph
    1311where the roots are primary variables.
    1412The variables in the model are weighted according to their dependency level
    15 \emph{vis-à-vis} primary variables and the properties will be weighted according to the sum of the weights
     13\emph{vis-à-vis} primary variables and the properties is weighted according to the sum of the weights
    1614of the variables present in it. We want to select the properties specifying
    1715behaviors that may have an impact on the global property. We observed that
    1816the more closer a variable is from the primary
    19 variable the more it affects the primary variable. Hence, a property will
     17variable the more it affects the primary variable. Hence, a property
    2018have higher priority according to the number of primary or close to primary variables it
    2119contains.
    2220Moreover, a global property often specifies the behavior at the interface of
    23 components. Typically, a global property will ensure that a message sent is
    24 always acknowledge or the good target get the message. This kind of behavior
     21components. Typically, a global property ensures that a message sent is
     22always acknowledged or the good target gets the message. This kind of behavior
    2523relates the input-output behaviors of components.
    2624We 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.
     25whereas variables which do not interfere with a primary variable are weighted 0.
    2826Here is how we proceed:
    2927\begin{enumerate}
    30 \item Build the dependency graph for all primary variables.
     28\item Build the structural dependency graph for all primary variables.
    3129\item Compute the depth of all variables (DFS or BFS)
    32 in all dependency graph.
     30in all dependency graphs.
    3331Note that a variable may belong to more than one dependency graph, in that case
    3432we consider the minimum depth.
    35 \item Give a weight to each variables (see algorithm  \ref{algo:weight}).
     33\item Give a weight to each variable (see algorithm  \ref{algo:weight}).
    3634\item Compute the weight of properties for each component.
    3735\end{enumerate}
    … …  
    131129
    132130
    133 Each verified properties available pertinence will be evaluated by adding the weights of all the variables in it.
     131Each properties  pertinence is evaluated by adding the weights of all the variables in it.
    134132It is definitely not an exact pertinence calculation of properties but provides a good indicator
    135133of their possible impact on the global property.
    136 After this pre-processing phase, we will have a list of properties $L_\phi$
    137 ordered according to their pertinence in comparison to the global property.
     134After this pre-processing phase, we have a list of properties $L_\phi$
     135ordered according to their pertinence with regards to the global property.
    138136
    139137
    … …  
    143141The refinement step consists of adding new AKS of properties selected according to
    144142their pertinence. This refinement respects items 1 and 2 of definition
    145 \ref{def:goodrefinement}. The first item comes form AKS definition.
    146 <<<<<<< .mine
     143\ref{def:goodrefinement}. The first item comes from AKS definition and the
     144composition property \ref{prop:concrete_compose}.
    147145Adding a new AKS in the abstraction leads to an abstraction where more behaviors
    148146are characterized. Hence there is more constrains behavior and more concretize
    149147states.
    150148
    151 \remark{Cécile}{Mettre definition, property and proof ?????}
    152149
    153150Unfortunately, this refinement does not ensure that the spurious counterexample
    154151is 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.
     152As we would like to ensure the elimination of the counter-example previously found,
     153we filter out properties that do not have an impact on the counterexample
     154$\sigma$ thus will not eliminate it.
    157155In order to reach this objective, a Abstract Kripke structure of the counterexample $\sigma$, $K(\sigma)$
    158156is 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
     157the global property $\Phi$ as show in figure \ref{AKSNegCex}. In case where
     158the counter-example exibits a bounded path, we add a last
     159state $s_T$ where all variable are free({\it unknown}). The tree starting from this
    161160state represents all the possible future of the counterexample.
    162161
    … …  
    184183\item $S_{\sigma} = \{s_{i}|s_i\in \sigma\}\cup\{s_T\}$
    185184\item $S_{0\sigma} = \{s_{0}\}$
    186 \item $L_{\sigma} = \widehat{L}_i$
     185\item $L_{\sigma} = \check{L}_i$
    187186\item $R_{\sigma} =  \{(s_{k}, s_{k+1})|(s_{k}\rightarrow s_{k+1})\in
    188187\sigma\}\cup\{(s_{n-1},s_T)\}$
    … …  
    243242property holds then the property will not discriminate the counterexample.
    244243Hence 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}
     244Therefore all properties that are satisfied are chosen to be
     245integrated in the next step of refinement. At this stage, we already have a
     246list 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}
    248249\begin{enumerate}
    249250\item If {\textbf{$K(\sigma) \vDash \varphi  \Rightarrow AKS(\varphi) $ will
    … …  
    254255\end{property}
    255256\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)$,
     260it implies that $\sigma$ is still a possible path in $AKS(\varphi)$.
     261\item $K(\sigma)$, where $\varphi$ does not hold, is not simulated by
    260262$AKS(\varphi)$, thus $\sigma$ is not a possible path in $AKS(\varphi)$
    261263otherwise $AKS(\varphi)\not\models \varphi$ that is not feasible due to AKS
    262 definition.
    263 
     264definition and the composition with $M_i$ with $AKS(\varphi)$ will eleiminate
     265$\sigma$.
     266\end{enumerate}
    264267\end{proof}
    265268
    266269The property at the top of the list (not yet selected and excluding the properties
    267270which 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 neglected and building the
     271We ensure that our refinement respects the definition \ref{def:goodrefinement}.
     272Moreover, the time needed to build an AKS is neglectible and building the
    270273next abstraction is just a parallel composition with the previous one. Thus the refinement
    271274 we propose is not time consuming.
Note: See TracChangeset for help on using the changeset viewer.