Index: papers/FDL2012/abstraction_refinement.tex =================================================================== --- papers/FDL2012/abstraction_refinement.tex (revision 78) +++ papers/FDL2012/abstraction_refinement.tex (revision 79) @@ -30,13 +30,15 @@ The counterexample at a refinement step $i$, $\sigma$, is a path in the -abstract model $\widehat{M}_i$ which dissatisfies $\Phi$. In the counterexample given by the model-checker, the variable configuration in each state is boolean. +abstract model $\widehat{M}_i$ which dissatisfies $\Phi$. In the +counterexample given by the model-checker, the variable configuration in each +state is boolean. We name $\check{L_i}$ this new labeling. The spurious counterexample $\sigma$ is defined such that : \begin{definition} Let $\sigma$ be a \emph{counter-example} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i}, -\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of length$|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots +\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of length $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots \rightarrow s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$. \begin{itemize} \item All its variables are concrete: $\forall s_i$ and $\forall p\in -\widehat{AP}_i$, $p$ is either true or false +\widehat{AP}_i$, $p$ is either true or false according to $\check{L_i}$. (not {\it unknown}), and $s_0 $ is an initial state of the concrete system: $s_0 \in \mathbf{R}_0$ \item $\sigma$ is a counterexample in $\widehat{M}_i$: $s_0\not\models \Phi$. @@ -45,17 +47,33 @@ \end{itemize} \end{definition} - +In the following we denote by The construction of the AKS representing all executions except the one described by the spurious counter-example is done in two steps. \subsubsection{step 1 : Build the structure of the AKS.} -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}}}, -\widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}}, \widehat{F}_{\overline{\sigma}} \rangle$. + +\begin{definition} +Let $\sigma$ be a counter-example of length $|\sigma| = n$, the \emph{ AKS of the +counter-example negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}}, +\widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}}, +\widehat{F}_{\overline{\sigma}} \rangle$ is such that : \begin{itemize} -\item The set of atomic propositions coincides with the one of $\sigma$ : $AP_{\overline{\sigma}} = {AP}_i$ -\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}}.$ -\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. -\item States $s'_0$ and $s"_0$ are initial states. -\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}}$. -\item \TODO{FAIRNESS} +\item $AP_{\overline{\sigma}} = {AP}_i$: +The set of atomic propositions coincides with the one of $\sigma$ +\item $\widehat{S}_{\overline{\sigma}}$: $\{s_T\} \cup \{s_{i}'|\forall i`in +[0..n-2] \vee s_i\in +\sigma\}\cup \{\bar{s_{i}}|\forall i in [0..n-1] \vee s_i\in \sigma\}$ +\item $\widehat{L}_{\overline{\sigma}}$ is such that $s_i'$ represents the +(concrete) configuration of state $s_i$ and state $\bar{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. $s_t$ is a state where all atomic propositions are {\it unknown}. + +\item $\widehat{S}_{0{\overline{\sigma}}} = \{ s_0',\bar{s_0}\}$ +\item $\widehat{R}_{\overline{\sigma}} = \{(\bar{s_i},s_T), \forall i\in +[0..n-1]\} \cup \{(s_i',\bar{s_{i+1}}), \forall i\in[0..n-2]\} \cup +\{(s_i',s_{i+1}',\forall i\in[0..n-3]\}$ + +\item $\widehat{F}_{\overline{\sigma}} = \emptyset$ \end{itemize} +\end{definition} The 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. Index: papers/FDL2012/framework.tex =================================================================== --- papers/FDL2012/framework.tex (revision 78) +++ papers/FDL2012/framework.tex (revision 79) @@ -108,4 +108,5 @@ We 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$. + As 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. The AKS composition has been defined in \cite{braunstein_phd07}; it extends @@ -114,5 +115,5 @@ %\bigskip -\begin{definition} An \emph{Abstract model} $\widehat{M}$is obtained by +\begin{definition} An \emph{Abstract model} $\widehat{M}$ is obtained by synchronous 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; let $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]$: @@ -149,6 +150,9 @@ \end{definition} -\begin{property} -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$. +\begin{property}[Concretization] +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_i \sqsubseteq A_j$. \end{property} \begin{proof} @@ -158,5 +162,16 @@ \end{proof} -\TODO{Name the simulation/concretization relation} +\begin{property}[Compostion and Concretization] +\label{prop:concrete_compose} +Let $\widehat{M_i}$ be an abstract model of $M$ and $\varphi_j^k$ be a property +of a component $C_j$ of M, $\widehat{M}_{i+1} = \widehat{M_i}\parallel +AKS(\varphi_j^k) $ is simulated by $ \widehat{M_i}$, $\widehat{M_i} +\sqsubseteq \widehat{M}_{i+1}$. +\end{property} + +\begin{proof} +By the property of the parallel composition, we have directly $\widehat{M_i} +\sqsubseteq \widehat{M}_{i} \parallel AKS(\varphi_j^k$. +\end{proof} \subsection{Initial abstraction} Index: papers/FDL2012/ordering_filter_properties.tex =================================================================== --- papers/FDL2012/ordering_filter_properties.tex (revision 78) +++ papers/FDL2012/ordering_filter_properties.tex (revision 79) @@ -1,5 +1,3 @@ -We take advantage of the specification of verified components to build more -accurate abstractions. The key is how to select the part of the -specification relevant enough to prove the global property. We propose an + We propose an heuristic to order the properties depending on the structure of each component. @@ -10,28 +8,28 @@ %\bigskip -The ordering of the properties will be based on the variable dependency graph +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 will be weighted according to the sum of the weights +\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 will +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 will ensure that a message sent is -always acknowledge or the good target get the message. This kind of behavior +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 will be weighted 0. +whereas variables which do not interfere with a primary variable are weighted 0. Here is how we proceed: \begin{enumerate} -\item Build the dependency graph for all primary variables. +\item Build the structural dependency graph for all primary variables. \item Compute the depth of all variables (DFS or BFS) -in all dependency graph. +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 variables (see algorithm \ref{algo:weight}). +\item Give a weight to each variable (see algorithm \ref{algo:weight}). \item Compute the weight of properties for each component. \end{enumerate} @@ -131,9 +129,9 @@ -Each verified properties available pertinence will be evaluated by adding the weights of all the variables in it. +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 will have a list of properties $L_\phi$ -ordered according to their pertinence in comparison to 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. @@ -143,20 +141,21 @@ 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 form AKS definition. -<<<<<<< .mine +\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. -\remark{Cécile}{Mettre definition, property and proof ?????} Unfortunately, this refinement does not ensure that the spurious counterexample is evicted. -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$ thus won't eliminate it. +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}. We add a last -state $s_t$ where all variable are free({\it unknown}). The tree starting from this +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. @@ -184,5 +183,5 @@ \item $S_{\sigma} = \{s_{i}|s_i\in \sigma\}\cup\{s_T\}$ \item $S_{0\sigma} = \{s_{0}\}$ -\item $L_{\sigma} = \widehat{L}_i$ +\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)\}$ @@ -243,7 +242,9 @@ 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 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$. - -\begin{property}{Counterexample evicted} +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 @@ -254,18 +255,20 @@ \end{property} \begin{proof} -By construction, $AKS(\varphi)$ simulates all model that verify -$\varphi$. Thus the tree describes by $K(\sigma)$ exists in $AKS(\varphi)$, -$\sigma$ is still a possible path in $AKS(\varphi)$.\\ -Conversely $K(\sigma_i)$, where $\varphi$ does not hold, is not simulated by +\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. - +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 respect the definition \ref{def:goodrefinement}. -Moreover, the time needed to build an AKS can be neglected and building the +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.